Lambda Calculus Free Variable Issue

Question

Я нашел Mike Gordon's Введение в функциональное программированиеNotes в сети, и я пытаюсь работать через него. На странице 9 есть этот вопрос:

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] 

Я предполагаю, что я мог бы сказать, что с V1 и V2 равны, мы могли бы повторить его таким образом:

(λ V2 V1 . E) E1 E2 

и поэтому говорят

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

с учетом того, что V2 не является свободным в E1. Но тогда мы не можем сказать

E[E1/V2][E2/V1] 

потому что E2 обязательно будет иметь V1 бесплатно. Или я чего-то не хватает?

Answer 1

Это не контрпример. Кроме того, я не понимаю ваши рассуждения на последнем шаге - почему V1 должен происходить свободно в E2? Кроме того, этот E[E1/V2][E2/V1] на последнем шаге не является инструкцией. Что вы имеете в виду, говоря: «Мы не можем сказать, что E[E1/V2][E2/V1]?»

Вы должны попытаться построить явную контрпример для этой гипотезы, то есть выбрать V1=V2=x (это на самом деле не имеет значения, из-за преобразования а), а затем найти явные выраженияE, E1, E2 таким образом, что они выполняют предположение о гипотезе (V2 не является бесплатным в E1), но выражение `E[E1/V2][E2/V2] не равно восстановлению (λV1 V2. E) E1 E2.

Поскольку вы сказали, что хотите сделать это сами, я не дам вам решение, но вы можете попросить больше указателей.