[Agda] Re: strict unit type

Andreas Abel andreas.abel at ifi.lmu.de
Mon Apr 30 15:23:28 CEST 2012

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

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


> 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

More information about the Agda mailing list