Problem z ewaluacją wyrażenia

Witam

Mam prostą zagadkę do rozwiązania nie wymagającą znajomości jakiegoś konkretnego języka, ale raczej analitycznego myślenia.
Otoż, piszę interpreter własnego języka funkcyjnego i natrafiłem na problem przy ewaluacji wyrażeń.

Powiedzmy, że składnie wyrażeń tego języka to
Lit = 0, 1, -1, 2, -2, ... # literały
Var = a, b, c, ... # są to zmienne o identyfikatorach ze zbioru Ident
Exp ::= Lit | Var | Exp1 + Exp2 | Exp1 - Exp2 | Exp1 * Exp2 | \ Ident -> Exp | Exp1 Exp2 | let Ident = Exp1 in Exp2 |
if Exp1 then Exp2 else Exp3 | (Exp1, Exp2)
Już wyjaśniam czym może być wyrażenie:

1. Może byc literałem np. 20, -7, 0
2. Może być zmienną np. x
3. Może być wyrażeniem arytm. 1+ 2, x * 7
4. Może być wyrażeniem warunkowym np. if x then 7 + x else 3 , czyli jeżeli x nierówny 0 to powiększ go o 7 a jeżeli x = 0 to daj 3
5. Może być lambda abstrakcją (nienazwaną funkcją) np. \x -> x + 1
6. Może być aplikacją do lam. abs. np. (\x -> x + 1) 7 w wyniku da 8
7. Może też być lokalną definicją let x = e1 in e2 , która oblicza wartość e1 i przypisuje ją na zmienną x a następnie w tak zmodyfikowanym środowisku oblicza e2 np. let x = 7 in x * 2 da w wyniku 14
8. Ostatecznie może być to para np. (1, 3) czy (\x -> x, 12)

Powiedzmy , że chcę najpierw zdefiniować sobie funkcję identycznościową id co mogę zrobić np. tak
id = \x -> x
Teraz chciałbym obliczyć coś takiego f = (\x -> \id -> (x, id) ). Jest to funkcja biorąca 2 argumentu i zwracająca parę
np. f 1 2 da w wyniku (1, 2), f (\x -> x + 1) 7 da (\x -> x +1, 7).
Niby nic szczególnego, ale teraz chcę zrobić coś takiego f id 7 (id jest cały czas zdefiniowana w środowisku).
Spodziewałbym się wyniku podobnego do ostatniego przykładu, czyli (id, 7), ale otrzymam (7, 7).
Jak ewaluuję (\x -> \id -> (x, id) ) id 7 ==> (\id -> (id, id) ) 7 ==> (7, 7).
Tu własnie jest ten problem z kolizją nazw. Przed zaaplikowaniem argumentu do lam. abs. muszę przezwać zmienne związane w lambda abstrakcjach np. (\x_$111 -> \id_$112 -> (x_$111, y_$112) ) id 7 (dalekie skojarzenie z name mangling).

Teraz sedno problemu: Wiem, że dla lam. abs. i aplikacji to zadziała, ale mam jeszcze lokalne definicje let ... in ...
i obawiam się, że tu też jest ten problem. W wyrażeniu let x = e1 in e2 mógłbym próbować przezwać x i wszystkie jego wystąpienia w e2, ale tu jest jeszcze gorszy problem: let'y mogą być zagnieżdzone i np. w e2 może być coś takiego jak ... lam x = e3 in e4 ... i teraz nie mogę na ślepo przezywać x, bo x = e1 jest czymś innym niż x = e3 z wnętrza.

Nie jestem pewien czy jak będę szedł od zewnątrz i zamieniał nazwy w let'ach przez dopisywanie $111, $112, ... to czy
takie coś wystarczy np. let x = 7 in let x = x + 7 in x * 2 i teraz przepisania:
pierwsze: let x$100 = 7 in let x$100 = x_$100 + 7 in x_$100 * 2
drugie: let x_$100 = 7 in let x_$100_$101 = x_$100 + 7 in x_$100_$101 * 2

1. Czy Waszym zdaniem takie przepisywanie niczego nie zepsuje?

2. Czy widzicie jeszcze jakieś ukryte problemy, których takie przepisywania nie obejmują?

Z góry dziekuję za pomoc.

Pozdrawiam

Adam

Znalazłem kolejny problem.
W tym moim języku wymyśliłem sobie, że będę miał wiązania statyczne i z taką lambda abstrakcją muszę przechowywać środowisko z chwili definiowania.
W takim razie muszę też przepisywać nazwy z domknięcia.
Widzicie jeszcze jakieś zagrożenia?

A w której chwili to ewaluujesz? Co np. wg ciebie powinno być wynikiem

let x = 10;;
let f -> x+10;;
let x = 11;;
f;; (*20 czy 21?*)

Czy zakładasz ze wiążesz z ostatnim wystąpieniem czy z wystąpieniem w chwili deklaracji?

Wiążę nazwy z chwili deklaracji, czyli późniejsze zmiany nie mają znaczenia (nawet typ może być inny).