Lambda Calculus Study Notes

Syntax:
- Composed of variables, abstraction, and application.
- Abstraction: λx.M where x is a variable and M is a lambda term.
- Application: (M N) where M and N are lambda terms.
Semantics:
- Focuses on the meaning of lambda terms.
- Reduction: Process of simplifying terms using beta reduction (substituting arguments into abstractions).
- Normal Form: A term is in normal form if no more reductions can be applied.

Technique of representing data and operators in lambda calculus.
Numerals: Represent natural numbers as functions.
- Example: 0 = λf.λx.x, 1 = λf.λx.f x, 2 = λf.λx.f (f x), etc.
Boolean values: Represent true and false as functions.
- true = λx.λy.x, false = λx.λy.y.

A variant of lambda calculus without variables.
Uses combinators (higher-order functions) to achieve the same results.
Important combinators:
- K: K x y = x (constant function).
- S: S f g x = f x (g x) (application combinator).
Combinatory logic demonstrates that functional expression can be systematically represented without named variables.

Assigns types to lambda terms to enable safe and predictable usage.
Simply Typed Lambda Calculus: Introduces types to lambda calculus.
- Terms are assigned types, e.g., λx:τ. M where τ is the type of x.
Polymorphism: Allows functions to operate on any type.
- Example: The identity function λx.x can have any type.
Type Inference: Mechanisms to automatically deduce types without explicit annotations.

Influences functional programming languages like Haskell, Scheme, and ML.
Provides foundational concepts for:
- Function definitions and calls.
- Recursion and higher-order functions.
Type systems derived from lambda calculus are used to ensure code safety.
Enables reasoning about program behavior through formal semantics.
Underpins many modern programming paradigms, including functional, imperative, and object-oriented programming.

Lambda calculus consists of three main components: variables, abstraction, and application.
Abstraction is denoted as λx.M, where x represents a variable, and M is any lambda term.
Application is expressed as (M N), representing the application of lambda term M to term N.
Semantics pertains to the interpretation and meaning of lambda terms within the calculus.
Reduction involves beta reduction, which simplifies terms by substituting function arguments into abstractions.
A term reaches normal form when no further reductions are applicable, indicating it cannot be simplified any further.

Church encoding is a method for representing data and operators using lambda calculus.
Numerals are represented as higher-order functions, capturing natural numbers through functions:
- 0 is encoded as λf.λx.x
- 1 is encoded as λf.λx.f x
- 2 is λf.λx.f (f x), and so on for higher numbers.
Boolean values are also represented as functions:
- true is expressed as λx.λy.x
- false is λx.λy.y

Combinatory logic is a modified form of lambda calculus that operates without named variables.
It employs combinators, defined as higher-order functions that replace the need for variables.
Key combinators include:
- K: Represents constant function behavior with K x y = x.
- S: Defined as S f g x = f x (g x), serving as the application combinator.
This logic illustrates that functional expressions can be represented systematically through combinators alone.

Type systems assign types to lambda terms, enhancing safety and predictability in usage.
Simply Typed Lambda Calculus introduces types, with terms expressed as λx:τ.M, where τ indicates the type of x.
Polymorphism allows for functions to handle various types, exemplified by the identity function λx.x, which can operate on any type.
Type Inference mechanisms facilitate automatic type deduction, eliminating the need for explicit type annotations.

Lambda calculus has significantly influenced functional programming languages like Haskell, Scheme, and ML.
Core concepts from lambda calculus underpin function definitions, calls, recursion, and higher-order functions.
Type systems inspired by lambda calculus ensure program safety and correctness.
It enables formal reasoning about program behavior, providing a foundation for modern programming paradigms including functional, imperative, and object-oriented approaches.