The Lambda Calculus, part 1 2 Applied lambda calculi; the simply typed lambda calculus

The first paragraph introduces the concept of applied lambda calculus, highlighting its evolution from pure lambda calculus. It explains that pure lambda calculus, consisting of variables, abstractions, and applications, is a universal model of computation equivalent to Turing machines. The speaker then discusses the rationale behind adding constants as primitives to the lambda calculus, which is the basis of applied lambda calculus. The paragraph also touches on the idea of extending semantics with constants and the concept of an 'apply' function, setting the stage for a more in-depth discussion on type systems and their origins in logic.

In this segment, the speaker delves into the purpose and utility of type systems, which classify programs into well-typed and not well-typed categories. Type systems are integral in programming languages, serving as a pre-processing step for type checking. The speaker explains the necessity for type systems to be effective, meaning there must be an algorithm to determine if a program is well-typed. The distinction between type checking and type inference is also clarified, with the latter being a central feature in languages like Haskell and ML, which attempt to deduce the type of a program rather than requiring explicit type information.

The third paragraph presents the syntax of the simply typed lambda calculus, which includes variables, abstractions, applications, and additional constructs like pairs, conditionals, and local declarations. The speaker emphasizes that these constructs are essentially constants in the lambda calculus. The semantics of the calculus are discussed, focusing on small-step semantics and value transitions. The rules for function application, including beta reduction and constant application, are introduced, illustrating how expressions evolve in the calculus.

This paragraph explores the type system of the simply typed lambda calculus, starting with the definition of types such as 'int', 'bool', and arrow and product types. The speaker discusses the role of a type environment, which is a partial function assigning types to variables within an expression. Type judgments are then defined, explaining how types are assigned to different syntactic elements of the language using a set of type rules. The speaker provides examples of type rules for variables, pairs, functions, applications, and conditionals, illustrating how type safety is ensured in the calculus.

The fifth paragraph introduces the concept of recursive definitions in the simply typed lambda calculus, allowing for the creation of recursive functions through 'let rec' expressions. The semantics for these recursive definitions are explained, showing how the definition of a function can be substituted within its own body to achieve recursion. The type rule for 'let rec' is also discussed, ensuring that the type of the recursive definition matches the type of the body of the function. The speaker emphasizes the importance of type safety in avoiding undefined operations, such as applying 'plus' to non-numeric values.

The final paragraph discusses two key results related to the type system of the simply typed lambda calculus: type preservation (subject reduction) and strong normalization. Type preservation ensures that well-typed programs remain well-typed throughout evaluation, while strong normalization guarantees that well-typed, recursion-free expressions will always terminate and reach a normal form. The speaker notes that these properties are desirable in any type system and highlights the limitations of the simply typed lambda calculus, suggesting a continuation of the discussion in future parts of the presentation.