[Agda] Re: strict unit type
Vladimir Voevodsky
vladimir at ias.edu
Mon Apr 30 15:36:52 CEST 2012
On Apr 30, 2012, at 9:23 AM, Andreas Abel wrote:
>> 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.
Well, that was my first thought as well but I am not so sure now. It does make it necessary to do some type checking before beta-reduction but anyhow the reduction such as a -> tt for objects of the unit type makes reduction context dependent. I have not checked all the details yet but it is possible that one can preserve confluence and normal form and still have reductions which change the sum/prod-structure of type expressions.
Vladimir.
PS From the point of view of a user who wants to construct/verify proofs the more identifications are recognized by the underlying system the better.
More information about the Agda
mailing list