7 ms·

In general, I like it. I think the syntax is a bit messy though. λx.x is much cleaner than {lambda {x} x} Don't want to use λ? Consider \x.x

by chewxy 8y ago

In general, I like it. I think the syntax is a bit messy though. λx.x is much cleaner than {lambda {x} x} Don't want to use λ? Consider \x.x For your special cases of multiple args, consider λx,y,z.(x z)(y x) // S combinator For nullary functions: λ().M Last, this is really more a lisp than a λ-calculus. Difference is subtle.

martyalain 8y ago
Shorter it is, obviously, but when things become more convoluted, I don't think so, you have to memorize priorities, add parenthesis to change them and things like this. The great strength of the prefixed parenthesed Lisp-like notation is to be systematic. IMHO. I think that using lambda instead of λ or even \ helps eyes to read convoluted code, to find the most important element of the language. And when I replace well known names like "true, false, cons, car, cdr, nil, isnil?] by such cryptic characters "|, ø, □, [, ], ?" it's to reduce long lines to short sequences of signs getting a chance to be viewed as a whole picture easy to memorize. A matter of choice. Maybe it's inconsistent. You say "this is really more a lisp than a λ-calculus." Long time I thought that {lambda talk) was a lisp and today I think it is not. Lisps use to begin with several primitives, (cons, car, cdr, ...) and never go down to the reduced set [word, abstraction, application]. I found useful to start from this infrastructure, I think I can better understand concepts. And later will come several superstructures to reach the level of a usable programming language.
- chewxy 8y ago
  yeah, it took me a while to realize you were trying to go for something more lisp than λ-calculus.
kazinator 8y ago
Is it cleaner? What does this mean? λy.λx.xy Is it: {lambda {y} {lambda {x} {x y}}} or is it {lambda {y} {{lambda {x} x} y}} We need to know the relative precedence of the "<function> <arg>" phrase versus the "λ <arg> . <body>" phrase. (I honestly do not know, even though I had studied Lambda Calculus.) If mathematics, that sphere of pure precision of thought, robes itself in ambiguity, isn't that a bit ironic? Of course, "precedence" is a mathematical concept. We establish it, thereby asserting a kind of axiom that governs the syntax we are using, and then everything is precise, as it should be. The only problem is that these distracting concepts are from a different field; they don't speak to the semantics of Lambda Calculus. Why do I have to think about "precedence", when I want to think about Lambda Calculus? Mathematics should be not only precise, but it should separate concerns. We can condense the syntax without introducing ambiguity, e.g.: (λy.(λx.(xy)) (λy.((λx.x)y)
- martyalain 8y ago
  In {lambda talk} it's not possible to write {lambda {y} {lambda {x} {x y}}} because in {lambda {x} {x y}} y is a free variable and lambdas don't define closures, don't accept free variables. I develop a little bit in http://lambdaway.free.fr/lambdaspeech/?view=closure http://lambdaway.free.fr/lambdaspeech/?view=closure. I just found that there is a life out of closures ... About precedence, let's compare the prefixed parenthesed syntax to the standard math notation: {+ 1 {* 2 3} 4} -> 11 // equivalent to 1+(2*3)+4 {+ {* 3 3} {* 4 4}} -> 25 // equivalent to (3*3)+(4*4) {/ {+ 2 5} 2} -> 3.5 // equivalent to (2+5)/2 Note that in the standard math notation, you can forget parenthesis in the two first formulas provided you remember to multiply before adding. In the last formula you must always use parenthesis. My opinion is that the systematic use of parenthesis helps to understand the process. And, last but not least, the evaluator is much more easier to write.
  - kazinator 8y ago
    > y is a free variable No it isn't; it's bound by the outer lambda. You have some funny situation going on there, I'm afraid. If the inner lambda effectively blocks the y reference from connecting with the outer lambda, then y cannot be called a "free variable" in any ordinary sense. Obviously the inner lambda binds it with the purpose of intercepting it and calling it invalid. We might call that an "intercepted, invalid variable" (new term I'm coining right here). A true free variable has no interaction with the enclosing lambda w.r.t. which it is free.
    - martyalain 8y ago
      " No it isn't; it's bound by the outer lambda. " Not in {lambda talk) where a lambda knows nothing but defined arguments. A lambda has no access to any outer environment ... because there is no environment except the global dictionary where are stored primitives and user defined constants and functions. Take a minute to read this page http://lambdaway.free.fr/lambdaspeech/?view=closure http://lambdaway.free.fr/lambdaspeech/?view=closure. Closure is a matter of implementation, not of semantic. And there is a life out of closure. For instance in Scheme we could define the pair structure like this (define cons (lambda (x y) (lambda (z) (z x y)))) (define car (lambda (z) (z (lambda (x y) x)))) (deffine cdr (lambda (z) (z (lambda (x y) y)))) where x and y in the inner lambda's body {z x y} get their values from the outer lambda. In {lambda talk} we define the pair structure like this {def cons {lambda {x y z} {z x y}}} {def car {lambda {z} {z {lambda {x y} x}}}} {def cdr {lambda {z} {z {lambda {x y} y}}}} where cons is a function waiting for three values. When called with two values, {cons hello world}, the lambda stores them in its body and returns a new lambda waiting for the missing value, {lambda {z} {z Hello World}}. And {car {cons Hello World}} will return Hello. The remaining issue without closure is that sometimes you have to build it "by yourself", see for instance this page http://lambdaway.free.fr/lambdaspeech/?view=let http://lambdaway.free.fr/lambdaspeech/?view=let In {lambda talk} lambdas are nothing but local text substitutions. As explained in http://lambdaway.free.fr/lambdaspeech/?view=factory_201902_paper http://lambdaway.free.fr/lambdaspeech/?view=factory_201902_p... . It's as simple as that!

by chewxy 8y ago

martyalain 8y ago

Shorter it is, obviously, but when things become more convoluted, I don't think so, you have to memorize priorities, add parenthesis to change them and things like this. The great strength of the prefixed parenthesed Lisp-like notation is to be systematic. IMHO. I think that using lambda instead of λ or even \ helps eyes to read convoluted code, to find the most important element of the language. And when I replace well known names like "true, false, cons, car, cdr, nil, isnil?] by such cryptic characters "|, ø, □, [, ], ?" it's to reduce long lines to short sequences of signs getting a chance to be viewed as a whole picture easy to memorize. A matter of choice. Maybe it's inconsistent. You say "this is really more a lisp than a λ-calculus." Long time I thought that {lambda talk) was a lisp and today I think it is not. Lisps use to begin with several primitives, (cons, car, cdr, ...) and never go down to the reduced set [word, abstraction, application]. I found useful to start from this infrastructure, I think I can better understand concepts. And later will come several superstructures to reach the level of a usable programming language.

chewxy 8y ago
yeah, it took me a while to realize you were trying to go for something more lisp than λ-calculus.

kazinator 8y ago

Is it cleaner? What does this mean? λy.λx.xy Is it: {lambda {y} {lambda {x} {x y}}} or is it {lambda {y} {{lambda {x} x} y}} We need to know the relative precedence of the "<function> <arg>" phrase versus the "λ <arg> . <body>" phrase. (I honestly do not know, even though I had studied Lambda Calculus.) If mathematics, that sphere of pure precision of thought, robes itself in ambiguity, isn't that a bit ironic? Of course, "precedence" is a mathematical concept. We establish it, thereby asserting a kind of axiom that governs the syntax we are using, and then everything is precise, as it should be. The only problem is that these distracting concepts are from a different field; they don't speak to the semantics of Lambda Calculus. Why do I have to think about "precedence", when I want to think about Lambda Calculus? Mathematics should be not only precise, but it should separate concerns. We can condense the syntax without introducing ambiguity, e.g.: (λy.(λx.(xy)) (λy.((λx.x)y)

martyalain 8y ago
In {lambda talk} it's not possible to write {lambda {y} {lambda {x} {x y}}} because in {lambda {x} {x y}} y is a free variable and lambdas don't define closures, don't accept free variables. I develop a little bit in http://lambdaway.free.fr/lambdaspeech/?view=closure http://lambdaway.free.fr/lambdaspeech/?view=closure. I just found that there is a life out of closures ... About precedence, let's compare the prefixed parenthesed syntax to the standard math notation: {+ 1 {* 2 3} 4} -> 11 // equivalent to 1+(2*3)+4 {+ {* 3 3} {* 4 4}} -> 25 // equivalent to (3*3)+(4*4) {/ {+ 2 5} 2} -> 3.5 // equivalent to (2+5)/2 Note that in the standard math notation, you can forget parenthesis in the two first formulas provided you remember to multiply before adding. In the last formula you must always use parenthesis. My opinion is that the systematic use of parenthesis helps to understand the process. And, last but not least, the evaluator is much more easier to write.
- kazinator 8y ago
  > y is a free variable No it isn't; it's bound by the outer lambda. You have some funny situation going on there, I'm afraid. If the inner lambda effectively blocks the y reference from connecting with the outer lambda, then y cannot be called a "free variable" in any ordinary sense. Obviously the inner lambda binds it with the purpose of intercepting it and calling it invalid. We might call that an "intercepted, invalid variable" (new term I'm coining right here). A true free variable has no interaction with the enclosing lambda w.r.t. which it is free.
  - martyalain 8y ago
    " No it isn't; it's bound by the outer lambda. " Not in {lambda talk) where a lambda knows nothing but defined arguments. A lambda has no access to any outer environment ... because there is no environment except the global dictionary where are stored primitives and user defined constants and functions. Take a minute to read this page http://lambdaway.free.fr/lambdaspeech/?view=closure http://lambdaway.free.fr/lambdaspeech/?view=closure. Closure is a matter of implementation, not of semantic. And there is a life out of closure. For instance in Scheme we could define the pair structure like this (define cons (lambda (x y) (lambda (z) (z x y)))) (define car (lambda (z) (z (lambda (x y) x)))) (deffine cdr (lambda (z) (z (lambda (x y) y)))) where x and y in the inner lambda's body {z x y} get their values from the outer lambda. In {lambda talk} we define the pair structure like this {def cons {lambda {x y z} {z x y}}} {def car {lambda {z} {z {lambda {x y} x}}}} {def cdr {lambda {z} {z {lambda {x y} y}}}} where cons is a function waiting for three values. When called with two values, {cons hello world}, the lambda stores them in its body and returns a new lambda waiting for the missing value, {lambda {z} {z Hello World}}. And {car {cons Hello World}} will return Hello. The remaining issue without closure is that sometimes you have to build it "by yourself", see for instance this page http://lambdaway.free.fr/lambdaspeech/?view=let http://lambdaway.free.fr/lambdaspeech/?view=let In {lambda talk} lambdas are nothing but local text substitutions. As explained in http://lambdaway.free.fr/lambdaspeech/?view=factory_201902_paper http://lambdaway.free.fr/lambdaspeech/?view=factory_201902_p... . It's as simple as that!