[Agda] Re: [TYPES] strict unit type

[Altenkirch Thorsten]

On 10/05/2012 00:04, "Vladimir Voevodsky" <vladimir at ias.edu> wrote:

>
>On May 1, 2012, at 5:24 AM, Altenkirch Thorsten wrote:
>
>> 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).
>
>Why just after beta reduction and not say iota-reduction or even some
>internal eta-reduction?

When I say beta I also mean beta for product and inductive types. The Coq
people seem to call this iota reduction.

What do you mean by internal eta-reduction.

Btw, I don't think you need to reduce under a lambda (which is also a form
of extensionality). So what I mean is to execute the purely computational
rules (these are the once used by any functional programming language).

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