[Prev][Next][Index][Thread]
Positive inductive definitions revisited
Recently Martin Hoffman presented program (in Lego notation), which computes
the list of entries of a binary labelled tree in the breadth first order
using non strictly positive datatype.
Below this program is rewritten in IPLL, which I devised for experimentation
with (positive) inductive definitions. It is shorter and easier to read.
The notation is similar to SML or Miranda. All terms are strongly normalizing
and confluent since function definitions must be explicit, recursion being
provided by iterators (or recursors), whose names, types and defining equations
are automatically generated from the datatype definition.
type CHAR = A|B|C|D|E|F|G|H|I|J|K|L|M;
(*--------------------------------------------------------------------------*)
type LIST 'a = Nil | Cons 'a (LIST 'a);
(*--------------------------------------------------------------------------*)
type TREE 'a = Leaf 'a | Node 'a (TREE 'a) (TREE 'a);
(*--------------------------------------------------------------------------*)
type CONT 'a = DC | CC ((CONT 'a) -> LIST 'a) -> LIST 'a;
(*--------------------------------------------------------------------------*)
val o = fn g f x => g ( f x );
(*--------------------------------------------------------------------------*)
val apply = fn k => _CONTit k (fn g => g DC)
(fn h g => h (fn f => g ( CC f)));
val breadth = fn t => _TREEit t
(fn a now => CC (fn later => Cons a (apply now later)))
(fn a brl brr now =>
CC (fn later => Cons a (apply now (o later (o brl brr))))
);
(*--------------------------------------------------------------------------*)
val extract = fn k => _CONTit k Nil (fn f => f (fn l => l));
(*--------------------------------------------------------------------------*)
val run = fn t => extract (breadth t DC);
(*--------------------------------------------------------------------------*)
val t = Node A
(Node B
(Node D (Leaf H) (Leaf I))
(Node E (Leaf J) (Leaf K))
)
(Node C
(Leaf F)
(Node G (Leaf L) (Leaf M))
);
(*--------------------------------------------------------------------------*)
run t;
This program was compiled from the file "lego.ipll" and system respons was as
follows:
THE INFERENTIAL PROGRAMMING LANGUAGE AND LOGIC SYSTEM ver. 1.5 (1-DEC-1992)
(c) Technical University of Wroclaw, 1992
Opening lego.ipll
+ type CHAR = A|B|C|D|E|F|G|H|I|J|K|L|M;
type CHAR
con A : CHAR
con B : CHAR
con C : CHAR
con D : CHAR
con E : CHAR
con F : CHAR
con G : CHAR
con H : CHAR
con I : CHAR
con J : CHAR
con K : CHAR
con L : CHAR
con M : CHAR
iter _CHARit : CHAR -> 'a -> 'a -> 'a -> 'a -> 'a -> 'a -> 'a -> 'a -> 'a
-> 'a -> 'a -> 'a -> 'a -> 'a
comp _CHARit A z y x w v u t s r q p o n = z
comp _CHARit B z y x w v u t s r q p o n = y
comp _CHARit C z y x w v u t s r q p o n = x
comp _CHARit D z y x w v u t s r q p o n = w
comp _CHARit E z y x w v u t s r q p o n = v
comp _CHARit F z y x w v u t s r q p o n = u
comp _CHARit G z y x w v u t s r q p o n = t
comp _CHARit H z y x w v u t s r q p o n = s
comp _CHARit I z y x w v u t s r q p o n = r
comp _CHARit J z y x w v u t s r q p o n = q
comp _CHARit K z y x w v u t s r q p o n = p
comp _CHARit L z y x w v u t s r q p o n = o
comp _CHARit M z y x w v u t s r q p o n = n
+ (*--------------------------------------------------------------------------*)
= type LIST 'a = Nil | Cons 'a (LIST 'a);
type LIST 'a
con Nil : LIST 'a
con Cons : 'a -> (LIST 'a) -> LIST 'a
iter _LISTit : (LIST 'a) -> 'b -> ('a -> 'b -> 'b) -> 'b
comp _LISTit Nil z y = z
comp _LISTit (Cons z y) x w = w z (_LISTit y x w)
+
= (*--------------------------------------------------------------------------*)
= type TREE 'a = Leaf 'a | Node 'a (TREE 'a) (TREE 'a);
type TREE 'a
con Leaf : 'a -> TREE 'a
con Node : 'a -> (TREE 'a) -> (TREE 'a) -> TREE 'a
iter _TREEit : (TREE 'a) -> ('a -> 'b) -> ('a -> 'b -> 'b -> 'b) -> 'b
comp _TREEit (Leaf z) y x = y z
comp _TREEit (Node z y x) w v = v z (_TREEit y w v) (_TREEit x w v)
+ (*--------------------------------------------------------------------------*)
= type CONT 'a = DC | CC ((CONT 'a) -> LIST 'a) -> LIST 'a;
type CONT 'a
con DC : CONT 'a
con CC : (((CONT 'a) -> LIST 'a) -> LIST 'a) -> CONT 'a
iter _CONTit : (CONT 'a) -> 'b -> ((('b -> LIST 'a) -> LIST 'a) -> 'b) -> 'b
comp _CONTit DC z y = z
comp _CONTit (CC z) y x = x (fn w => z (fn v => w (_CONTit v y x)))
+ (*--------------------------------------------------------------------------*)
= val o = fn g f x => g ( f x );
val o : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+
= (*--------------------------------------------------------------------------*)
= val apply = fn k => _CONTit k (fn g => g DC)
= (fn h g => h (fn f => g ( CC f)));
val apply : (CONT 'a) -> ((CONT 'a) -> LIST 'a) -> LIST 'a
+ val breadth = fn t => _TREEit t
= (fn a now => CC (fn later => Cons a (apply now later)))
= (fn a brl brr now =>
= CC (fn later => Cons a (apply now (o later (o brl brr))))
= );
val breadth : (TREE 'a) -> (CONT 'a) -> CONT 'a
+
= (*--------------------------------------------------------------------------*)
= val extract = fn k => _CONTit k Nil (fn f => f (fn l => l));
val extract : (CONT 'a) -> LIST 'a
+
= (*--------------------------------------------------------------------------*)
= val run = fn t => extract (breadth t DC);
val run : (TREE 'a) -> LIST 'a
+ (*--------------------------------------------------------------------------*)
= val t = Node A
= (Node B
= (Node D (Leaf H) (Leaf I))
= (Node E (Leaf J) (Leaf K))
= )
= (Node C
= (Leaf F)
= (Node G (Leaf L) (Leaf M))
= );
val t : TREE CHAR
+ (*--------------------------------------------------------------------------*)
= run t;
Cons A (Cons B (Cons C (Cons D (Cons E (Cons F (Cons G (Cons H (Cons I (Cons J
(Cons K (Cons L (Cons M Nil)))))))))))) : LIST CHAR
+
=
Closing lego.ipll
IPLL exit - returning to SML
Recursors are also generated, but this information was removed from the
protocol, since they are not used in this program.
In view of strong normalization and confluence we have decidable (intensional)
equality between terms of any type, which can be used in automatic verification
of programs, as in the following example.
Equational specificationn of Ackermann's function
ack 0 v = Suc v
ack (Suc u) 0 = ack u 1
ack (Suc u) (Suc v) = ack u (ack (Suc u) v)
The program below solves and verifies these equations.
type NAT = Suc NAT | O;
(*-------------------------------------------------------------------------*)
val ack = fn u => _NATit u (fn y v => _NATit v y (y (Suc O))) Suc;
(* Verification *)
( fn v => ack O v) = ( fn v => Suc v );
( fn u v => ack (Suc u) O ) = ( fn u v => ack u (Suc O) );
( fn u v => ack (Suc u) (Suc v) ) = ( fn u v => ack u (ack (Suc u) v) );
Interactive session looks as follows:
+ type NAT = Suc NAT | O;
type NAT
con Suc : NAT -> NAT
con O : NAT
iter _NATit : NAT -> ('a -> 'a) -> 'a -> 'a
comp _NATit (Suc z) y x = y (_NATit z y x)
comp _NATit O z y = y
rec _NATrec : NAT -> (NAT * 'a -> 'a) -> 'a -> 'a
comp _NATrec (Suc z) y x = y (z , _NATrec z y x)
comp _NATrec O z y = y
+ (*-------------------------------------------------------------------------*)
= val ack = fn u => _NATit u (fn y v => _NATit v y (y (Suc O))) Suc;
val ack : NAT -> NAT -> NAT
+
= (* Verification *)
= ( fn v => ack O v) = ( fn v => Suc v );
True : BOOL
+ ( fn u v => ack (Suc u) O ) = ( fn u v => ack u (Suc O) );
True : BOOL
+ ( fn u v => ack (Suc u) (Suc v) ) = ( fn u v => ack u (ack (Suc u) v) );
True : BOOL
+
I devised similar algorithms for inductive types defined as greatest fixed
points, as well as algorithms translating programs and types in IPLL into
terms and types in F but they are not implemented (yet). Current version of
IPLL was implemented by my student in Standard ML Core Language as a course
project.
-- Zdzislaw Splawski
Centre of Informatics
Technical University of Wroclaw
Wybrzeze Wyspianskiego 27, Poland