@@ -35,11 +35,11 @@ func Mul(m Numeral) Term {
35
35
}
36
36
37
37
/*
38
- Kleene's trick:
38
+ Kleene's trick:
39
39
40
- Let's define incStep(N) as Nth iteration of { Pair _ n |-> Pair n (Inc n) },
41
- so it maps (Pair `0` `0`) to (Pair ( `N-1` f) ( `N` f) ), and the left side
42
- of N(incStep)(Pair 0 0 ) is "decremented" N
40
+ Let's define incStep(N) as Nth iteration of { Pair _ n |-> Pair n (Inc n) },
41
+ so it maps (Pair `0` `0`) to (Pair `N-1` `N`), and the left side
42
+ of N(incStep)(Pair `0` `0` ) is "decremented" N
43
43
*/
44
44
func incStep (p Term ) Term {
45
45
return Pair (Right (p ))(Inc (Right (p )))
@@ -79,37 +79,25 @@ func Sub(m Numeral) Term {
79
79
80
80
So, if a solution exists, Div is a fixed point of genDiv
81
81
combinator. To find a fixed point, we can use powerful
82
- tool Y-combinator:
82
+ tool Y-combinator (see y_comb.go) :
83
83
84
- YComb == (\x.\y.y(xxy))(\x.\y.y(xxy))
84
+ yComb == (\x.\y.y(xxy))(\x.\y.y(xxy))
85
85
86
86
For any combinator F:
87
87
88
- YComb F = (\x.\y.y(xxy)) (\x.\y.y(xxy)) F
89
- = F((\x.\y.y(xxy)) (\x.\y.y(xxy)) F)
90
- = F(YComb F)
88
+ yComb F = (\x.\y.y(xxy)) (\x.\y.y(xxy)) F
89
+ = F((\x.\y.y(xxy)) (\x.\y.y(xxy)) F)
90
+ = F(yComb F)
91
91
92
92
(if you don't understand the first transition, just
93
93
substitute (\x.\y.y(xxy)) as x and F as y into the first
94
94
closure).
95
95
96
96
So, now we have a formula for Div:
97
97
98
- Div == YComb (\G . Less(m, n) Zero Inc(G (Sub m n) n))
98
+ Div == yComb (\G . Less(m, n) Zero Inc(G (Sub m n) n))
99
99
*/
100
100
101
- // yCombPart == (\x.\y.y(xxy))
102
- func yCombPart (x Term ) Term {
103
- return func (y Term ) Term {
104
- return y (x (x )(y ))
105
- }
106
- }
107
-
108
- // YComb == (\x.\y.y(xxy))(\x.\y.y(xxy))
109
- func YComb (g Term ) Term {
110
- return (yCombPart )(yCombPart )(g )
111
- }
112
-
113
101
// genDiv G == Less(m, n) Zero Inc(G (Sub m n) n)
114
102
func genDiv (g Term ) Term {
115
103
return func (m Numeral ) Term {
@@ -119,9 +107,9 @@ func genDiv(g Term) Term {
119
107
}
120
108
}
121
109
122
- // div == YComb genDiv
110
+ // div == yComb genDiv
123
111
func div (m Numeral ) Term {
124
- return YComb (genDiv )(m )
112
+ return yComb (genDiv )(m )
125
113
}
126
114
127
115
var _ = div // unfortunately, it does not actually work :(
@@ -133,7 +121,7 @@ var _ = div // unfortunately, it does not actually work :(
133
121
// overflow callstack (because go runtime
134
122
// evaluates all arguments before apply).
135
123
//
136
- // Test for this function does not check YComb
124
+ // Test for this function does not check yComb
137
125
// trick, but it checks recursive formula.
138
126
func Div (m Numeral ) Term {
139
127
return func (n Term ) Numeral {
0 commit comments