[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: 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.

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

>
> 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.
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?

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


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