When1: 1941
When2: 1956
Who: Alonzo Church [Church, Alonzo]
What: mathematician
Where: USA
works\ Calculi of Lambda-Conversion [1941]; Introduction to Mathematical Logic [1944 and 1956]
Detail: He lived 1903 to 1995, studied denotation, and helped develop quantum logic. Symbol strings can represent numbers and functions. Using functions on input function and data strings makes output function and data strings {lambda calculus, Church}. Lambda acts on variable or function, or variable and function combination, which is second-function dummy variable: lambda(x(f(x))) = f, lambda(x(f(x)))(a) = f(a), lambda(f(f(f(x)))) = lambda(f(lambda(x)(f(f(x))))) = lambda(f(x)(f(f(x)))). This expression is a function and precedes a value, which substitutes into function. In particular, after lambda, expressions can have variable zero times, function of variable one time, function of function of variable two times, and so on: 0 = lambda(f(x)(x)), 1 = lambda(f(x)(f(x))), 2 = lambda(f(x)(f(f(x)))). Function of function equals lambda and function of function {abstraction, lambda calculus}: f(f(x)) = lambda(x)(f(f(x))). Really, symbols are functions. Lambda calculus represents recursion, iteration, and algorithm loops. Recursive functions can be equation sets. Recursive functions are computable {Church's theorem}. Functions are computable if they are recursive {Church's thesis, recursion}. Recursive functions can be lambda calculus. Lambda calculus is equivalent to Post grammar and Turing machine and so can express all algorithms. LISP computer language depends on lambda calculus.
Epistemology
Formal systems can prove most theorems {effectively calculable} {computability}. Lambda calculus shows that it is impossible to prove some valid theorems in most formal systems, including arithmetic.
Mathematical Sciences>Mathematics>History>Logic
Outline of Knowledge Database Home Page
Description of Outline of Knowledge Database
Date Modified: 2022.0224