From: Raffael Mancini
Subject: Lambda-calculus and lisp
Date: 
Message-ID: <52s5l4F1qaeqrU1@mid.uni-berlin.de>
Hi,
I�ve been fancying with learning common lisp for some time now. I
actually read "lisp primer" to some extend some time ago and really
liked the idea behind the language.
But do you find it important or helpful to know lambda-calculus in order
to learn lisp? I�ve lent "An introduction to Lambda Calculi for Computer
Scientists" by Chris Hankin and read a few Pages of it. It�s damn
interesting (I�d even call it brain sex ;)) even though it�s a tough read.
So should I first learn lisp, then about lambda calculus or the other
way around, or even do something different.

Thanks for your opinions.

Greetings from Munich,
Raffael Mancini

From: Ken Tilton
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <vr7yh.165$Pf7.19@newsfe11.lga>
Raffael Mancini wrote:
> Hi,
> I�ve been fancying with learning common lisp for some time now. I
> actually read "lisp primer" to some extend some time ago and really
> liked the idea behind the language.
> But do you find it important or helpful to know lambda-calculus in order
> to learn lisp? I�ve lent "An introduction to Lambda Calculi for Computer
> Scientists" by Chris Hankin and read a few Pages of it. It�s damn
> interesting (I�d even call it brain sex ;)) even though it�s a tough read.
> So should I first learn lisp, then about lambda calculus or the other
> way around, or even do something different.

I have been doing Lisp heavily for ten years and I understand nothing of 
lambda calculus. I doubt it would even help.

ken


-- 
Well, I've wrestled with reality for 35 years, Doctor, and
I'm happy to state I finally won out over it.
                                   -- Elwood P. Dowd

In this world, you must be oh so smart or oh so pleasant.
                                   -- Elwood's Mom
From: Ken Tilton
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <4P7yh.567$8Z3.438@newsfe08.lga>
Ken Tilton wrote:
> 
> 
> Raffael Mancini wrote:
> 
>> Hi,
>> I�ve been fancying with learning common lisp for some time now. I
>> actually read "lisp primer" to some extend some time ago and really
>> liked the idea behind the language.
>> But do you find it important or helpful to know lambda-calculus in order
>> to learn lisp? I�ve lent "An introduction to Lambda Calculi for Computer
>> Scientists" by Chris Hankin and read a few Pages of it. It�s damn
>> interesting (I�d even call it brain sex ;)) even though it�s a tough 
>> read.

btw, you are in good company, McCarthy did not understand it either.

ken

-- 
Well, I've wrestled with reality for 35 years, Doctor, and
I'm happy to state I finally won out over it.
                                   -- Elwood P. Dowd

In this world, you must be oh so smart or oh so pleasant.
                                   -- Elwood's Mom
From: Espen Vestre
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <m164aefn7o.fsf@gazonk.vestre.net>
Ken Tilton <·········@gmail.com> writes:

> I have been doing Lisp heavily for ten years and I understand nothing
> of lambda calculus. I doubt it would even help.

:-)

You don't have to understand lambda calculus to understand LAMBDA or
functions-as-first-class-objects, but I think you need to know enough
of math to at least be able to grasp the idea of nameless functions,
the fact that your everyday math operations are nothing but functions,
or the fact that any relation also is a function.
-- 
  (espen)
From: Ken Tilton
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <_liyh.656$9R1.484@newsfe12.lga>
Espen Vestre wrote:
> Ken Tilton <·········@gmail.com> writes:
> 
> 
>>I have been doing Lisp heavily for ten years and I understand nothing
>>of lambda calculus. I doubt it would even help.
> 
> 
> :-)
> 
> You don't have to understand lambda calculus to understand LAMBDA or
> functions-as-first-class-objects, but I think you need to know enough
> of math to at least be able to grasp the idea of nameless functions,

No, you need to have been programming C non-stop for five years and 
always hated it when you had to stop in the middle of a nice bit of code 
to go find a blank space on the page of source where you could type in a 
seperate function you need /just this once/ and make up a stupid name 
for it just so you could pass its address to another function.

:)

kzo

-- 
Well, I've wrestled with reality for 35 years, Doctor, and
I'm happy to state I finally won out over it.
                                   -- Elwood P. Dowd

In this world, you must be oh so smart or oh so pleasant.
                                   -- Elwood's Mom
From: Holger Schauer
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <yxzk5yuvyrd.fsf@gmx.de>
On 4907 September 1993, Espen Vestre wrote:
> or the fact that any relation also is a function.

It just the other way 'round.

Holger

-- 
---          http://hillview.bugwriter.net/            ---
Fachbegriffe der Informatik - Einfach erkl�rt
37: Fehlertolerant
       Das Programm erlaubt keine Benutzereingaben.
From: Espen Vestre
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <m1k5yuca5e.fsf@gazonk.vestre.net>
Holger Schauer <··············@gmx.de> writes:

> On 4907 September 1993, Espen Vestre wrote:
>> or the fact that any relation also is a function.
>
> It just the other way 'round.

Huh?
-- 
  (espen)
From: Raffael Mancini
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <52u6frF1qaka9U1@mid.uni-berlin.de>
Espen Vestre wrote:
> Holger Schauer <··············@gmx.de> writes:
> 
>> On 4907 September 1993, Espen Vestre wrote:
>>> or the fact that any relation also is a function.
>> It just the other way 'round.
> 
> Huh?

Well not every relation is a function, as relations can have more than
one results which is not allowed for functions. So functions are a
subset of relations.

Greets, Raffael Mancini
From: Espen Vestre
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <m13b5ic8hl.fsf@gazonk.vestre.net>
Raffael Mancini <·······@yahoo.de> writes:

>> Huh?
>
> Well not every relation is a function, as relations can have more than
> one results which is not allowed for functions. So functions are a
> subset of relations.

You're both missing the point... Heck, I thought this was completely
obvious to any lisper (but I have to admit that I've probably got a
minor brain damage due to some exposure to axiomatic set theory and
lambda calculus)! What do you guys do when you encounter a relation
and need to implement a check for it?  Run for help from the prolog
guys? I think not! You probably implement a in-my-relation-p
function. And there's my point: Any relation is also a function, but
of course a function with a different /range/, namely the set of truth
values {0, 1} (or {T,F}, (t nil) or whatever notation you like :)).
-- 
  (espen)
From: Raffael Mancini
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <52uadqF1q0bukU1@mid.uni-berlin.de>
Espen Vestre wrote:
> Raffael Mancini <·······@yahoo.de> writes:
> 
>>> Huh?
>> Well not every relation is a function, as relations can have more than
>> one results which is not allowed for functions. So functions are a
>> subset of relations.
> 
> You're both missing the point... Heck, I thought this was completely
> obvious to any lisper (but I have to admit that I've probably got a
> minor brain damage due to some exposure to axiomatic set theory and
> lambda calculus)! What do you guys do when you encounter a relation
> and need to implement a check for it?  Run for help from the prolog
> guys? I think not! You probably implement a in-my-relation-p
> function. And there's my point: Any relation is also a function, but
> of course a function with a different /range/, namely the set of truth
> values {0, 1} (or {T,F}, (t nil) or whatever notation you like :)).
 What I was talking about are strictly mathematical function, but I
think I got your point.
From: Espen Vestre
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <m1r6t2ardg.fsf@gazonk.vestre.net>
Raffael Mancini <·······@yahoo.de> writes:

>  What I was talking about are strictly mathematical function, but
> think I got your point.

I hate to nit-pick, but functions with range {0,1} /are/ strictly
mathematical - their range is just different from their domain (if
they're not unary truth functions, that is ;-)).
-- 
  (espen)
From: Raffael Mancini
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <52ucv7F1pt2n1U1@mid.uni-berlin.de>
Espen Vestre wrote:
> Raffael Mancini <·······@yahoo.de> writes:
> 
>>  What I was talking about are strictly mathematical function, but
>> think I got your point.
> 
> I hate to nit-pick, but functions with range {0,1} /are/ strictly
> mathematical - their range is just different from their domain (if
> they're not unary truth functions, that is ;-)).

What I was trying to say is that the assertion:

[...] any relation also is a function.

is wrong as far as I know. Imagine a relation that maps a number to two
other numbers so that the sum of those numbers is equal to the first
number; this relation is not a NOT a function because it has multiple
possible results (like the reciprocal of the sine function for example).
Of course you could say that the ralation I cited here returns back a
set of values, but then you simply avoid the problem.
From: Espen Vestre
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <m1bqk5vrbf.fsf@vestre.net>
Raffael Mancini <·······@yahoo.de> writes:

> What I was trying to say is that the assertion:
>
> [...] any relation also is a function.
>
> is wrong as far as I know. 

Yes, my formulation was sloppy, it would have been better to use "has
a characteristic function" or something like that. Lambda calculus
does not distinguish the two: Relations /are/ characteristic
functions. So maybe that's the answer to "how much lambda calculus do
you need" ;)
-- 
  (espen)
From: Raffael Mancini
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <52uh7lF1peig0U1@mid.uni-berlin.de>
Espen Vestre wrote:
> Raffael Mancini <·······@yahoo.de> writes:
> 
>> What I was trying to say is that the assertion:
>>
>> [...] any relation also is a function.
>>
>> is wrong as far as I know. 
> 
> Yes, my formulation was sloppy, it would have been better to use "has
> a characteristic function" or something like that. Lambda calculus
> does not distinguish the two: Relations /are/ characteristic
> functions. So maybe that's the answer to "how much lambda calculus do
> you need" ;)

Well, don�t take me to serious ;). I�m just telling you what my teachers
 have been telling me for years now.
But as I really like math (well, not doing exercises, just reading about
it), I think I�ll continue reading this book, and later learn common
lisp or some other lisp dialect.

Anyway, thank you for your inspiring answers.

ps: I�m a little astonished that this group is so civilized, I haven�t
seen any trolling yet :)

Greetings,
Raffael Mancini
From: Harald Hanche-Olsen
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <pcoy7n991ov.fsf@shuttle.math.ntnu.no>
+ Raffael Mancini <·······@yahoo.de>:

| ps: I�m a little astonished that this group is so civilized, I
| haven�t seen any trolling yet :)

Well, you really are new around here I guess.
Or maybe even our trolls /seem/ nice, on the surface.
Oh, and quite often the nice guys behave like trolls.
It's a confusing place, for sure.  But fun.

-- 
* Harald Hanche-Olsen     <URL:http://www.math.ntnu.no/~hanche/>
- It is undesirable to believe a proposition
  when there is no ground whatsoever for supposing it is true.
  -- Bertrand Russell
From: Ken Tilton
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <_nLyh.28$pj6.11@newsfe12.lga>
Raffael Mancini wrote:

> ps: I�m a little astonished that this group is so civilized, I haven�t
> seen any trolling yet :)

It's the hounds. Big mistake. Unbalanced the ecosystem, drove the trolls 
to extinction. No fun around here anymore. :(

ken

-- 
Well, I've wrestled with reality for 35 years, Doctor, and
I'm happy to state I finally won out over it.
                                   -- Elwood P. Dowd

In this world, you must be oh so smart or oh so pleasant.
                                   -- Elwood's Mom
From: Holger Schauer
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <yxzk5ytu1eu.fsf@gmx.de>
On 4907 September 1993, Espen Vestre wrote:
> Raffael Mancini <·······@yahoo.de> writes:
>> What I was trying to say is that the assertion:
>> [...] any relation also is a function.
>> is wrong as far as I know. 

Yes, that's the point I was trying to make, too.

> Yes, my formulation was sloppy, it would have been better to use "has
> a characteristic function" or something like that. Lambda calculus
> does not distinguish the two: Relations /are/ characteristic
> functions.

If I am not very much mistaken, lambda calculus doesn't make any
claims with regard to what is a relation and what is a function.[1]
I'm not even sure if it makes sense to talk about lambda calculus
wrt. to relations: after all, what result you eventually arrive at is
surely determined in lambda calculus, hence the expressions in lambda
calculus are functions, not relations. If it's still unclear, consider

(lambda (x y)
  (+ x y)

There is no way in which this expression can be converted/reduced to
anything but 3 for x=1 and y=2. That is fine for a function. But for
some relation, it would be fine to have 3,4 and even 5 as equally fine
"results" for that same set of "inputs" 1 and 2. That's not true for
functions -- a function relates each of the elements of its domain to
exactly one element of its codomain (range) (in lambda calculus as
well as in mathematics in general).

What you were confusing in your other posting are two very different
things: the relation itself (to which value relates the set 1 and 2)
and the *test* whether some domain and range values are related (to
stick with the example, that's the function {{1,2},3}->{true,false}).
Say that this function ('foo-p') returns indeed true for the given set
(relation 'foo') and also true for {{1,2},4}. This still doesn't imply
that 'foo' itself is a function.

> So maybe that's the answer to "how much lambda calculus do
> you need" ;)

Well, having grasped lambda calculus surely helps understanding apply,
funcall, mapc* and friends. And it's quite useful for scaring students
away from those overcrowded lisp courses we teach all day, of course.
:-)

Holger

Footnotes: 
[1]  Actually, that's not quite true. How the expressions arrived at
by the various transformations are *related* is via equivalence
relations. 


-- 
---          http://hillview.bugwriter.net/            ---
"Sendmail ist nur der Lackmustest f�r mediokre Admins.
 Du schreibst hin, was du willst, und genau das bekommst du.
 Und wenn du nicht weisst, was du willst, was machst du dann da?"
                  -- Juergen Ernst Guenther in dasr
From: Espen Vestre
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <m1mz3ptz7n.fsf@vestre.net>
Holger Schauer <··············@gmx.de> writes:

> What you were confusing in your other posting are two very different
> things: the relation itself (to which value relates the set 1 and 2)
> and the *test* whether some domain and range values are related (to
> stick with the example, that's the function {{1,2},3}->{true,false}).
> Say that this function ('foo-p') returns indeed true for the given set
> (relation 'foo') and also true for {{1,2},4}. This still doesn't imply
> that 'foo' itself is a function.

Yes it does, as far as the mathematical theory of lambda calculus is
concerned. If you use lambda calculus as your mathematical language,
there is simply no way to distinguish between a relation (e.g. 'foo')
and its characteristic function (e.g. 'foo-p') - the relation IS the
test for membership!  If you instead use axiomatic set theory as your
mathematical language, it's the other way round: Functions are a
special case of relations, which again are a special case of ordered
tuples, which again are a special case of sets.
-- 
  (espen)
From: Harald Hanche-Olsen
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <pcops8kbnai.fsf@shuttle.math.ntnu.no>
+ Espen Vestre <·····@vestre.net>:

| If you use lambda calculus as your mathematical language, there is
| simply no way to distinguish between a relation (e.g. 'foo') and its
| characteristic function (e.g. 'foo-p') - the relation IS the test
| for membership!

Just to expand on this a bit:  I think a common way to express a
boolean value in lambda calculus is as the equivalent two-way if:
In other words,
true  == (lambda (x y) x), while
false == (lambda (x y) y).
(I'm using Lisp notation here, since this is a Lisp group.)
So a relation R is typically used as (R a b x y), where x is chosen if
(a,b) satisfy R, and y is chosen otherwise.
(Also bear in mind that everything is Schoenfinkelized, uh, Curried.)

| If you instead use axiomatic set theory as your mathematical
| language, [...]

Lambda calculus is a fine formalism for talking about computation in
the abstract.  But as a foundation for all of mathematics, it was
rather a failure, was it not?

-- 
* Harald Hanche-Olsen     <URL:http://www.math.ntnu.no/~hanche/>
- It is undesirable to believe a proposition
  when there is no ground whatsoever for supposing it is true.
  -- Bertrand Russell
From: Espen Vestre
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <m1y7n8qqn8.fsf@vestre.net>
Harald Hanche-Olsen <······@math.ntnu.no> writes:

> Lambda calculus is a fine formalism for talking about computation in
> the abstract.  But as a foundation for all of mathematics, it was
> rather a failure, was it not?

At least Church's project was. However, AFAIK some of the modern
constructive mathematics approaches are quite related to lambda
calculus, but I'll shut my mouth now, because this is really far
beyond my knowledge (I just have a faint memory of some of this stuff
being presented at logic seminars in Oslo almost 20 years ago, and I
always thought it was extremely weird :-)).

(Besides its usage in Computer Science, lambda calculus has had a
 strong impact on linguistics)
-- 
  (espen)
From: Andras Simon
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <vcdr6t0mbbi.fsf@csusza.math.bme.hu>
Espen Vestre <·····@vestre.net> writes:

> Harald Hanche-Olsen <······@math.ntnu.no> writes:
> 
> > Lambda calculus is a fine formalism for talking about computation in
> > the abstract.  But as a foundation for all of mathematics, it was
> > rather a failure, was it not?
> 
> At least Church's project was. However, AFAIK some of the modern
> constructive mathematics approaches are quite related to lambda
> calculus, but I'll shut my mouth now, because this is really far
> beyond my knowledge (I just have a faint memory of some of this stuff
> being presented at logic seminars in Oslo almost 20 years ago, and I
> always thought it was extremely weird :-)).

Also working from faint memories: I think these "modern constructive
mathematics approaches" all use typed lambda calculi. Those are very
different from untyped lambda calculus and combinatory logic, which
Church and Curry wanted to use as a foundation of mathematics. 
(Personally, I find the untyped variants much more appealing. Those 
preferring the typed ones inhabit c.l.haskell and c.l.functional :))

Anyway, for the mathematically inclined, Henk Barendregt's astonishing
monograph on untyped lambda calculus is available online. (Or used to
be; I can only find broken links to it now.)

Andras
From: Harald Hanche-Olsen
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <pco4ppvkb3h.fsf@shuttle.math.ntnu.no>
+ Andras Simon <······@math.bme.hu>:

| Anyway, for the mathematically inclined, Henk Barendregt's astonishing
| monograph on untyped lambda calculus is available online. (Or used to
| be; I can only find broken links to it now.)

Top google hit, not broken now at least:

  http://www.andrew.cmu.edu/user/cebrown/notes/barendregt.html

This is all HTML, which makes the formulas sort of unpleasant to
read.  But it's all there.  Possibly a copyright violation ...

-- 
* Harald Hanche-Olsen     <URL:http://www.math.ntnu.no/~hanche/>
- It is undesirable to believe a proposition
  when there is no ground whatsoever for supposing it is true.
  -- Bertrand Russell
From: Andras Simon
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <vcdmz3nmwz1.fsf@csusza.math.bme.hu>
Harald Hanche-Olsen <······@math.ntnu.no> writes:

> + Andras Simon <······@math.bme.hu>:
> 
> | Anyway, for the mathematically inclined, Henk Barendregt's astonishing
> | monograph on untyped lambda calculus is available online. (Or used to
> | be; I can only find broken links to it now.)
> 
> Top google hit, not broken now at least:
> 
>   http://www.andrew.cmu.edu/user/cebrown/notes/barendregt.html
> 
> This is all HTML, which makes the formulas sort of unpleasant to
> read.  But it's all there.  Possibly a copyright violation ...

Unfortunately, it's not The Book, but Chad Brown's notes for it. But a
useful link nevertheless! Following it backwards, I found a proof
assistant written by him in CL
http://gtps.math.cmu.edu/cebrown/scunak/scunak-1.0.tar.gz
So we're back on topic, finally!

Andras
From: John Thingstad
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <op.tncfwyh3pqzri1@pandora.upc.no>
On Tue, 06 Feb 2007 21:10:24 +0100, Raffael Mancini <·······@yahoo.de>  
wrote:

> Hi,
> I´ve been fancying with learning common lisp for some time now. I
> actually read "lisp primer" to some extend some time ago and really
> liked the idea behind the language.
> But do you find it important or helpful to know lambda-calculus in order
> to learn lisp? I´ve lent "An introduction to Lambda Calculi for Computer
> Scientists" by Chris Hankin and read a few Pages of it. It´s damn
> interesting (I´d even call it brain sex ;)) even though it´s a tough  
> read.
> So should I first learn lisp, then about lambda calculus or the other
> way around, or even do something different.
>
> Thanks for your opinions.
>
> Greetings from Munich,
> Raffael Mancini

Tough question! Lambda calculus can help you think functinally and
might help you program mure sucinct Lisp.
On the other hand the ways of Lisp and Lambda Calulus parted a long
time ago. I'm honestly not sure how much it helps.
Lisp in it's current form is not purely functional.
You might want to look at acl2 to get the basic idea.

http://www.cs.utexas.edu/users/moore/acl2/

-- 
Using Opera's revolutionary e-mail client: http://www.opera.com/mail/
From: Pascal Bourguignon
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <87veif3u5s.fsf@thalassa.informatimago.com>
Raffael Mancini <·······@yahoo.de> writes:

> Hi,
> I�ve been fancying with learning common lisp for some time now. I
> actually read "lisp primer" to some extend some time ago and really
> liked the idea behind the language.
> But do you find it important or helpful to know lambda-calculus in order
> to learn lisp? 

Do you find it important or helpful to know atoms in order to learn
micro-biology?


> I�ve lent "An introduction to Lambda Calculi for Computer
> Scientists" by Chris Hankin and read a few Pages of it. It�s damn
> interesting (I�d even call it brain sex ;)) even though it�s a tough read.
> So should I first learn lisp, then about lambda calculus or the other
> way around, or even do something different.

Depends on whether you're more a theorical type who likes nice big
abstract constructions (you could then start with lambda calculus and
implement a purely functional "lisp" and above it a Common Lisp,
perhaps with some additionnal intermediary layers).

Or if you're more pratical, just learn Common Lisp, and read some
about lambda calculus to get the background.  It's interesting to know
about lambda calculus from a philosiphical point of view, to know that
you can "deduce", or implement the whole stateful universe from the
basic notion of function.


But in anycase, it might not be too important, since you can implement
lambda calculus easily in Common Lisp, you can start from any point.

I've got this file I can't find the URL:
------------------------------------------------------------------------
#|
The scene: 1930s, Alonzo's office at Princeton University.

In the beginning, the world was without form, and void.

So Alonzo said, Let there be functions: and there were functions.

And Alonzo saw the functions, that they were good.

And all the rest follows...

* * *

This is an example of embedding the lambda calculus in Common Lisp,
written to accompany a talk presented to the LispNYC user group.
It is not designed to be completely self-explanatory.

By Anton van Straaten, based on traditional LC definitions.
|#

;; zero: \fx . x
(setq zero (lambda (f) (lambda (x) x)))

;; one: \fx . (f x)
(setq one (lambda (f) (lambda (x) (funcall f x))))

;; two: \fx . (f (f x))
(setq two (lambda (f) (lambda (x) (funcall f (funcall f x)))))

;; three: \fx . (f (f (f x)))
(setq three (lambda (f) (lambda (x) (funcall f (funcall f (funcall f x))))))

;; (lambda (f) (lambda (x) (f (f (f x)))))
;; lambda f . lambda x . f(f(f(f(f(x)))))

;; Booleans

;; true: \xy . x
(setq true (lambda (x) (lambda (y) x)))

;; false: \xy . y
(setq false (lambda (x) (lambda (y) y)))

;; not: \b . b false true
(defun not (b) (funcall (funcall b false) true))

;; Pairs

;; pair: \xy. ((z x) y)
(defun pair (h r) (lambda (f) (funcall (funcall f h) r)))

;; fully expanded versions of head and rest (car & cdr):
;;(defun head (p) (p (lambda (h) (lambda (r) h))))
;;(defun rest (p) (p (lambda (h) (lambda (r) t))))

;; versions of head and rest which make 
;; use of correspondence car=true, cdr=false
(defun head (p) (funcall p true))
(defun rest (p) (funcall p false))

;; nil: \f.\xy.x
(defun nil (f) true)

;; null: \L.L\hr.\xy.y
(defun null (L) (L (lambda (h) (lambda (r) false))))

;; lazy-if: this is not lambda calculus, it is required to support 
;; embedding in Lisp.  The x and y arguments must be thunks (i.e. 
;; wrapped in lambda).  The first funcall below is equivalent to 'force'.
(defun lazy-if (b x y) (funcall (funcall (funcall b x) y)))

;; iszero: \n. n (x false) true
(defun iszero (n) (funcall (funcall n (lambda (x) false)) true))

;; succ: \n.\fx. f (n f x)
;; takes a Church numeral, returns that numeral wrapped 
;; with an extra call to its successor function f.
(defun succ (n)
  (lambda (f)
    (lambda (x)
      (funcall f (funcall (funcall n f) x)))))

(setq four (succ three))
(setq five (succ four))

(defun add (m)
  (lambda (n)
    (lambda (x)
      (lambda (y)
        (funcall (funcall m x) (funcall (funcall n x) y))))))

(defun sub (n) (lambda (m) (funcall (funcall m pred) n)))

(defun mult (n) (lambda (m) (funcall (funcall n (add m)) zero)))

(setq zeropair (pair zero zero))

(defun pred (n) 
  (rest (funcall (funcall n 
                          (lambda (x) 
                            (pair (funcall (add (head x)) one) (head x))))
                          zeropair)))

;; relies on (sub x y) >= 0 (non-negative integer arithmetic)
(defun islessequal (x) (lambda (y) (iszero (funcall (sub x) y))))
(defun isgreaterequal (x) (lambda (y) (iszero (funcall (sub y) x))))
(defun isgreater (x) (lambda (y) (not (funcall (islessequal x) y))))
(defun isless (x) (lambda (y) (not (funcall (isgreaterequal x) y))))

;; recursion is done via the applicative order Y-combinator
(defun Y (f)
  ((lambda (x)
     (funcall f (lambda (a) (funcall (funcall x x) a))))
   (lambda (x)
     (funcall f (lambda (a) (funcall (funcall x x) a))))))

;; good old factorial
(setq fact (Y (lambda (f) 
                (lambda (n) 
                  (lazy-if (iszero n) 
                           (lambda () one)
                           (lambda () (funcall (mult n) (funcall f (pred n)))))))))

;; Conversion functions : convert lambda calculus values to CL values for display purposes

(defun to-num (n) (funcall (funcall n #'1+) 0))

(defun to-bool (b) (funcall (funcall b T) nil))

;; Examples

;; calculate factorial of 5 - result is a function (like all LC values)
(setq fact-five (funcall fact five))

;; display fact-five in human readable form
(print (to-num fact-five))

;; now do fact-five minus one
(print (to-num (pred fact-five)))

;; and a simple multiplication: (* 5 3)
(print (to-num (funcall (mult five) three)))

------------------------------------------------------------------------


-- 
__Pascal Bourguignon__                     http://www.informatimago.com/

HEALTH WARNING: Care should be taken when lifting this product,
since its mass, and thus its weight, is dependent on its velocity
relative to the user.
From: S. Robert James
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <1170889804.536391.126140@s48g2000cws.googlegroups.com>
On Feb 6, 3:31 pm, Pascal Bourguignon <····@informatimago.com> wrote:
> HEALTH WARNING: Care should be taken when lifting this product,
> since its mass, and thus its weight, is dependent on its velocity
> relative to the user.

Perhaps my physics is rusty, but I don't think that's true.  The mass
which (appears to) vary with v is the m in F=ma.  But universal
gravitation, AFAIK, is based on rest mass (m sub 0).

(Otherwise, turning on a light bulb would pull us all into it!)

Can any Physics buffs confirm or deny this?
From: Kaz Kylheku
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <1170892123.872166.202850@s48g2000cws.googlegroups.com>
On Feb 7, 3:10 pm, "S. Robert James" <············@gmail.com> wrote:
> On Feb 6, 3:31 pm, Pascal Bourguignon <····@informatimago.com> wrote:
>
> > HEALTH WARNING: Care should be taken when lifting this product,
> > since its mass, and thus its weight, is dependent on its velocity
> > relative to the user.
>
> Perhaps my physics is rusty, but I don't think that's true.  The mass
> which (appears to) vary with v is the m in F=ma.  But universal
> gravitation, AFAIK, is based on rest mass (m sub 0).
> (Otherwise, turning on a light bulb would pull us all into it!)

Photons have mass,  because they have energy. And that mass is why
light is bent by gravity.

Mass is mass: gravitational and inertial mass are the same thing. This
equivalence is a basic postulate in General Relativity.
From: Tim Bradshaw
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <eqdpl1$jjm$2$8300dec7@news.demon.co.uk>
On 2007-02-07 23:48:43 +0000, "Kaz Kylheku" <········@gmail.com> said:

> Photons have mass,  because they have energy. And that mass is why
> light is bent by gravity.

And, of course, they have zero rest mass.
From: Alain Picard
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <87odo5jbs0.fsf@memetrics.com>
"Kaz Kylheku" <········@gmail.com> writes:

> Photons have mass,  because they have energy. And that mass is why
> light is bent by gravity.

Well....  kinda.  I think what most physicists really think
happens (i.e. how they construe the model in their minds) is
that the mass curves the spacetime, and the light is following
the local geodesics.

IIRC if you just use the "equivalent mass" assumption (E/c^2) and
compute the trajectory, you end up being off by a factor of two.
But I might be misremembering.
From: Pascal Bourguignon
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <87wt2tzg5t.fsf@thalassa.informatimago.com>
"S. Robert James" <············@gmail.com> writes:

> On Feb 6, 3:31 pm, Pascal Bourguignon <····@informatimago.com> wrote:
>> HEALTH WARNING: Care should be taken when lifting this product,
>> since its mass, and thus its weight, is dependent on its velocity
>> relative to the user.
>
> Perhaps my physics is rusty, but I don't think that's true.  The mass
> which (appears to) vary with v is the m in F=ma.  But universal
> gravitation, AFAIK, is based on rest mass (m sub 0).
>
> (Otherwise, turning on a light bulb would pull us all into it!)
>
> Can any Physics buffs confirm or deny this?

The point is that usually the relative speed of the object you are
lifting is small, so it's not relativistic.

But if you are careless and give enough acceleration to the object
lifted so it acquires a relativistic relative speed, then its
appearant mass will increase.  On the other hand, if you can
accelerate a macroscopic object from 0 to 0.2c or more 
over 0.5 or 1.0 m, you should be strong enough to handle the added mass.

-- 
__Pascal Bourguignon__                     http://www.informatimago.com/

"Remember, Information is not knowledge; Knowledge is not Wisdom;
Wisdom is not truth; Truth is not beauty; Beauty is not love;
Love is not music; Music is the best." -- Frank Zappa
From: S. Robert James
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <1170893440.160746.82870@k78g2000cwa.googlegroups.com>
On Feb 7, 6:44 pm, Pascal Bourguignon <····@informatimago.com> wrote:
>
> But if you are careless and give enough acceleration to the object
> lifted so it acquires a relativistic relative speed, then its
> appearant mass will increase.

True.  But it's _weight_ won't increase.  That is, the gravitational
force doesn't change.

If it did, the photons, since they are travelling at light speed have
m = infinity, would have infinite gravitational attraction, which they
don't.

(Again, I may be wrong here, my physics is weak)
From: Pascal Bourguignon
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <87hctwzq8z.fsf@thalassa.informatimago.com>
"S. Robert James" <············@gmail.com> writes:

> On Feb 7, 6:44 pm, Pascal Bourguignon <····@informatimago.com> wrote:
>>
>> But if you are careless and give enough acceleration to the object
>> lifted so it acquires a relativistic relative speed, then its
>> appearant mass will increase.
>
> True.  But it's _weight_ won't increase.  That is, the gravitational
> force doesn't change.

I guess what they meant is that the force needed to go on lifting will
be increased as the lifting speed increases.  Since lifting is
vertical, it would "feel" like if the weight increased.  Of course, as
soon as you stop lifting, it recovers its rest mass, and you only need
to hold its normal weight.


> If it did, the photons, since they are travelling at light speed have
> m = infinity, would have infinite gravitational attraction, which they
> don't.
>
> (Again, I may be wrong here, my physics is weak)


-- 
__Pascal Bourguignon__                     http://www.informatimago.com/
        Un chat errant
se soulage
        dans le jardin d'hiver
                                        Shiki
From: Harald Hanche-Olsen
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <pcolkj8bn0q.fsf@shuttle.math.ntnu.no>
+ "S. Robert James" <············@gmail.com>:

| True.  But it's _weight_ won't increase.  That is, the gravitational
| force doesn't change.
|
| If it did, the photons, since they are travelling at light speed have
| m = infinity, would have infinite gravitational attraction, which they
| don't.

But photons are massless (meaning zero rest mass).  Otherwise, their
mass as seen by us would be infinite.  But we do observe that photons
have energy, hence mass.  It's basically a case of zero times infinity
being a finite number.  Perhaps more to the point, photons are bent by
a strong gravitational field, which shouldn't happen if it's the rest
mass that counts.  (Yes, I'm on shaky ground here as well.)


- Harald
From: Harald Hanche-Olsen
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <pcod54kbmnp.fsf@shuttle.math.ntnu.no>
+ Harald Hanche-Olsen <······@math.ntnu.no>:

| But photons are massless (meaning zero rest mass).

Oops, should have read the whole thread before repeating what others
already said.

-- 
* Harald Hanche-Olsen     <URL:http://www.math.ntnu.no/~hanche/>
- It is undesirable to believe a proposition
  when there is no ground whatsoever for supposing it is true.
  -- Bertrand Russell
From: John Thingstad
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <op.tnffkdnqpqzri1@pandora.upc.no>
On Thu, 08 Feb 2007 00:10:06 +0100, S. Robert James  
<············@gmail.com> wrote:

> On Feb 6, 3:31 pm, Pascal Bourguignon <····@informatimago.com> wrote:
>> HEALTH WARNING: Care should be taken when lifting this product,
>> since its mass, and thus its weight, is dependent on its velocity
>> relative to the user.
>
> Perhaps my physics is rusty, but I don't think that's true.  The mass
> which (appears to) vary with v is the m in F=ma.  But universal
> gravitation, AFAIK, is based on rest mass (m sub 0).
>
> (Otherwise, turning on a light bulb would pull us all into it!)
>
> Can any Physics buffs confirm or deny this?
>

sure!

E = h f

where h is plancs constant and f is the frequency.

E = m c^2

(needs no explanation) so

m c^2 = h f

or

m = h f / c^2



-- 
Using Opera's revolutionary e-mail client: http://www.opera.com/mail/
From: Raffael Mancini
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <530hv9F1oj1jfU1@mid.uni-berlin.de>
John Thingstad wrote:
> On Thu, 08 Feb 2007 00:10:06 +0100, S. Robert James
> <············@gmail.com> wrote:
> 
>> On Feb 6, 3:31 pm, Pascal Bourguignon <····@informatimago.com> wrote:
>>> HEALTH WARNING: Care should be taken when lifting this product,
>>> since its mass, and thus its weight, is dependent on its velocity
>>> relative to the user.
>>
>> Perhaps my physics is rusty, but I don't think that's true.  The mass
>> which (appears to) vary with v is the m in F=ma.  But universal
>> gravitation, AFAIK, is based on rest mass (m sub 0).
>>
>> (Otherwise, turning on a light bulb would pull us all into it!)
>>
>> Can any Physics buffs confirm or deny this?
>>
> 
> sure!
> 
> E = h f
> 
> where h is plancs constant and f is the frequency.
> 
> E = m c^2
> 
> (needs no explanation) so
> 
> m c^2 = h f
> 
> or
> 
> m = h f / c^2
> 
> 
> 
> --Using Opera's revolutionary e-mail client: http://www.opera.com/mail/

WRONG! look at this page:
http://math.ucr.edu/home/baez/physics/ParticleAndNuclear/photon_mass.html

Greetings,
Raffael Mancini
From: DS
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <1170950091.515258.135730@k78g2000cwa.googlegroups.com>
>
> WRONG! look at this page:http://math.ucr.edu/home/baez/physics/ParticleAndNuclear/photon_mass....
>

So what is going on in this experiment?

http://www.nytimes.com/2007/02/08/science/08quantum.html?ref=us

-- DS
From: Harald Hanche-Olsen
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <pcohctwbmq3.fsf@shuttle.math.ntnu.no>
+ "DS" <······@riverglassinc.com>:

| So what is going on in this experiment?
|
| http://www.nytimes.com/2007/02/08/science/08quantum.html?ref=us

A lot of very complicated physics, that's what.  8-)

Seriously, nothing in that experiment has a bearing on the behaviour
of photons in a vacuum.

-- 
* Harald Hanche-Olsen     <URL:http://www.math.ntnu.no/~hanche/>
- It is undesirable to believe a proposition
  when there is no ground whatsoever for supposing it is true.
  -- Bertrand Russell
From: John Thingstad
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <op.tnfjm1qrpqzri1@pandora.upc.no>
On Thu, 08 Feb 2007 13:05:10 +0100, Raffael Mancini <·······@yahoo.de>  
wrote:

> John Thingstad wrote:
>> On Thu, 08 Feb 2007 00:10:06 +0100, S. Robert James
>> <············@gmail.com> wrote:
>>
>>> On Feb 6, 3:31 pm, Pascal Bourguignon <····@informatimago.com> wrote:
>>>> HEALTH WARNING: Care should be taken when lifting this product,
>>>> since its mass, and thus its weight, is dependent on its velocity
>>>> relative to the user.
>>>
>>> Perhaps my physics is rusty, but I don't think that's true.  The mass
>>> which (appears to) vary with v is the m in F=ma.  But universal
>>> gravitation, AFAIK, is based on rest mass (m sub 0).
>>>
>>> (Otherwise, turning on a light bulb would pull us all into it!)
>>>
>>> Can any Physics buffs confirm or deny this?
>>>
>>
>> sure!
>>
>> E = h f
>>
>> where h is plancs constant and f is the frequency.
>>
>> E = m c^2
>>
>> (needs no explanation) so
>>
>> m c^2 = h f
>>
>> or
>>
>> m = h f / c^2
>>
>>
>>
>> --Using Opera's revolutionary e-mail client: http://www.opera.com/mail/
>
> WRONG! look at this page:
> http://math.ucr.edu/home/baez/physics/ParticleAndNuclear/photon_mass.html
>
> Greetings,
> Raffael Mancini

lol

-- 
Using Opera's revolutionary e-mail client: http://www.opera.com/mail/
From: Pascal Costanza
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <52s9lcF1n4ufkU1@mid.individual.net>
Raffael Mancini wrote:
> Hi,
> I�ve been fancying with learning common lisp for some time now. I
> actually read "lisp primer" to some extend some time ago and really
> liked the idea behind the language.

> But do you find it important or helpful to know lambda-calculus in order
> to learn lisp? 

No.

> I�ve lent "An introduction to Lambda Calculi for Computer
> Scientists" by Chris Hankin and read a few Pages of it. It�s damn
> interesting (I�d even call it brain sex ;)) even though it�s a tough read.
> So should I first learn lisp, then about lambda calculus or the other
> way around, or even do something different.

This depends whether you are more mathematically oriented and have fun 
juggling around lots of greek letters on paper, or whether you prefer to 
type in code in some command line and see what happens. The former would 
indicate that you should start with lambda calculus, the latter that you 
should start with Lisp.

Pascal

-- 
My website: http://p-cos.net
Common Lisp Document Repository: http://cdr.eurolisp.org
Closer to MOP & ContextL: http://common-lisp.net/project/closer/
From: Alan Crowe
Subject: Re: Lambda-calculus and lisp
Date: 
Message-ID: <86r6szozk4.fsf@cawtech.freeserve.co.uk>
Pascal Costanza <··@p-cos.net> writes:

> Raffael Mancini wrote:
> > I�ve lent "An introduction to Lambda Calculi for Computer
> > Scientists" by Chris Hankin and read a few Pages of it. It�s damn
> > interesting (I�d even call it brain sex ;)) even though it�s a tough read.
> > So should I first learn lisp, then about lambda calculus or the other
> > way around, or even do something different.
> 
> This depends whether you are more mathematically oriented and have fun 
> juggling around lots of greek letters on paper, or whether you prefer to 
> type in code in some command line and see what happens. The former would 
> indicate that you should start with lambda calculus, the latter that you 
> should start with Lisp.

http://www.hulver.com/scoop/story/2006/12/27/181024/91

and

http://www.hulver.com/scoop/story/2006/3/11/122553/217

hint that I am "mathematically oriented and have fun
juggling around lots of greek letters"

However I found lambda calculus very hard. It yielded to
coding implementations in Common Lisp. I found it necessay
to play with higher order functions repeatedly before I was
familiar enough with them to follow what was going on.

I think that the general rule is to work from concrete to
abstract. Since your CL implementation checks your work,
throwing errors or printing the result of the computation you
actually requested (not the one you thought you requested) I
think that typing code in some command qualifies as concrete
and is the starting point for every-one.

Alan Crowe
Edinburgh
Scotland