Lambda Calculus Synopsis
Apr. 3rd, 2013 09:06 amhttp://arxiv.org/abs/1304.0558
This text gives a rough, but linear summary covering some key definitions, notations, and propositions from Lambda Calculus: Its Syntax and Semantics, the classical monograph by Barendregt. First, we define a theory of untyped extensional lambda calculus. Then, some syntactic sugar, a system of combinatory logic, and the fixed point theorem are described. The final section introduces a topology on the set of lambda terms which is meant to explain an illusory contradiction. Namely, functions defined on the set of lambda terms are in the set of lambda terms itself, the latter being a countable set. However, the functions on the set of lambda terms appear to be continuous with respect to a topology of trees.
This text gives a rough, but linear summary covering some key definitions, notations, and propositions from Lambda Calculus: Its Syntax and Semantics, the classical monograph by Barendregt. First, we define a theory of untyped extensional lambda calculus. Then, some syntactic sugar, a system of combinatory logic, and the fixed point theorem are described. The final section introduces a topology on the set of lambda terms which is meant to explain an illusory contradiction. Namely, functions defined on the set of lambda terms are in the set of lambda terms itself, the latter being a countable set. However, the functions on the set of lambda terms appear to be continuous with respect to a topology of trees.
