[Agda] Re: [TYPES] strict unit type

[Altenkirch Thorsten]

In general we shouldn't expect to decide eta equality by untyped
reduction. eta equality isa form of decidable extensionality and does not
correspond well to computation to a normal form.

Clearly, the case of the unit type shows that we need to know the type to
check equality.

Trying to decide eta equalities by reduction is very non-modular. This is
basically the point of Vladimir's email.

However, if we implement it as a type directed decision procedure things
are much better. E.g. to terms f,g : Pi x:A.B x are convertible if f x and
g x : B x are convertible (whewre x is a fresh variable) after beta
reduction. Similarily, two terms p,q : Sigma x:A.B x are convertible if
p.1 and q.1 : A are convertible after beta reduction and p.2 and q.2 : B
p.1 (or B q.1) are convertible after beta reduction. (The and here has to
be read sequentially, and the choice B p.1 or B p.2 actually causes some
technical problems).

This is also modular, because we can implement the equality for one type
without having to rethink the equalities at other types.

Thorsten



On 01/05/2012 04:10, "Frederic Blanqui" <frederic.blanqui at inria.fr> wrote:

>[ The Types Forum,
>http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>
>
>Le 30/04/2012 21:04, Vladimir Voevodsky a écrit :
>> On Apr 29, 2012, at 8:27 PM, Frederic Blanqui wrote:
>>
>>> [ The Types Forum,
>>>http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>>
>>> Hello Vladimir.
>>>
>>> Le 29/04/2012 22:10, Vladimir Voevodsky a écrit :
>>>> [ The Types Forum,
>>>>http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>>>
>>>> Hello,
>>>>
>>>> let Pt be the unit type ("one point"). In Coq-like systems it is
>>>>introduced through an eliminator and the associated iota-reduction
>>>>rule. This is in practice sufficient for proving all its expected
>>>>properties modulo propositional equality (or identity types) but does
>>>>not create a terminal object in the category of contexts.
>>>>
>>>> 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 has been done already with this reduction rule. Please, check the
>>>work of Roberto Di Cosmo and Delia Kesner for instance.
>>>
>>>> 2. Prod x : T , Pt reduces to Pt,
>>>>
>>>> 3. Prod x : Pt , T reduces to T.
>>> On the other hand, I am not sure that these rules have been considered
>>>yet since, by doing so, you may well loose the property that reduction
>>>preserves typing: if t : T reduces to u, then u : T (a property often
>>>called "subject reduction"). Unless perhaps if you consider the
>>>following extra rules:
>>>
>>> 2'. (\lambda x:T. t) reduces to tt if t : Pt,
>>>
>>> 3'. (\lambda x:Pt, t) reduces to t{x=tt}.
>> Yes, I did. But also this would follow from the previous 3 rules. For
>>example  (\lambda x:T. t) for t:Pt will have the type, in normal form,
>>Pt and therefore will be reducible to tt by the first reduction.
>>
>> Vladimir.
>>
>>
>>
>Yes, 2' is a consequence of 2 & 1. But I do not see why 3' is a
>consequence of the other rules. By 1, you have (\lambda x:Pt. t) reduces
>to (\lambda x:Pt. t{x=tt}). Then, how to remove (\lambda x:Pt)?
>
>But, after all, it may not be necessary to consider this extra rule. I
>was thinking that having term-level rules corresponding to your
>type-level rules could help, but I am not sure anymore. It may well work
>fine to consider types up to your equivalence relation.
>
>On the other hand, there is a little problem with rule 3 in case x
>occurs free in T. You should instead consider:
>
>3. (Prod x:Pt, T) reduces to T{x=tt}.
>
>Frederic.
>

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.