Mathematical logic seminar - November 11, 2014

Time: 12:30 - 13:30

Room: Wean Hall 8220

Speaker:     Rick Statman    
Department of Mathematics
CMU

Title: An introduction to λ-calculus

Abstract:

λ-calculus is that branch of logic which employs algebraic methods to study computer programs and the resulting computable functions. Conventional algebraic structures such as groups and fields are normally absent, and unconventional structures such as Cartesian monoids and near-rings take their place. The object is to classify computer programs and the functions they compute by their functional/algebraic properties such as typeability;

f: D -> R

and invariance;

P(f) = f.

The first lecture will give an introduction to λ-calculus à la Rocquencourt. The basic theorems of reduction and conversion will be discussed,including η-conversion,and the Schönfinkel-Curry theory of combinators will be introduced. The second lecture will describe several algebraic structures, including Cartesian monoids and near-rings, which occur in λ-calculus.