[Agda] Re: strict unit type
Andreas Abel
andreas.abel at ifi.lmu.de
Tue May 1 09:51:01 CEST 2012
On 30.04.12 3:36 PM, Vladimir Voevodsky 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.
I agree that this can likely be modeled, i.e., terms and types can be
interpreted in a way that these reductions become identities.
Partially, this is done in Werner et al.'s proof irrelevant model of the
CIC.
However, I am not so convinced that reduction is the right method in
this case. For instance, subject reduction fails unless you work on
equivalence classes of types. A more "semantic" approach seems more
fitting, from my experience. Also, from the implementor's perspective
such reductions complicate the picture. For instance, the problem
tt : \prod x:T. Y(x) with Y a meta-variable
cannot be decided at the spot, but has to wait for the solution of Y.
Also, then a term has many types, which makes type inference more
complicated.
In Agda, if you have to supply a term of type \prod x:T. Pt, you can
always just write _ (for a fresh meta-variable). Eta-expansion then
fills in the term for you
_ --> \x:T. _ --> \x:T. tt
That seems to do the job.
> 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.
I agree, this is why I have been working on (proof) irrelevance for Agda.
Cheers,
Andreas
--
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/
More information about the Agda
mailing list