[Agda] Re: strict unit type

[Andreas Abel]

On 30.04.12 3:01 PM, Vladimir Voevodsky wrote:
> Thanks for a detailed explanation!
>
> I guess the problem with expansion instead of reduction is that it is
> non-terminating (e.g. in the case of dependent sums or lambda's) and
> the condition that one is allowed to apply expansion only once, it
> seems to me, should complicate rigorous meta-theory a lot.

Yes, this is why one moves eta into the equality check rather than doing 
reduction or expansion.  For the method, see, e.g.

   On Irrelevance and Algorithmic Equality in Predicative Type Theory
   http://www2.tcs.ifi.lmu.de/~abel/types10.pdf

> PS There is another non-confluent situation with a ->  tt for a : Pt
> which does not require dependent sums namely \lambda x:T, f x where f
> : T ->  Pt reduces both to f and to \lambda x:T tt . Both
> non-confluences can be taken care of by additional reductions in
> particular the reduction \prod x:T, Pt ->  Pt for the example with
> \lambda.

Such a reduction is unhealthy except in the situation where \prod is a 
"for all" that does not leave marks on the term level.

Cheers,
Andreas

> On Apr 29, 2012, at 5:36 PM, Guillaume Brunerie wrote:
>
>> 2012/4/29 Vladimir Voevodsky<vladimir at ias.edu>:
>>>
>>> On Apr 29, 2012, at 12:36 PM, Guillaume Brunerie wrote:
>>>
>>>>>>> I wonder if any one has considered type theories where Pt
>>>>>>> is introduced as having a distinguished object tt
>>>>>>> together with reduction rules of the following form (in
>>>>>>> the absence of dependent sums, otherwise one needs
>>>>>>> more):
>>>>>>>
>>>>>>> 1. any object of Pt other than tt reduces to tt,
>>>>>>
>>>>>> This is just the eta-expansion rule for Pt. For example
>>>>>> Agda has it if you implement Pt as a record. You only need
>>>>>> this (and beta/iota reduction) for (Pt) to be terminal in
>>>>>> the category of contexts (it will be isomorphic to the
>>>>>> empty context).
>>>>>
>>>>> I wonder how it works in Agda. This reduction for the unit
>>>>> type creates non-confluet situation when combined with
>>>>> iota/eta reduction for dependent sums. Additional reductions
>>>>> are needed to recover confluence. Are they implemented in
>>>>> Agda?
>>>>
>>>> Do you have an example of a problematic situation? By the way,
>>>> I am far from a specialist in Agda, but perhaps that
>>>> normalization is implemented with something like normalization
>>>> by evaluation, which does not require confluence (I think).
>>>
>>> For c: \sum x : Pt, Y the term [pair]([pr1](c), [pr2](c)) reduces
>>> both to c and to [pair](tt, [pr2](c)) and these two terms can not
>>> be reduced to a common term unles a special reduction rule is
>>> introduced for this.
>>>
>>> V.
>>
>> Eta-conversion is usually seen as an expansion rule, it’s c that
>> "reduces" to [pair]([pr1](c), [pr2](c)) and not the other way
>> around. In your example, everything reduces to [pair](tt, [pr2](c))
>> and there is no problem of confluence. Do you have another example
>> which would still be a problem with this eta-expansion rule?
>>
>> Similarly, for functions the eta-expansion rule reduces f to
>> \lambda x . f x (you have to make sure that f has not already been
>> eta-expanded, I don’t remember exactly how). This makes sense
>> because the purpose of eta-expansion is to convert terms to
>> canonical inhabitants of their type. A canonical inhabitant of Pt
>> is tt, so eta-expansion convert u : Pt to tt, a canonical
>> inhabitant of \sum x : A, P x is a pair, so eta-expansion expands
>> a term into a pair, and a canonical inhabitant of a function type
>> is a \lambda abstraction. Also, normalization by evaluation always
>> gives beta-reduced eta-expanded normal forms.
>>
>> I’m not sure how Agda works, though. I tried a few things, and in
>> the context (u : unit), the normal form of u is u, but refl u is
>> nevertheless accepted as an inhabitant of the identity type Id unit
>> u tt, so it seems that convertibility is not defined as equality
>> of normal forms in Agda.
>>
>> Guillaume
>
> _______________________________________________ Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/