[plt-scheme] The Lambda Calculus behind functional programming

On 9/1/07, Jos Koot <jos.koot at telefonica.net> wrote:
>
> ----- Original Message -----
> From: "Corey Sweeney" <corey.sweeney at gmail.com>
> To: "Jos Koot" <jos.koot at telefonica.net>
> Cc: "PLT Scheme" <plt-scheme at list.cs.brown.edu>
> Sent: Saturday, September 01, 2007 7:59 PM
> Subject: Re: [plt-scheme] The Lambda Calculus behind functional programming
>
>
> > What have I implemented?  I've implemented everything! heh.  Some of
> > the features are:  The scheme-like syntax for the lambda calculus,
> > libraries, JIT compilation to 80486 machine code, 80486 virtual
> > machine, the GUI IDE (with built in mp3 player ;), *editor side
> > transformations*, my bizzare "type system", a new feature that I guess
> > could best be called "syntactic manipulation" (the feature in LC has
> > some similarities to macros in scheme).  Plus there are many other
> > things that are harder to explain ;)
>
> A compiler. That sounds like you have choosen a fixed reduction strategy.

Actually dynamic reduction stratagies are one of my original goals,
but I havn't gotten that implemented yet. Also instead of calling it a
compiler, i should probably call it a "compiler"  (with quotes), as it
may or may not count as a compiler to a particular person depending on
the individuals precice definition of a compiler.

> > Now when I say I've implemented these, that dosn't mean that these are
> > all finished.  That just means that I've gotten each of them working
> > for at least 1 case.  For example the scheme like syntax is pretty
> > much fully completed, whereas the 80486 virutal machine only works for
> > a handfull of instructions so far, which are just the instructions
> > needed to complete a specific task. There is a substantial ammount of
> > work to do before the system will be ready for "prime time".
> >
> >
> > ....Now back to the discussion:
> >
> > I did not know  auto-currying was addressed in the documentation.  too
> > bad i didn't know that before I wrote my own :)
>
> I dont know which documentation you mean.
> What I do mean by the term 'autocurrying' is to interpret
> (lambda (x y ...) body) as
> (lambda (x) (lambda (y ...) body))
> In Barendregt it is introduced as a "convenient notation"
> (lambda argument-name-with-arrow dot body)
> Barendregt does not consider this to be part of LC itself.
> It is simply an abbreviation (for the human reader).
> Barendrecht does not introduce it as a well formed expression of the lambda
> calculus itself.

That is exactly what I implmented as "autocurrying", and I fully agree
with Barendregt.  autocurrying is a function of the editor (part of
the GUI IDE), not part of the language semantics.


> >
> > So yes, scheme can be brought to the same syntax as the lambda
> > calculus, and my point with this was that a introductory programming
> > course in LC could be made to be almsot exactly the same as a
> > introductory functional programming course in scheme.  The only
> > important difference would be the day that the student asks how
> > numbers work, and you tell him to define addition (or multiplication
> > as shown below)
> >
> > (( (lambda (m) (lambda (n) ((m (lambda (x) (+ n x))) 0)))
> >   3)
> > 7)
> >
> > In LC this is 21.
>
> I suppose LC means Lambda Calculus. Does it? In my limited ears the above sounds
> as though LC means something else.

yes LC refers to lambda calculus.  (that notation got started sometime
earlier in this thread)

> In Lambda Calculus there is no such thing as a number.
> There are several ways to represent numbers by means of lambda terms.
> And there is a way to represent lambda terms by the representatives of numbers
> (Goedel numbering)
> Do you mean that your "LC" converts numbers into, for instance, Church numerals?

Yes that's exactly what I mean.  it takes a syntax similar to scheme,
in this case, it might be the string "3", and converts it to (lambda
(s) (lambda (z) (s (s (s z))))). Again this is a function of the
editor, as it does not belong in LC.  And that's what I mean by a
"scheme like syntax".

>
> >
> > In scheme this is:
> > . procedure application: expected procedure, given: 3; arguments were:
> > #<procedure>
> >
> >
> > In LC (lambda (s) (lamba (z) (s (s (s z))))) and 3 are equivilant.  In
> > scheme they are not.
>
> I disagree. 3 is a number. It is not the same as "left half square bracket
> number right half square bracket", which is an abbreviation for a Church numeral
> (or a numeral of some other representation of numbers as long as it is clear
> which representation has been choosen)
>
> >
> > Scheme implements the lambda of lambda calculus, but is missing all
> > the libraries needed for LC development. The libraries can be
> > implemented as scheme functions, but you still need to do the 3 ->
> > (lambda (s) (lamba (z) (s (s (s z))))) translations.
> >
> > How clear was that?
>
> For Me? Not very clear I am afraid, but I am sure that is to blame on me :)
> Jos Koot

Your guess was correct, so we can't be doing that bad ;).

Corey

>
>
> >
> > Corey
> >
> >
> > On 9/1/07, Jos Koot <jos.koot at telefonica.net> wrote:
> >> ----- Original Message -----
> >> From: "Corey Sweeney" <corey.sweeney at gmail.com>
> >> To: "Jos Koot" <jos.koot at telefonica.net>
> >> Cc: "PLT Scheme" <plt-scheme at list.cs.brown.edu>
> >> Sent: Friday, August 31, 2007 8:46 PM
> >> Subject: Re: [plt-scheme] The Lambda Calculus behind functional programming
> >>
> >>
> >> > On 8/31/07, Jos Koot <jos.koot at telefonica.net> wrote:
> >> >> Would it make sense to present a formal mathematical definition of a real
> >> >> number
> >> >> on primary school as a starting point for elementary arithmetics?
> >> >
> >> > Starting with real numbers would probably be a bad idea.  But I do
> >> > think the peano axioms would be a good place to start.
> >> >
> >> > Now, when I say that, I don't necicarly mean that kids have to learn
> >> > what the "upside down A" means (for all), and what the "backwards E"
> >> > means (there exists), etc.  You can teach anything isomorphic to the
> >> > symbols.  (for a LC example, see "the aligator eggs" link posted
> >> > earlier http://worrydream.com/AlligatorEggs/ ).
> >> >
> >> > So the problems in the course would be essentially the same, just
> >> > "tweaked".
> >> >
> >> > I'm not the first person to think this.  I heard that they tried
> >> > teaching the axioms at the beginning years ago, and gave it up.  I
> >> > briefly looked into it a while back, and the reason appeared to be
> >> > that most grade school teachers didn't understand what they were
> >> > teaching.
> >> >
> >> > As for math, "what is this good for?":  By knowing the axioms, the
> >> > student can check their own work.
> >> >
> >> > Before I move on, I'll give a example isomorphism for some of the peano
> >> > axioms:
> >> >
> >> > Put up your right hand.  We will call your palm is "zero".
> >> > Put up some fingers.  Each finger will be called "successor".
> >> >
> >> > Peano axiom:  You are allowed to "move" a finger from one hand to another.
> >> >     i.e. (Sx + y) = (x + Sy)
> >> >
> >> > Peano axiom:  You are allowed to raise, or put down your left hand at
> >> > any time iff you have no fingers up on it.
> >> >     i.e. (0 + x) = x
> >> >
> >> > You probably get the idea from here....
> >> >
> >> >
> >> >
> >> > Similarly, I think we might be differing on how we imagine a
> >> > introductory functional programming course in LC.  The LC syntax can
> >> > be adjusted to look almost like the scheme syntax, and the problems in
> >> > the book could be the same problems.
> >> >
> >> > so the "answer" to a problem in LC might be:
> >> > (map (+ 2)  (list 2 3 4))
> >> >
> >> > and the "answer" to the same problem in scheme:
> >> > (map (lambda (x) (+ 2 x))  (list 2 3 4))
> >> >
> >> > So the way I see it, the course syllabus would mostly be unaffected by
> >> > the move to LC.  However with LC we now have the ability to reference
> >> > + as something other then just a primative when the student asks.
> >> >
> >> >
> >> > Does that make sence to you?
> >> >
> >> > (P.S. say yes, cause I've already implemented the scheme-like LC syntax.
> >> > heh)
> >>
> >> I am not sure what you mean. The syntax is already in Scheme (just maintain
> >> (arity 1 or autocurrying) lambda and refrain from everything else )
> >> BTW, section 12.5  Special Syntax Identifiers in PLT MzScheme: Language
> >> Manual
> >> already shows how to strip Scheme in this way.
> >> The distinction between (lambda-dot-variable ...) and (lambda (variable) ...)
> >> notation is not essential, I agree. So we have the syntax. What about normal
> >> forms, undecidibility and reduction strategies?
> >> Personally I have had much profit from the approach by Daniel P. Friedman and
> >> Matthias Felleisen in The Little LISPer (nowadays The Little Schemer)
> >> In this book a subset of Scheme is used for the introduction of recursion (it
> >> is
> >> not a programming course), but at the end it shows that it is possible to
> >> drop
> >> most of the introduced primitives and indeed it made me wonder whether or not
> >> it
> >> would be possible to drop all except lambda the ultimate and it almoset made
> >> me
> >> redecover LC almost by myself. May be it is not always possible, but giving
> >> your
> >> students a feeling that they are on a discovery tour and do rediscovery
> >> rather
> >> than reproduction, seems a good method to me. So I would suggest to make the
> >> students ripe for the discovery of LC and CL before presenting it in ready
> >> shaped form. As I already said: first make the students ask the right
> >> questions.
> >> Mho.
> >>
> >> Nevertheless your last line above makes me curious about what your
> >> implementation is like and particularly "what it implements".
> >> Best wishes, Jos Koot
> >>
> >> > Corey
> >> >
> >> >
> >> >> I think that for most students LC is too abstract as long as they have not
> >> >> yet
> >> >> done some fp.
> >> >> I would have been such a student, I think.
> >> >> I try always to be prepared for the question "what is this good for?"
> >> >> When working with future programmers, an answer might be: "to better
> >> >> understand
> >> >> the essentials of computation" but this would not make sense to someone
> >> >> who
> >> >> does
> >> >> not yet have any idea of computation at all.
> >> >> Jos koot
> >> >>
> >> >> ((((lambda(x)((((((x x)x)x)x)x)x))
> >> >>    (lambda(x)(lambda(y)(x(x y)))))
> >> >>   (lambda(x)(write x)x))
> >> >>  'greeting)
> >> >> ----- Original Message -----
> >> >> From: "Corey Sweeney" <corey.sweeney at gmail.com>
> >> >> To: "Jos Koot" <jos.koot at telefonica.net>
> >> >> Cc: "Grant Rettke" <grettke at acm.org>; "PLT Scheme"
> >> >> <plt-scheme at list.cs.brown.edu>
> >> >> Sent: Thursday, August 30, 2007 4:39 PM
> >> >> Subject: Re: [plt-scheme] The Lambda Calculus behind functional
> >> >> programming
> >> >>
> >> >>
> >> >> > On 8/29/07, Jos Koot <jos.koot at telefonica.net> wrote:
> >> >> >> For me discovering Lambda Calculus (and combinatory logic) was fabulous
> >> >> >> in
> >> >> >> itself. It is beauty.
> >> >> >> Whether or not it makes you a better programmer. I am inclined to think
> >> >> >> so,
> >> >> >> but
> >> >> >> I don't have any kind of evidence,
> >> >> >> Anyway, when my friends ask me what I am doing these days, I have much
> >> >> >> trouble
> >> >> >> making an understandable answer.
> >> >> >> My conclusion:
> >> >> >> 1: Lambda calculus is not the starting point of learning programming, I
> >> >> >> think.
> >> >> >
> >> >> > I personally would tend to disagree with the idea of lambda calucus
> >> >> > not being a good starting point.  (well, technically typing would be
> >> >> > the starting point :) .  Why do you think it's not a good starting
> >> >> > point?  Is it the lack of a good IDE?  (which by the way, i have a
> >> >> > solution for ;) .   I would agree that paper and pencil is not a good
> >> >> > way to start.  But for the motivated learner, I think that the lambda
> >> >> > calculus with a few moddification could be a near optimal environment.
> >> >> >
> >> >> > What are other peoples thoughts?
> >> >> >
> >> >> > Corey
> >> >> >
> >> >> >> 2: At some stage you wonder: what are the essential principles of
> >> >> >> programming.
> >> >> >> 3: At that point lambda Calculus may be an answer.
> >> >> >> 4: Wait for your students to ask the question before answering it
> >> >> >> 5: Not all of us can claim to be as clever as Socrates, but asking
> >> >> >> questions
> >> >> >> is
> >> >> >> a good method to make your students ask the right questions.
> >> >> >> 6: I know I have failed on this many times
> >> >> >> Jos Koot
> >> >> >>
> >> >> >>
> >> >> >> ((((lambda(x)((((((x x)x)x)x)x)x))
> >> >> >>    (lambda(x)(lambda(y)(x(x y)))))
> >> >> >>   (lambda(x)(write x)x))
> >> >> >>  'greeting)
> >> >> >> ----- Original Message -----
> >> >> >> From: "Grant Rettke" <grettke at acm.org>
> >> >> >> To: "PLT Scheme" <plt-scheme at list.cs.brown.edu>
> >> >> >> Sent: Wednesday, August 29, 2007 8:27 PM
> >> >> >> Subject: [plt-scheme] The Lambda Calculus behind functional programming
> >> >> >>
> >> >> >>
> >> >> >> > When I tell people that I'm learning Scheme the first thing they ask
> >> >> >> > me is "So have you learned lambda calculus?". I've learned enough to
> >> >> >> > say the words "lambda calculus" and that everyone says that lambda
> >> >> >> > calculus is the theoretical backbone of functional programming; but
> >> >> >> > that is it.
> >> >> >> >
> >> >> >> > The following question is a simple one, it makes no attempt to
> >> >> >> > generalize whether anything is worth learning, I think you get the
> >> >> >> > idea.
> >> >> >> >
> >> >> >> > So to revisit this again, what do you need to learn of the lambda
> >> >> >> > calculus relative to FP?
> >> >> >> >
> >> >> >> > What would you tell folks about who have never looked at FP when they
> >> >> >> > ask you about lambda calculus?
> >> >> >> > _________________________________________________
> >> >> >> >  For list-related administrative tasks:
> >> >> >> >  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
> >> >> >> >
> >> >> >>
> >> >> >> _________________________________________________
> >> >> >>   For list-related administrative tasks:
> >> >> >>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme
> >> >> >>
> >> >> >
> >> >> >
> >> >> > --
> >> >> > ((lambda (y) (y y)) (lambda (y) (y y)))
> >> >> >
> >> >>
> >> >>
> >> >
> >> >
> >> > --
> >> > ((lambda (y) (y y)) (lambda (y) (y y)))
> >> >
> >>
> >>
> >
> >
> > --
> > ((lambda (y) (y y)) (lambda (y) (y y)))
> >
>
>


-- 
((lambda (y) (y y)) (lambda (y) (y y)))