The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Here is another example for mixed induction-coinduction:  Guarded
recursive types.  Agda snippet:

mutual
  data Ty {i : Size} : Set where
    _×?_ : ? (a b : Ty {i}) ? Ty {i}
    _??_ : ? (a b : Ty {i}) ? Ty {i}
    ??_  : ? (a? : ?Ty {i}) ? Ty {i}

  record ?Ty {i : Size} : Set where
    coinductive
    constructor delay_
    field       force_ : ?{j : Size< i} ? Ty {j}

?? : ?{i} ? (?{j : Size< i} ? ?Ty {j} ? Ty {j}) ? ?Ty {i}
force (?? F) = F (?? F)

Cheers,
Andreas

On 28.03.2014 17:02, Jean-Baptiste Jeannin wrote:
> Hi all,
> 
> Thanks for your answers. Thorsten's solution is exactly what we
> were looking for. Abhishek's solution is an interesting alternative
> where the inductive constructors can only appear finitely many
> times along each path.
> 
> Thanks, Jean-Baptiste
> 
> On Mar 28, 2014, at 8:28 AM, Dexter Kozen wrote:
> 
>> Hi Thorsten, That's  exactlly what we wanted, except instead of
>> 'gets' and 'puts' we have something else, but we wanted exactly
>> that behavior. Thanks! Dexter
>> 
>> On Mar 28, 2014, at 6:48 AM, Altenkirch Thorsten
>> <psztxa AT exmail.nottingham.ac.uk>
>>  wrote:
>> 
>>> There are many examples of inductive – coinductive definitions.
>>> My favorite one is Stream processors:
>>> 
>>> data SP (I O : Set) : Set where
>>> 
>>> get : (I -> SP I O) -> SP I O put : O -> \infty (SP I O) -> SP
>>> I O
>>> 
>>> The idea is that you can have only finitely many gets between
>>> any two puts but you can have infinitely many puts. In Agda you
>>> can achieve this by simply putting the \infty symbol in front
>>> of the recursive occurrence of the type. In Coq that can be
>>> achieved by a hack by Tarmo Uustalu and Keiko Nakata.
>>> 
>>> Hence in Agda your type could be translated as
>>> 
>>> data even_list : Set data odd_list : Set
>>> 
>>> data even_list where ENil : even_list ECons : nat -> odd_list
>>> -> even_list
>>> 
>>> data odd_list : Set OCons : nat -> \infty even_list ->
>>> odd_list.
>>> 
>>> However, in a way this is a bad example because it doesn't
>>> really matter wether one or both constructors are coinductive.
>>> 
>>> 
>>> Cheers, Thorsten
>>> 
>>> See
>>> 
>>> Subtyping, Declaratively - An Exercise in Mixed Induction and
>>> Coinduction 
>>> http://www.cs.nott.ac.uk/~txa/publ/danielsson-altenkirch-subtyping.pdf
>>>
>>>
>>> 
Termination Checking Nested Inductive and Coinductive Types
>>> http://www.cs.nott.ac.uk/~txa/publ/InvertedQuantifiers.pdf
>>> 
>>> 
>>> From: Jean-Baptiste Jeannin 
>>> <jeannin AT cs.cornell.edu>
>>>  Reply-To:
>>> "coq-club AT inria.fr"
>>>  
>>> <coq-club AT inria.fr>
>>>  Date: Thu, 27 Mar 2014
>>> 18:55:46 +0000 To: 
>>> "coq-club AT inria.fr"
>>>  
>>> <coq-club AT inria.fr>
>>>  Cc:
>>> Dexter Kozen 
>>> <kozen AT cs.cornell.edu>,
>>>  Konstantinos Mamouras
>>> <mamouras AT cs.cornell.edu>
>>>  Subject: [Coq-Club] Mixing Inductive
>>> and CoInductive constructors/destructors in the same type
>>> 
>>>> Hi,
>>>> 
>>>> I am trying to define a type with both inductive constructors
>>>> and coinductive constructors (really destructors).
>>>> 
>>>> With the [Inductive] keyword, I can define a type with all
>>>> constructors inductive, as in:
>>>> 
>>>> Inductive list: Type:= | LNil : list | LCons : nat -> list ->
>>>> list.
>>>> 
>>>> and similarly with the [CoInductive] keyword, I can define a
>>>> type with all constructors coinductive, as in:
>>>> 
>>>> CoInductive stream : Type := | SCons : nat -> stream ->
>>>> stream.
>>>> 
>>>> If I want some constructors to be inductive and others to be
>>>> coinductive, an idea I had was to use two mutually recursive
>>>> types, with a construct akin to:
>>>> 
>>>> CoInductive even_list : Set := | ENil : even_list | ECons :
>>>> nat -> odd_list -> even_list with odd_list : Set := | OCons :
>>>> nat -> even_list -> odd_list.
>>>> 
>>>> But I can't seem to make odd_list just [Inductive], while
>>>> keeping even_list [CoInductive]. Is there any way I could do
>>>> this? Or any other way to mix Inductive and CoInductive
>>>> constructors?
>>>> 
>>>> (examples taken or inspired from
>>>> http://adam.chlipala.net/cpdt/html/Coinductive.html and
>>>> http://adam.chlipala.net/cpdt/html/InductiveTypes.html) Thank
>>>> you, Jean-Baptiste
>>> 
>>> This message and any attachment are intended solely for the
>>> addressee and may contain confidential information. If you have
>>> received this message in error, please send it back to me, and
>>> immediately delete it.   Please do not use, copy or disclose
>>> the information contained in this message or in any attachment.
>>> Any views or opinions expressed by the author of this email do
>>> not necessarily reflect the views of the University of
>>> Nottingham. This message has been checked for viruses but the
>>> contents of an attachment may still contain software viruses
>>> which could damage your computer system, you are advised to
>>> perform your own checks. Email communications with the
>>> University of Nottingham may be monitored as permitted by UK
>>> legislation.
>>> 
>> 
> 
> 


- -- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel AT gu.se
http://www2.tcs.ifi.lmu.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iEYEARECAAYFAlM4IkwACgkQPMHaDxpUpLNbzwCeP4AaHuDuH9MHS3GCI8g/JZHs
9Q4AoL2gX73NB1cMqQRC6rMoo8c531Ke
=xqLc
-----END PGP SIGNATURE-----