Syllabus
Introduction. Schoenfinkel combinatorial calculus. Combinatorial objects as representants of single-parameter functions. Representation of multiple-parameter functions. Abstraction of variables and unknowns. Combinatorial completeness of calculus. Calculus consistency. Church-Rosser property.
Lambda calculus, informal description. Variables, free and bound, abstraction bounded and unbounded. Lambda objects in normal form. Church-Rosser property and uniformity of lambda objects in normal form.
Lambda calculi. Syntactic description of lambda objects, free and bound variables, alpha and beta reduction. Extensions of lambda calculus, extensionality, delta rule.
Conversion, application, abstraction. Lambda terms, combinators. Fixed-point theorems.
Representation of computable functions. Numerals, boolean constants, tuples.
Representability of (total) recursive functions by lambda terms.
Consistency of combinatorial calculi and lambda calculi. Church-Rosser property and calculi consistency. Objects without normal form. Paradoxes. Combinatorial logic and predicate logic: Curry paradox.
Functional programming and lambda calculus. Computational model of functional language, reduction, normal forms and functional programming, controlling of computation in functional programming. Strict functions.
Typed lambda calculus. Extension of lambda calculus language with object types.
Motivation for introduction of types: partial correctness of programs, effectivity of computations. Type variables and value assignment to type variables. Curry and Church type systems.
Annotation
Combinatorial calculi and lambda calculi, untyped calculi, representability of recursive functions,
Church Rosser property and consistency of lambda calculus, typed lambda calculi, functional programming constructs