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


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.