July 3, 2007

Lambda calculus

	core programming language, turing-equivalent

	syntax

	free & bound vars
	substitutions (very similar to those seen in unification)

	equivalence as a proof system (derivation rules)

	alpha-equivalence
	beta-equivalanece
	eta-equivalence

	order of evaluation
		normal order (call by name)
		eager/strict (call by value)
		nonstrict--accomplishes same result as normal order

	church-rosser/confluence

	encodings
		booleans
			true
			false
			not
			and
		pairs
			construct
			first
			second
		naturals
			zero
			succ
			add
			fold/primitive recursion

	combinators
		Y
		S, K, I
		mention combinatory logic as equivalent to LC, don't go into it

	infinite loop

	simply-typed lambda calculus
		type expressions
		not turing-complete/can't expression nontermination
			even with parametric polymorphism
		need for a built-in let rec or Y