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

[Andreas Abel]

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/