<p>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.</p>

CC BY-SA 4.0
2023-01-05T14:11:24.533Z
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?
Henning Basold
CC BY-SA 4.0
2023-01-05T15:45:07.017Z
Yes actually, that is correct - for typable Lambda Calculus terms, how do you prove application preserves the strongly normalizing property?
Abhishek Manikandan
CC BY-SA 4.0
2023-01-05T18:56:48.630Z
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 https://people.mpi-sws.org/~dg/teaching/pt2012/gallier.pdf is a place to look?
Martin Berger
CC BY-SA 4.0
2023-01-05T22:01:42.120Z
Cross-posted: https://cstheory.stackexchange.com/q/52349/5038, https://cs.stackexchange.com/q/156607/755.  Please [do not post the same question on multiple sites](https://meta.stackexchange.com/q/64068).
D.W.
CC BY-SA 4.0
2023-01-23T18:19:34.987Z
Oh hey I wrote something on this almost 8 years ago! https://mathoverflow.net/a/206529/36103
cody
<lambda-calculus><typed-lambda-calculus><normalization>
Simple Lambda Calculus Question
Abhishek Manikandan
# Simple Lambda Calculus Question

(Asked by: username_0 on 2023-01-05)

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.

**Tags:** lambda-calculus, typed-lambda-calculus, normalization

> **Comments:**
> **username_1**: 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?  
> **username_0**: Yes actually, that is correct - for typable Lambda Calculus terms, how do you prove application preserves the strongly normalizing property?  
> **username_2**: 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 https://people.mpi-sws.org/~dg/teaching/pt2012/gallier.pdf is a place to look?  
> **username_3**: Cross-posted: https://cstheory.stackexchange.com/q/52349/5038, https://cs.stackexchange.com/q/156607/755.  Please [do not post the same question on multiple sites](https://meta.stackexchange.com/q/64068).  
> **username_4**: Oh hey I wrote something on this almost 8 years ago! https://mathoverflow.net/a/206529/36103  

---

## 0 answers

