Lambda Calculus with Elementary Type Theory
8/23/21
The Lambda Calculus that we have been looking at in Lambda Calculus and Combinatory Logic has been the untyped Lambda Calculus. It is plenty interesting for sure, being able to provide a foundation for computability, programming languages, and many areas of linguistics and philosophy. But untyped Lambda calculus also has some features to be wary of; for example, some reduction sequences go on forever and never reduce the expression to a normal form.