« first day (33 days earlier)    last day (14 days later) » 

Zgarb
Zgarb
08:40
@Qwerp-Derp Ping! You asked about the factorial in lambda calculus.
@Qwerp-Derp Ping again by reply, just in case.
Qwerp-Derp
Qwerp-Derp
09:12
@Zgarb Yup, I did ask that.
The Wikipedia example is just psuedocode and I don't understand how it uses the Y combinator and stuff
Zgarb
Zgarb
Do you know how to handle Booleans in LC?
I mean, do you know how to write G = λr. λn.(1, if n = 0; else n × (r (n−1))) as a lambda term?
Qwerp-Derp
Qwerp-Derp
Yup
Uhhh
Not really
Zgarb
Zgarb
Gotta go, I'll be back later.
Zgarb
Zgarb
10:13
@Qwerp-Derp Back.
Qwerp-Derp
Qwerp-Derp
@Zgarb Hello
Zgarb
Zgarb
Alright, so Boolean values in LC are encoded as true =: λx.λy.x and false =: λx.λy.y. The conditional is ifthenelse =: λp.λa.λb.p a b.
This means that ifthenelse true foo bar = foo and iftehelse false foo bar = bar.
Then we want iszero, which tests whether a Church numeral is 0. It's iszero =: λn.n (λx.false) true. If you give it 0, then the function (λx.false) is iterated 0 times on true, and the result is true. If you give it a positive n, then the function is iterated at least once, and the result is false.
(Remember that a Church numeral is just function iteration).
Finally, we need the n-1 function, which we call pred (for predecessor).
Qwerp-Derp
Qwerp-Derp
So basically λn.IFTHENELSE (ISZERO n) and then the rest of the stuff after it
Zgarb
Zgarb
Yeah.
G =: λr.λn.IFTHENELSE (ISZERO n) 0 (TIMES n (r (PRED n)))
You can probably decode TIMES and PRED from the Wiki article.
Qwerp-Derp
Qwerp-Derp
yeah
@Zgarb So what's G?
G's been used for the Y thing right?
Zgarb
Zgarb
10:27
Yeah, so we know that Y f = f (Y f) holds for all f. In other words, if we denote Y f = F, then F = f F.
Let's see what Y G is.
Denote Y G = F. Then F = G F = (λr.λn.IFTHENELSE (ISZERO n) 0 (TIMES n (r (PRED n)))) F = λn.IFTHENELSE (ISZERO n) 0 (TIMES n (F (PRED n))
Qwerp-Derp
Qwerp-Derp
Mmhmm
Zgarb
Zgarb
F = λn.IFTHENELSE (ISZERO n) 0 (TIMES n (F (PRED n))
That's recursion!
Qwerp-Derp
Qwerp-Derp
Whoa
That's really cool :)
Also that explanation is really clear thanks :)
Zgarb
Zgarb
This is how we use the Y combinator to implement recursion. You write a "recursive lambda term" that can refer to itself, like F = λn.IFTHENELSE (ISZERO n) 0 (TIMES n (F (PRED n)). Then you give it an extra function argument r and replace the Fs in the body with rs to get G = λr.λn.IFTHENELSE (ISZERO n) 0 (TIMES n (r (PRED n))). Apply Y and you're done.

« first day (33 days earlier)    last day (14 days later) »