You can probably define a function of that type, but you can’t define a
*constructor* of that type for llist. (Contrast what I’d consider to be
llist’s standard constructors, LNIL and LCONS. They have types α llist, and α
-> α llist -> α llist respectively.)
You said you wanted a stream type, does this mean you want a constructor for
stream of type
(α -> bool) -> α stream
?
Such a constructor is not recursive, so I can just write
Datatype`stream = SetConstructor (α -> bool)`
The SetConstructor term then has the desired type.
So I’m afraid I still don’t understand your question.
Michael
From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Monday, 7 May 2018 at 11:38
To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype
Thanks for the explanation. Let me state it clearly. Can I write down a
constructor of type
(α -> bool) -> α llist
On Sun, May 6, 2018 at 8:39 PM,
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>> wrote:
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<mailto:hol-info@lists.sourceforge.net>>
Reply-To: Waqar Ahmad
<12phdwah...@seecs.edu.pk<mailto:12phdwah...@seecs.edu.pk>>
Date: Sunday, 6 May 2018 at 11:58
To: hol-info
<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
Cc: Waqar Ahmad <waqar.ah...@seecs.edu.pk<mailto: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<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
--
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/
------------------------------------------------------------------------------
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
