[Agda] Termination proof in partiality monad

[Anton Setzer]

Nils Anders Danielsson wrote:
> On 2008-11-19 10:24, Dan Doel wrote:
>>
>> Is it possibly a bug of some sort?
>
> Yes, Agda currently lacks subject reduction (as does Coq). See
> http://thread.gmane.org/gmane.comp.lang.agda/226 and
> http://pauillac.inria.fr/pipermail/coq-club/2008/003675.html.
>
> Thorsten thinks he knows how to fix this (using one of Thierry's ideas):
> http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=104.
>
I repeat the first file linked above:

> Hi,
>
> The current implementation of codata seems to be a bit problematic.
> The following program was suggested by Nicolas Oury:
>
>   data _≡_ {a : Set} (x : a) : a -> Set where
>     refl : x ≡ x
>
>   codata Stream : Set where
>     cons : Stream -> Stream
>
>   out : Stream -> Stream
>   out (cons xs) = cons xs
>
>   out-≡ : (xs : Stream) -> xs ≡ out xs
>   out-≡ (cons xs) = refl
>
>   ω : Stream
>   ω ~ cons ω
>
>   p : ω ≡ cons ω
>   p = out-≡ ω
>
> If we evaluate p we get refl, but if we replace the right-hand side of
> p with refl we get a type error, so we do not have preservation of
> types.
>
>   
The problem is that there are two different forms of cons, which
are identified in Agda:

- There is cons which forms the shapes of elements of Stream
  If a: Stream, then if one applies the * operator suggested by
  me and others to it, we obtain an element
  of the form (cons a' l')
  This element should not be an element of Stream but an element
  of a type Stream_Shape with the definition
 
  data Stream_Shape : Set where
    cons : Stream -> Stream

- There is cons' which is a defined element of Stream which has
  shape cons
  cons' is defined by course of guarded recursion using the defintion

  cons' : Stream -> Stream
  (cons' l) * = cons l

 
 
If we distinguish cons and cons' we obtain


out : Stream -> Stream
out x = case (x *) of
        (cons xs) -> cons' xs

out-≡ : (xs : Stream) -> xs ≡ out xs
out-≡ x  = case (x *) of
        (cons xs) -> {! !}

where the type of the goal is
x ≡  cons' xs

which is not inhabited by refl, since
x is not definitionally equal to cons' xs, but is an element
which if we apply * to it has the form (cons xs)

If x was defined as cons' xs, then refl is an element
of   x ≡  cons' xs
If x x was defined differently (e.g. as ω)
it is not definitially  equal to cons xs, and therefore
x ≡  cons' xs
 is not inhabited by  refl.

I think the use of codata is a historic accident, which we
should get rid off. Maybe the best is to throw codata in the bin,
and have a nice fresh start.


Anton


 
-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------