Hi All, I am working on the exercise questions of book The Lambda calculus. One of the questions that I am stuck is proving the following: Show that the application is not associative; in fact, x(yz) not equals (xy)z Here is what I have worked on so far: Let x = λa.λb. ab Let y = λb.λc. bc Let z = λa.λc. ac (xy)z => ((λa.λb. ab) (λb....
Hi All, Continuing on exercises in book Lambda Calculus, the question is as follows: Suppose a symbol of the λ-calculus alphabet is always 0.5cm wide. Write down a λ-term with length less than 20 cm having a normal form with length at least (10^10)^10 lightyear. The speed of light is c = 3 * (10^10) cm/sec. I have absolu...
Hi All, For a lambda expression (x (λx y. x y) z h), I did not understand how free variables x (outer x), z and h can be converted in C code? Regards, darkie ...
Hi all, I'm trying to figure out how to express the Y-Combitor in this Finally Tagless EDSL: class Symantics exp where lam :: (exp a -> exp b) -> exp (exp a -> exp b) app :: exp (exp a -> exp b) -> exp a -> exp b fix :: ... fix f = ..... I'm not certain but I think a default implementation of the Y-Combinator should ...
Infrequently I've seen the word "combinator" in Lisp/Scheme books or video lectures. But it just appears like a glint and I never pay attention to. However, while studying lambda calculus I found out that wikipedia says "[combinatory logic] has more recently been used in computer science as a theoretical model of computation and also a...
All, Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem. (λm λn λa λb . m (n a b) b) (λ f x. x) (λ f x. f x) This is what I tried, but I am stuck: Considering the above expression as : (λm.E) M equates to E= (λn λa λb. m (n a b) b) M = (λf x. x)(λ f x....
I can understand how to create and think about the SKI and BCKW calculus, but I am never able to find practical uses. Maybe I am not looking deeply enough? That is, I wonder if (an example only please, I am not implying this is true) Java Servlets use S extensively and Python generators are an example of BCW and I am just unable to see...
http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html is a concise definition of the simply typed lambda calculus in Prolog. It looks okay, but then he purports to assign a type to the Y combinator... whereas in a very real sense the entire purpose of adding types to lambda calculus is to refuse to assign ...
I am working through SICP, and the problem 2.6 has put me in something of a quandary. In dealing with Church numerals, the concept of encoding zero and 1 to be arbitrary functions that satisfy certain axioms seems to make sense. Additionally, deriving the direct formulation of individual numbers using the definition of zero, and an add-1...
I am writing a lambda calculus in F#, but I am stuck on implementing the beta-reduction (substituting formal parameters with the actual parameters). (lambda x.e)f --> e[f/x] example of usage: (lambda n. n*2+3) 7 --> (n*2+3)[7/n] --> 7*2+3 So I'd love to hear some suggestions in regards to how others might go about this. Any ideas w...