Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Tue, 6 Oct 92 10:35:42 -0700
From: austel@edu.ucla.cs (Vernon Austel)
Message-Id: <9210061735.AA17714@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: inductively defined recursive types


Say you want to model lists; not abstract ones, but ones actually
implemented in an array of memory cells.
This is my rendition:

new_theory `List`;;

% Assume that memory cells are tagged as pointers or values 	%
define_type `Cell` `Cell = VAL num | PTR num`;;

% This is the machine memory - infinite for simplicity 		%
new_type_abbrev(`Mem`, ":num->Cell");;

% A List in this memory is either a null pointer, 		%
% or a pointer to a List together with some value in the next 	%
% cell.								%
let (List_rules,List_ind) = 
	let List = "List:num->Mem->bool" in
	let M = "M:Mem" in
	new_inductive_definition false `List` 
	("^List n M", [])

	[ [	
	  % -------------------------------- %	"^M n = PTR 0" ],
		"^List n M";

	  [	
	  % -------------------------------- %	"^M n = PTR next";
						"^M (SUC n) = VAL val";
					   	"^List next M"],
		"^List n M"
	];;

close_theory();;


Although this isn't syntactically a data type, I can't help but think
of the objects that are in the relation List as constituting one.
Unfortunately, this kind of list is much more difficult to use
in HOL than one defined syntactically, using define_type.

As it turns out, it seems pretty straight-forward to massage
relations defined on these kinds of data types into recursive functions.
The advantage is that such recursive functions are easier to 
deal with that relations (or so it appears to me).
For example, a recursive function that computes the length of such
lists would look something like this:

	|- !l M. (null l M ==> (length l M = 0)) /\
		 (link l M ==> (length l M = SUC (length (M l) M)))

where
	|- !l M. null l M = (M l = PTR o)
	|- !l M. link l M = ?next. (M l = PTR next) /\
 				    (M (SUC l) = CONST val) /\
				    (List next M)

(The functions ``null'' and ``link'' just encapsulate the premisses
and side-conditions of the inductive rules for List.)

Note that the specification of length above is not a definition,
because one can't define recursive functions on non-recursive data
types in HOL (as far as I know); however, it has all the flavor of one.

I haven't gotten as far as being able to generate such theorems yet,
but I'm about halfway there and am pretty sure that I can.
My questions are:

0. Is there a better way to do this?
1. Does this interest anyone?
2. Has anyone else already done this?
3. Would a facility like this be a useful addition to the HOL library?


Thanks,
Vernon Austel
austel@cs.ucla.edu