File tree 1 file changed +2
-2
lines changed
content/lambda-calculus/lambda-definability
1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change 39
39
represents a function accepting two arguments $ f$ and $ x$ , and
40
40
returns $ f^n(x)$ . Church numerals are evidently in normal form.
41
41
42
- A represention of natural numbers in the lambda calculus is only
42
+ A representation of natural numbers in the lambda calculus is only
43
43
useful, of course, if we can compute with them. Computing with Church
44
44
numerals in the lambda calculus means applying a $ \lambd $ -term~$ F$ to
45
45
such a Church numeral, and reducing the combined term~$ F\, \num n$ to
48
48
of the computation as being the number~$ m$ . We can then think of~$ F$
49
49
as defining a function $ f\colon \Nat \to \Nat $ , namely the function
50
50
such that $ f(n) = m$ iff $ F\, \num n \red \num m$ . Because of the
51
- Church-Rosser property, normal forms are unique if they exist. So if
51
+ Church-- Rosser property, normal forms are unique if they exist. So if
52
52
$ F\, \num n \red \num m$ , there can be no other term in normal form,
53
53
in particular no other Church numeral, that $ F \, \num n$ reduces to.
54
54
You can’t perform that action at this time.
0 commit comments