proving that simply typed lambda calculus terminates using SKI combinators
I want to prove that simply typed lambda calculus (STLC) is strongly normalizing. I had the following idea for how to do it:
- show that any expression in STLC can be expressed using just simply typed SKI combinators.
- show by induction that any expression in the above form is strongly normalizing.
Would this work?
Posted Nov 1, 2025, 11:56 PM UTC
82