[Agda] Strangeness with corecursion

[James Wood]

Hi Thorsten,

This looks bad! Have you tried checking the following code (with the
second definition of |_*∞_|)?

|inf∞ : ℕ∞ prd∞ inf∞ = just inf∞ test : Is-nothing (prd∞ (inf∞ *∞
zero∞)) test = nothing |

The bug is not that the first definition is rejected; it’s that the
second definition is accepted. I can’t really say why it’s accepted, though.

Conat multiplication needs some other trick to make it productive. In
the test case, |n| is added to itself infinitely many times. If it’s a
successor, that’s okay because the consumer just gets infinitely many
successors. But if it’s 0, the consumer has to wait (forever) as to
whether the result is a zero or a successor.

Regards,

James

On 03/03/2019 12:16, Thorsten Altenkirch wrote:

> Hi,
>
>  
>
> I just set the exercise to define multiplication for conats for my
> course on type theory. So please don’t blurt put the solution – see
> the attached code. The following is not a solution because agda
> doesn’t see that the definition is productive (even though it is):
>
>  
>
> prd∞ (m *∞ n) with prd∞ m                                             
>
> prd∞ (m *∞ n) | (just pm) = prd∞ (n +∞ (pm *∞ n))
>
> prd∞ (m *∞ n) | nothing   = nothing
>
>  
>
> but after the following change
>
>  
>
> prd∞ (m *∞ n) with prd∞ m                                            
>
> prd∞ (m *∞ n) | (just pm) with (pm *∞ n)
>
> prd∞ (m *∞ n) | (just pm) | x = prd∞ (n +∞ x)
>
> prd∞ (m *∞ n) | nothing   = nothing
>
>  
>
> agda seems to accept is. Actually even if +∞ is not contractive.
>
>  
>
> Is this a known bug? Otherwise can somebody remind e how to report this?
>
>  
>
> Cheers,
>
> Thorsten
>
> 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 contact the sender and delete the email and
> attachment. 
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

​
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190303/6a5c55aa/attachment.html>