This house is the Barcelona Pavilion buit by Mies van der Rohe in the thirties. It's often compared to the Maxwell's equations of architecture. As are the rules defining the λ-calculus:[ e := v | λv.e | ee ] written upon the picture.
I must admit it's a little "cryptic".
What I'm trying to do is quickly explained in the Abstract below the picture. and in deep in the rest of the paper. Probably it's not clear enough. Sorry.
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.
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.:
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. 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:
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.
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.
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. 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 issue is that the processing of your outer lambda is not traversing its interior to connect with the y reference; it is blocked by the inner lambda.
> lambdas are nothing but local text substitutions
An outer lambda can substitute inside the inner lambda, even if it's all textual.
"{{lambda {y} {lambda {x} {x y}}} arg}"
--> substitute y = "arg" everywhere y is not shadowed.
"{lambda {x} {x arg}}"
There you go: lexical closure: the "arg" text is captured inside the character string "{lambda {x} {x arg}}".
This simple thing not working is just a bug in your implementation (that you simply documented away as a requirement instead of fixing it).
Thank you for your kind remarks but I'm still unable to understand the proposed code. Testing the first expression in the current {lambda talk} evaluator doesn't return anything:
A) abstraction:
1: {{lambda {y} {lambda {x} {x y}}} arg}
2: {{lambda {y} _LAMB_0} arg} // where _lAMB_0 is {lambda {x} {x y}}
3: {_LAMB_1 arg} // where _LAMB_1 is {lambda {y} _LAMB_0}
Well I don't understand your idea. I'm just an amateur.
In this paper http://lambdaway.free.fr/lambdaspeech/?view=fabric_new I give the eval_lambda() JS code (section 2.3. special forms evaluation) where inner lambdas are recursively evaluated without carrying arguments which are ipso facto unknown by inner lambdas. Until now I am unable to write a code which could carry them.
In this page http://lambdaway.free.fr/workshop/?view=lambdacode, following Peter Norvig (http://norvig.com/lispy.html) I wrote a more "standard" evaluator tokenizing the code, building a nested tree and recursively evaluating it. The evaluator's main function ( var evaluate = function (x, env) {...} ) works in nested environments and lambdas naturally define closures. It's a very clever approach compared to "my" regexp based evaluation. And everything works fine ... but doesn't completely fit my needs in a wiki context:
- First, as in most of languages, words must be quoted to be protected from any unwanted evaluation,
- the {pre some code} container can't be used (spaces, tabs, line returns are destroyed during the tokenization),
- I just can't imagine the cost of the AST approach for such a page http://lambdaway.free.fr/lambdaspeech/?view=jules_verne containing 1228778 chars, simply copy/pasted from a text file, as it is. It's just text as in a text editor (plus some enrichments, a TOC, ...). The {lambda talk}'s evaluator flies quickly over the 1228778 chars, say 250000 words, words are just words, and has to evaluate a reduced number of function calls, about 180, until all curly braces have disappeared.
What seems to be going on in (A) is a kind of inside-out reduction. The inner lambda term has been replaced by the placeholder __LAMB_0, and so now it is impossible to substitute y into it. Substitution simply has has to go outside in.
We consider the call{{{lambda {y} {lambda {x} {x y}}} arg}, and so the text arg is identified with y. The job is then to substitute y <- arg in the interior of the outer lambda: {lambda {y} <interior ...>}.
That interior happens to be {lambda {x} {x y}}. So we need a recursive walk procedure which performs that substitution. The procedure has a list of bindings which contains {y -> arg} which it passes down. The procedure has to recognize your special forms like lambda and let so that it handles variable shadowing. Our y = arg could be shadowed by some inner y.
Once we have done the substitution, then we can convert the substituted lambda to _LAMB_0. So we have:
1: input:
{{lambda {y} {lambda {x} {x y}}} arg}
2: lambda is identified, and encode dinto a _LAM term:
{_LAMB_0 arg} where _LAMB_0 is {lambda {y} {lambda {x} {x y}}}
3: lambda term is called, with arg:
this simply substitution y = arg into its body and then producing the
substituted body:
{lambda {x} {x y}} -> {lambda {x} {x arg}}
4. lambda call returns this:
{lambda {x} {x arg}}
5. This converts to the _LAMB_* term:
_LAMB_1
There is no captured environment in the inner lambda because the text is fully substituted; we have removed the variable y. The __LAM_1 string is effectively a closure. Closures don't require external environments if we are working with strings, which are copied and pasted in place. Environments are required when the expressions contain unsubstituted variables.
Alternatively to the above evaluation strategy, we could identify and convert all LAM terms upfront:
1: input:
{{lambda {y} {lambda {x} {x y}}} arg}
2: all lambdas are recursively identified:
{__LAMB_0 arg}, where ...
_LAMB_0 = {lambda {y} _LAMB_1}, where ...
_LAMB_1 = {lambda {x} {x y}}
3: arg is applied to _LAMB_0:
_LAMB_0: equates "y" with "arg" and processes the body, which consists of _LAMB_1:
the result is:
{lambda {x} {x arg}}
RULE: when a _LAMB term undergoes substitution, it produces a new _LAMB term.
4: Thus {_LAMB_0 arg} reduces to _LAMB_2, which denotes {lambda {x} {x arg}}.
Woaaaw, thank you very much for having taken time to go inside the code and for starting these new ways. I have no more excuse to say "Well, there is a life out of closure and I don't mind because my lambdas are de facto partially applicable, etc ..."
I have now a lot of work to implement closure in {lambda talk}. Maybe I can do that.
You might want to put some content width limits on it so people don't end up with extreme line widths on UW screens. Rule of thumb is to aim for 60-80 characters per line for optimal readability - without zooming, I get about 480 characters per line in your layout.
Thanks, I agree with you, even if it's always possible to reduce the width of the browser's window to adjust lines to the desired display. So I defined the limit to 700px which looks good for me.
