[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 ;)

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 :)

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.

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.

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?

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)))