The Coq mailing list

[Andreas Abel <abela AT chalmers.se>]

Sorry, EnigMail destroyed the unicode characters... Trying again.

mutual
  data Ty {i : Size} : Set where
    -- 1̂   : Ty {i}
    -- _+̂_ : ∀ (a b : Ty {i}) → Ty {i}
    _×̂_ : ∀ (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}
open ∞Ty public

-- Guarded fixpoint types (needs sized types)

μ̂ : ∀{i} → (∀{j : Size< i} → ∞Ty {j} → Ty {j}) → ∞Ty {i}
force (μ̂ F) = F (μ̂ F)

On 30.03.2014 15:55, Andreas Abel wrote:
> 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/

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