[TYPES] decidability/confluence of beta-eta convertibility in Church-style STLC

[Altenkirch Thorsten]

Hmm, I thought it was you. :-)

Is this really the generalisation of NBE for simply typed lambda calculus
to dependent types we ought to expect?

I mean your construction involves PERs but the strong NBE for STL doesn't.
Maybe because you do it for an impredicative system.

Is there a PER-free version if we don't have impredicativity?
Or the other way around: How would the STL version of your construction
look like?

In my view the main ingredient of NBE is the observation that the presheaf
model for the simply typed lambda calculus is equivalent to the initial
model (interpreting base types syntactically). Indeed it is a
proof-relevant generalisation of the completeness proof for Kripke models.

I would expect that the same holds for dependent types.

Thorsten

On 16/08/2012 13:22, "Andreas Abel" <andreas.abel at ifi.lmu.de> wrote:

>On 14.08.2012 11:13, Altenkirch Thorsten wrote:
>> [ The Types Forum,
>>http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> An alternative are semantic methods, I.e. normalisation by evaluation.
>> There is a weak version for combinatory logic which can be used to only
>> implement beta reduction (but not xi or eta rules) or a strong one which
>> does give you full beta eta equality. However, to extend strong NBE for
>> more complex systems can be quite tricky too. I don't think I have seen
>>a
>> straightforward extension of the strong version to dependent types (I am
>> saying this expecting somebody to scream :-).
>
>Yes, me!
>
>Towards Normalization by Evaluation for the Calculus of Constructions
>     Andreas Abel
>     Tenth International Symposium on Functional and Logic Programming,
>FLOPS 2010, 19-21 April 2010, Sendai, Japan © Springer.
>
>   http://www2.tcs.ifi.lmu.de/~abel/publications.html#flops10
>
>With computation on the type-level, it does not get much more
>straightforward...
>
>Cheers,
>Andreas
>
>> Another idea which James Chapman and I have investigated is to directly
>> prove that the natural implementation of a decision procedure using big
>> step semantics is correct. This also has the advantage that you actually
>> prove the correctness of the implementation. This has been written up in
>> James PhD and there is also a journal paper - see
>> http://www.cs.nott.ac.uk/~txa/publ/jtait07.pdf
>>
>> Cheers,
>> Thorsten
>>
>
>
>-- 
>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/

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.