Re: [Hol-info] Extension of Co-algebraic Datatype

[Waqar Ahmad via hol-info]

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,  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 
> *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Sunday, 6 May 2018 at 11:58
> *To: *hol-info 
> *Cc: *Waqar Ahmad 
> *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/
> [image:
> 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
>
>


-- 
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

Re: [Hol-info] Extension of Co-algebraic Datatype

[Michael.Norrish]

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 
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Sunday, 6 May 2018 at 11:58
To: hol-info 
Cc: Waqar Ahmad 
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