I think you may be able to make your needs more precise by explicitly
considering what your co-algebra would be.
In particular, write down the type of the “general” destructor
myType -> F(myType)
For lazy lists, this is
α llist -> (α # α llist) option
For the co-algebraic numbers it’s
num -> num option
For arbitrarily (but finite)-branching trees, it’s
Tree -> Tree list
(If you change list to llist you get possibly infinitely branching trees.)
In the lazy lists, this destructor might be called “HDTL”; in the numbers, it’s
“predecessor”; in the trees it’s “children”. Because the types are
co-algebraic each might be iterable an infinite number of times. (The
corresponding destructors in the algebraic types are always well-founded.)
What are the co-algebras for your desired types? I don’t think I’ve understood
what you want, but it superficially appears as if you want dependent types,
where you combine the type with some term-level predicate. That sort of thing
is impossible to capture within a HOL type.
Finally, I’m afraid that there is no general tool for defining co-algebraic
types in HOL4 at the moment.
Michael
From: Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Sunday, 6 May 2018 at 11:58
To: hol-info <hol-info@lists.sourceforge.net>
Cc: Waqar Ahmad <waqar.ah...@seecs.edu.pk>
Subject: [Hol-info] Extension of Co-algebraic Datatype
Hi,
Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which is
developed based on the co-algebraic datatype. I understand that the datatype 'a
llist is derived as a subset of the option type :num -> 'a option. Now, I
want to define a new datatype based on datatype 'a llist. For instance,
P of 'a llist
such that P: 'a llist -> 'a stream, where 'a stream is essentially the similar
datatype as 'a llist but having different properties. In shallow embedding, I
can define it by using filter function of llistTheory as:
val Stream = Define `Stream L = LFILTER (\n:'a. T) L`;
One way of defining the co-inductive datatype stream is to follow the same
procedure as described in "llistTheory", which is quite cumbersome. Is there
any alternate way similar to that of package "Hol_datatype"?
Secondly, Is it possible to define a co-inductive datatype that takes a set
type (:'a -> bool) and maps it to a set of type (:'a llist -> bool)? A similar
function, in shallow embedding, I can think of is:
val streams_def = Define
`streams A = IMAGE (\a. Stream a) {llist_abs x | x IN A} `;
where the function streams is of type (:num -> 'a option) ->bool -> 'a llist->
bool
In some cases, the function streams doesn't suffice for modeling the correct
behavior of streams related properties..
Any suggestion or thoughts would be highly helpful...
--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
[http://research.bournemouth.ac.uk/wp-content/uploads/2014/02/NUST_Logo2.png]
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
