0
$\begingroup$

For any 2 strongly normalizing terms in the simply typed Lambda Calculus, s and t, is st also strongly normalizing? And why? I'm a bit confused as this is used in a proof regarding strong normalization and the typable lambda calculus, but I have not been able to show that this is the case. Any help would be much appreciated.

Improve this question
$\endgroup$
5
  • 2
    $\begingroup$ In the untyped λ-calculus, this is is of course not the case. The self-application term λx.xx is SN but applied to itself this gives the canonical non-terminating term. But given what you write, I wonder whether you ask about this property for the simply typed λ-calculus? It has the property but this is not how the proof of SN for it proceeds. Could you clarify? $\endgroup$
    – Henning Basold
    Jan 5 at 14:11
  • $\begingroup$ Yes actually, that is correct - for typable Lambda Calculus terms, how do you prove application preserves the strongly normalizing property? $\endgroup$
    – Abhishek Manikandan
    Jan 5 at 15:45
  • 5
    $\begingroup$ Proving that application preserves SN is the hard part. Given the exact correspondence between type theories and logics know as Curry-Howard correspondence, this must be hard by Gödel's 2nd incompleteness theorem. The standard technique used in SN proofs is called reducibility candidates. Maybe people.mpi-sws.org/~dg/teaching/pt2012/gallier.pdf is a place to look? $\endgroup$
    – Martin Berger
    Jan 5 at 18:56
  • $\begingroup$ Cross-posted: cstheory.stackexchange.com/q/52349/5038, cs.stackexchange.com/q/156607/755. Please do not post the same question on multiple sites. $\endgroup$
    – D.W.
    Jan 5 at 22:01
  • $\begingroup$ Oh hey I wrote something on this almost 8 years ago! mathoverflow.net/a/206529/36103 $\endgroup$
    – cody
    Jan 23 at 18:19

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.