The expression would equal the reduction of the expression.Īlonzo Church invented the lambda calculus in the 1930s, originally to provide a new and simpler basis for mathematics. Considered as a mathematical deductive system, each reduction would not alter the value of the expression. In this interpretation, if the expression never reduces to normal form then the program never terminates, and the value is undefined. One interpretation of the untyped lambda calculus is as a programming language where evaluation proceeds by performing reductions on an expression until it is in normal form. y means false).Deductive lambda calculus considers what happens when lambda terms are regarded as mathematical expressions. the first argument, this evaluates to (λa.λb. Since the body of this function is simply a, i.e. a)) and every occurrence of n is replaced with the second argument ( (λa.λb. This means that every occurrence of m in m n m is replaced with the first argument ( (λa.λb. The first step is simply to replace each identifier with its definition, i.e. (*) Where "taking two arguments" means "taking an argument and returning a function taking another argument".Īnd true false as seen on the wiki page works like this: So basically the function returns a if both m and n are true and b otherwise. If m is false, it will evaluate to its second argument b. This in turn will evaluate to a if n is true and b if n is false.
If m is true, it will evaluate to its first argument which is n a b. From the looks of it m and n are supposed to be booleans and a and b some other values. The function you showed above takes four arguments*. False is represented as function taking two arguments* and returning the second. In lambda calculus true is represented as a function taking two arguments* and returning the first.
It's the lambda calculus' version of if m and n then a else b. n (m a b) bĪs with other computations in lambda calculus, especially when using Church encodings, it is often easier to work things out with algebraic laws and equational reasoning, then convert to lambdas at the end.Īctually it's a little more than just the AND operator. n (m s f) fĪnd if we rename the success and failure continuations to a and b we return to your original & = \n. Only these are functions, so (n & m) s f = (n ? m : false) s f = n ? (m s f) : (false s f) = n ? (m s f) : fīUT, the ternary construct, when coded in the lambda calculus, is just function application, so we have (n & m) s f = (n m false) s f = n (m s f) (false s f) = n (m s f) f
LAMBDA CALCULUS BOOLEAN CODE
How do we code and? Well, in C we could expand it to n & m = n ? m : false Now I hope you can see where this is going. Where s stands for success, f stands for failure, and the backslash is an ASCII lambda. This coding is called the Church encoding, and the idea is that a Boolean is very much like an "if-then-else function". The arguments are called continuations, because they continue with the rest of the computation the boolean True calls the success continuation and the Boolean False calls the failure continuation. In the lambda calculus, a Boolean is represented by a function that takes two arguments, one for success and one for failure. And that's just the definition of and!Īll this was invented by Alonzo Church, who invented the lambda calculus. Since a is the first argument of your function and b is the second, and true has been defined as a function that gives the first of its two arguments, then if m and n are both true, so is the whole expression. This expression evaluates to a if both m and n are true, and to b otherwise. Then m (n a b) b means if m then (if n then a else b) else b Looking inside your expression at (n a b), that means if n then a else b. So define true = lambda(x).lambda(y).xĪnd a b c will behave like if a then b else c. Gives either b or c, which is just what we want the IF to do. So if a is one of those expressions, then a b c Will give you the first of its arguments, and lambda(x).lambda(y).y Lambda expressions can do that very easily: lambda(x).lambda(y).x This is an expression which chooses the first branch, b, if it is true, and the second, c, if it is false.
LAMBDA CALCULUS BOOLEAN HOW TO
To understand how to represent Booleans in lambda calculus, it helps to think about an IF expression, "if a then b else c".
0 kommentar(er)
