CODEWITHSUNDEEP
lambda-calculus
user2054900
user2054900

Reputation: 341

Lambda Calculus Free Variable Issue

I found Mike Gordon's Introduction to Functional Programming Notes on the web and I'm trying to work through it. On page 9 there's this question:

Find an example to show that if V1 = V2 , then even if V2 is not free in E1,
it is not necessarily the case that:

(λ V1 V2 . E ) E1 E2 = E [E1/V1][E2/V2]

I'm guessing that I could say that since V1 and V2 are equal, we could redo it thus:

(λ V2 V1 . E ) E1 E2

and therefore say 

(λ V1 . E[E1/V2] ) E2

given the stipulation that V2 is not free in E1. But then we cannot say

E[E1/V2][E2/V1]

because E2 would necessarily have V1 free. Or am I missing something?

Upvotes: 1

Views: 145

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8258

This is not a counterexample. Apart from that, I don't understand your reasoning in the last step – why does V1 have to occur freely in E2? Apart form that, this E[E1/V2][E2/V1] in your last step is not a statement. What do you mean by saing "We cannot say that E[E1/V2][E2/V1]?"

You should try to construct an explicit counterexample for this hypothesis, i.e. choose V1=V2=x (it really doesn't matter, due to α conversion) and then find explicit expressions E, E1, E2 such that they fulfil the assumption of the hypothesis (V2 not free in E1), but the expression `E[E1/V2][E2/V2] is not equal to the reduct of (λV1 V2. E ) E1 E2.

Since you said you wanted to do this by yourself, I will not give you the solution, but feel free to ask for more pointers.

Upvotes: 1

Related Questions