Last Lecture (Lambda Calculus)

BastiS
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 224
Registriert: 3. Nov 2005 19:12
Kontaktdaten:

Last Lecture (Lambda Calculus)

Beitrag von BastiS »

I just reviewed the contents of last lecture and I do have a problem while finding the conclusion of this lecture.... (already had it during the lecture but hoped it's understandable when recapulating it):

On slide 18 it's written "Can we get rid of define?"

Then it's explained how to build recursion without "define" - as I understood the \(\equiv\)-construct right it's just used here to show that we don't define functions rather use them directly when needed. So we also have to type them multiple times because we don't have a name for them any longer. Am I right so far?

But then on page 27ff when fixpoint combinator was introduced, we use a define-construct again? So isn't it possible to get rid of define at all?

Would be very heldful to get an answer - maybe here or maybe in the final lecture.

Benutzeravatar
sewe
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 295
Registriert: 16. Jan 2009 14:53
Kontaktdaten:

Re: Last Lecture (Lambda Calculus)

Beitrag von sewe »

So we also have to type them multiple times because we don't have a name for them any longer. Am I right so far?
No, not quite. We do have identifiers and function literals and function applications; thus, we can use the old with preprocessor trick to name things.

BastiS
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 224
Registriert: 3. Nov 2005 19:12
Kontaktdaten:

Re: Last Lecture (Lambda Calculus)

Beitrag von BastiS »

Ah, ok - that's right, I've overseen this possibility. But what's about the define-thing?

Benutzeravatar
sewe
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 295
Registriert: 16. Jan 2009 14:53
Kontaktdaten:

Re: Last Lecture (Lambda Calculus)

Beitrag von sewe »

But what's about the define-thing?
Hm, if you want to know how to define a named, recursive function (what define allows us to do), it goes like this: first, use the Y-combinator to define make a recursive function and then name it with with; your named, recursive function is then available in the body of the with. But I am not sure whether I have understood your question correctly.

Pavel
Windoof-User
Windoof-User
Beiträge: 37
Registriert: 21. Okt 2006 23:42

Re: Last Lecture (Lambda Calculus)

Beitrag von Pavel »

I also have a question regarding this. I followed you until slide 23, but there I am stuck. So ≡ can be thought as a define without recursion, right?

How can we then get there:

Code: Alles auswählen

((lambda (mk-fact) (mk-fact mk-fact))
--- all open brackets closed here --
  (lambda (f)
   (lambda (n)
     (if (zero? n)
     1
     (* n ((f f) (sub1 n)))))))
Did you probably mean:

Code: Alles auswählen

(define* fact (mk-fact mk-fact))
--- all open brackets closed here --
(define* (mk-fact f) 
  (lambda (f)
   (lambda (n)
     (if (zero? n)
     1
     (* n ((f f) (sub1 n)))))))
where define* would be ≡ ?

Benutzeravatar
sewe
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 295
Registriert: 16. Jan 2009 14:53
Kontaktdaten:

Re: Last Lecture (Lambda Calculus)

Beitrag von sewe »

Yes, you can think of ≡ as define. It is, however, not part of our language, but rather a way for us to name expressions for the purpose of presentation. At any rate, the critical part is in line 2 of the following:

Code: Alles auswählen

((lambda (mk-fact) (mk-fact mk-fact))
--- all open brackets closed here --
  (lambda (f)
   (lambda (n)
     (if (zero? n)
     1
     (* n ((f f) (sub1 n)))))))
Your statement, namely that all open brackets [are] closed here is not correct; the function mk-fact is ≡'ed in the upper part of slide 23 is used as an input to the following lambda:

Code: Alles auswählen

(lambda (mk-fact) (mk-fact mk-fact))
The overall expression would then be fact. That being said, your alternative interpretation does essentially do the same thing, but it defines names as well.

Antworten

Zurück zu „Archiv“