From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.6.10/8.6.6) id RAA24707 for caml-redistribution; Thu, 12 Sep 1996 17:11:26 +0200
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.6.10/8.6.6) with ESMTP id OAA21405 for <caml-list@pauillac.inria.fr>; Thu, 12 Sep 1996 14:24:44 +0200
Received: from irz301.inf.tu-dresden.de (irz301.inf.tu-dresden.de [141.76.1.11]) by concorde.inria.fr (8.7.1/8.7.1) with SMTP id OAA23497 for <caml-list@pauillac.inria.fr>; Thu, 12 Sep 1996 14:24:22 +0200 (MET DST)
Received: from tcs.inf.tu-dresden.de (tcs.inf.tu-dresden.de [141.76.75.101]) by irz301.inf.tu-dresden.de (8.6.12/8.6.12-s1) with SMTP id OAA20136 for <caml-list@pauillac.inria.fr>; Thu, 12 Sep 1996 14:24:02 +0200
Received: from ithif17.ithi by tcs.inf.tu-dresden.de (4.1/SMI-4.1)
	id AA03648; Thu, 12 Sep 96 14:23:53 +0200
Received: by ithif17.ithi (5.x/SMI-SVR4)
	id AA01164; Thu, 12 Sep 1996 14:24:06 +0200
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
X-Sun-Charset: US-ASCII
Sender: weis


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