[plt-scheme] The Lambda Calculus behind functional programming

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