## Exam Check-List: Discussion on Part 09 - Lambda Calculus

FeG
Endlosschleifenbastler Beiträge: 182
Registriert: 6. Dez 2007 07:01

### Exam Check-List: Discussion on Part 09 - Lambda Calculus

Hi,

here is my solution to the ninth topic of the exam check-list (-> spoiler alert...).

Best,
Felix

1. What types of expressions are present in the lambda calculus. Deﬁne a deﬁnition of the [concrete/abstract] syntax of the lambda calculus.

Present expressions:
* function definition / lambda expressions
* function application
* identifiers

Concrete Syntax:

Code: Alles auswählen

<LC> ::= {fun {<id>} <LC>}
| {<LC> <LC>}
| <id>

Abstract Syntax:

Code: Alles auswählen

(define-type LC
[fun (param symbol?) (body LC?)]
[app (fun-expr LC?) (arg-expr LC?)]
[id (name symbol?)])

2. Encode given [boolean values/numbers/pairs/lists] and given operations on these values in the lambda calculus.

Encoding of values:

Code: Alles auswählen

#t         -> (lambda (l r) l)
0          -> (lambda (f) (lambda (x) x))
2          -> (lambda (f) (lambda (x) (f (f x))))
pair (0,1) -> (lambda (sel) (sel #0 #1))   ;; where #0, #1 are the encodings of 0 and 1, respectively
'()        -> (lambda (c n) n)
'(0 1 2)   -> (lambda (c n) (c 0 (c 1 (c 2 n))))

Operations:

Code: Alles auswählen

(define succ (lambda (n)
(lambda (f) (lambda (x) (f ((n f) x))))))

(define sum (lambda (n) (lambda (m)
((m succ) n))))

(define prod (lambda (n) (lambda (m)
(lambda (f) (lambda (x) ((n (m f)) x))))))

(l (lambda (c n) c) null)))

(define append (lambda (l1 l2)
(lambda (c n) (l1 c (l2 c n)))))

3. Deﬁne the major property of the ﬁx-point operator (Y-combinator).

The major property of a fix-point combinator FIX is that it computes the fix-point of the function given as argument, i.e., for any function g it holds that g(FIX(g)) = FIX(g).
4. Use the given ﬁx-point operator to implement the speciﬁed recursive function.

Fix-point operator:

Code: Alles auswählen

(define Y
(lambda (f)
((lambda (x) (f (lambda (v) ((x x) v))))
(lambda (x) (f (lambda (v) ((x x) v)))))))

Recursive function:

Code: Alles auswählen

(define (length lst)
(if (empty? lst)
0
(+ 1 (length (rest lst)))))

Implementation using fix-point operator:

Code: Alles auswählen

(define length-f
(Y (lambda (f) (lambda (lst)
(if (empty? lst)
0
(+ 1 (f (rest lst))))))))

5. Which of the given ﬁx-point operators are correct? Prove it. Which of them support [eager evaluation/call-by-value semantics]?

Fix-point operators A and B:

Code: Alles auswählen

(define A
(lambda (f)
((lambda (x) (f (lambda (v) ((x x) v))))
(lambda (x) (f (lambda (v) ((x x) v)))))))

(define B
(lambda (f)
(f f)))

A is correct:

Code: Alles auswählen

A(g)
= ((lambda (x) (g (lambda (v) ((x x) v)))) (lambda (x) (g (lambda (v) ((x x) v)))))
= (g (lambda (v) (((lambda (x) (g (lambda (v) ((x x) v)))) (lambda (x) (g (lambda (v) ((x x) v))))) v)))
= (g (lambda (v) ((g (lambda (v) (((lambda (x) (g (lambda (v) ((x x) v)))) (lambda (x) (g (lambda (v) ((x x) v))))) v))) v)))
= ...

... I don't see why this is = g(A(g)), but I know A is correct (used above...) :-/

B is incorrect:

Code: Alles auswählen

B(g)
= (g g)
!= g((g g))
= g(B(g))


On the second part of the question: How do you see whether a fix-point operator supports eager evaluation resp. call-by-value semantics? (@Andreas)

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

### Re: Exam Check-List: Discussion on Part 09 - Lambda Calculus

FeG hat geschrieben: A is correct:
... I don't see why this is = g(A(g)), but I know A is correct (used above...) :-/
Let me redo the derivation, as I think the last step went wrong:

Code: Alles auswählen

A(g)
= ((lambda (x) (g (lambda (v) ((x x) v))))
(lambda (x) (g (lambda (v) ((x x) v)))))
= (g (lambda (v) (((lambda (x) (g (lambda (v) ((x x) v))))
(lambda (x) (g (lambda (v) ((x x) v))))) v)))
= ...

Now you make use of the fact that (lambda (x) (f x)) is equivalent to f and then apply the definition of fix:

Code: Alles auswählen

...
= (g ((lambda (x) (g (lambda (v) ((x x) v))))
(lambda (x) (g (lambda (v) ((x x) v))))))
= (g (fix g))

This completes the proof.

Note that the last two steps are not derivation steps (as an interpreter would take them) but rather abstract equivalence arguments.
FeG hat geschrieben: On the second part of the question: How do you see whether a fix-point operator supports eager evaluation resp. call-by-value semantics? (@Andreas)[/list]
Regarding the second part of the question, you have to see whether your proof/derivation works when the order of evaluation is that required by eager evaluation. If it does, then the fix-point operator in question supports eager evaluation.

FeG
Endlosschleifenbastler Beiträge: 182
Registriert: 6. Dez 2007 07:01

### Re: Exam Check-List: Discussion on Part 09 - Lambda Calculus

sewe hat geschrieben:This completes the proof.

Note that the last two steps are not derivation steps (as an interpreter would take them) but rather abstract equivalence arguments.
Okay, i assumed it had to be completely derivational, with this application argument I think I got it..
FeG hat geschrieben: On the second part of the question: How do you see whether a fix-point operator supports eager evaluation resp. call-by-value semantics? (@Andreas)[/list]
Regarding the second part of the question, you have to see whether your proof/derivation works when the order of evaluation is that required by eager evaluation. If it does, then the fix-point operator in question supports eager evaluation.
Could you restate the second half of the sentence; I didn't get the "when the order of evaluation is that required by eager evaluation".

Concerning call-by-value semantics: Are there combinators that work with call-by-reference?

Best,
Felix