Date: Thu, 12 Sep 1996 14:24:06 +0200
From: reichel@tcs.inf.tu-dresden.de (Horst Reichel)
Message-Id: <9609121224.AA01164@ithif17.ithi>
To: caml-list@pauillac.inria.fr
Subject: Caml semantics
Hi,
can somebody give me a reference which deals with the following
questions?
What is the formal semantics of recursive data types in Caml and Ocaml?
Since recursive values like d and e defined by
let rec d = 3 :: e and e = 5 :: d ;;
are typed as "int list" values the semantics of recursive type definitions
ist not the initial algebra of least fixpoint semantics (as in SML).
What are the values of "int list"?
If we take all finite and infinite lists, one would take the
terminal co--algebra or greatest fixpoint semantics. In that case I would
expect lazy evaluation to get a value also for
head(merge(d,e));;
with
let rec merge = function ([],l) -> l | (l,[]) -> l
| (x :: l1,l) -> x :: merge(l,l1) ;;
The present implementations get out of memory during evaluation.
The present implementations seem to make no difference between
inductive data types and co--inductive data types, which are
distinguished in CHARITY. In CHARITY is co-induction the tool to
define functions on values of co-data types. How I can define
functions in Caml or Ocaml which manipulates recursive types like
d and e above. A reference to streams is not a satisfying answer, since
in the more general situation given by
type 'a tree = Node of ('a * 'a tree) list ;;
let rec a = Node([(1,b);(2,c)]) and
b = Node([(2,c);(3,Node[])]) and
c = Node([(3,a);(4;Node[])]) ;;
one gets a, b c of type "int tree" and the "stream" module does not help
any more. Recursive values of type "'a tree" allow the representation
of infinite computation trees used in CCS. How one can define the
process composing operations of process algebras in Caml for these
infinite computation trees?
Thanks for help!
Horst