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.

  • 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$ Commented Jan 5, 2023 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$ Commented Jan 5, 2023 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$ Commented Jan 5, 2023 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.
    Commented Jan 5, 2023 at 22:01
  • $\begingroup$ Oh hey I wrote something on this almost 8 years ago! mathoverflow.net/a/206529/36103 $\endgroup$
    – cody
    Commented Jan 23, 2023 at 18:19


Your Answer

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