Caml semantics
 reichel@t...
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  19960912 (15:11) 
From:  reichel@t... 
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 coalgebra 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 coinductive data types, which are distinguished in CHARITY. In CHARITY is coinduction the tool to define functions on values of codata 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