---
title : Wyklad 11,12
---
Zmienna wolna i zamknięty term.
Wszytkie zmienny, które nie są w let, są wolne.
Czyli jeżeli nasz ewaluator napotka zmienną, to znaczy ża nasza zmienna jest wolna

(define (eval [e : Exp]) : Value
  (type-case Exp e
    [(numE n) (numV n)]
    [(trueE) (boolV #t)]
    [(falseE) (boolV #f)]
    [(opE o l r) ((op->proc o) (eval l) (eval r))]
    [(ifE b l r)
     (type-case Value (eval b)
       [(boolV v)
        (if v (eval l) (eval r))]
       [else
        (error 'eval "type error")])]
    [(varE x)
     (error 'eval "unbound variable")]
    ))

A dlaczego napotkanie zmiennej w ewaluatorze, będzie oznaczalo, że to jest zmienna wolna?
Dlatego, że interpretacja let'a jest taka, że zmienną, którą on wiążę, zostanie zastąpione zamlniętym wyrażeniem.

Patrzymy jak jest obliczany *let*

[(letE x e1 e2)
     (let ([v1 (eval e1)])
       (eval (subst e2 x (value->exp v1))))]

Zauważymy tą *metacykliczność* : używam let'a, żeby zinterpretować let'a.
Obliczamy wyrażenie e1.
I to co teraz zrobimy z wyrażeniem e2, w którym wiemy, że *x* może mieć wolne wystąpienie. Cała rzecz, żeby miał :)
Zastąpimy *x* wyrażeniem, które reprezentuje wartość e1.
I jak to podstawienie się uda, to dostaniemy nowe wyrażenie, i to wyrażenie damy ewaluotorowi.

1) Dlaczego wykonujemy koercję (konwertowania) wartości do wyrażenia? *(value->exp v1)*
Chcemy operować na składni. Nasz ewaluator liczy wartości wyrażeń, które są reprezentowanie typem **Value**
Jak się doliczymy się do Value, to teraz potrzepujemy podstawienie. Ale my za zmienne w wyrażeniach będziemy podstawiać nowe wyrażenia, więc potrzebujemy przkształcić nasze wartości na Value.
2) Operacja podstawienia:
e - wyrażenie za które będziemy podstawiać
x - zmienna za którą bedziemy podstawiać
a - wyrażenie, które bedziemy podstawiać

;; precondition: a is a closed expression
(define (subst [e : Exp] [x : Symbol] [a : Exp]) : Exp
  (type-case Exp e
    [(numE n)
     (numE n)]
    [(trueE)
     (trueE)]
    [(falseE)
     (falseE)]
    [(opE o l r)
     (opE o (subst l x a) (subst r x a))]
    [(ifE b l r)
     (ifE (subst b x a) (subst l x a) (subst r x a))]
    [(varE y) 
     (if (eq? x y) a (varE y))]
    [(letE y e1 e2)
     (let ([e1-new (subst e1 x a)]
           [e2-new (if (eq? x y)
                       e2
                       (subst e2 x a))])
       (letE y e1-new e2-new))])
       

* (varE y)
Jeżeli x $\neq$ y, to znaczy, że y może występować w innym letcie, i nie dotykam tej zmiennej.
* (letE y e1 e2)
Ponieważ *y* (który tu wiążemy) nie jest widoczyny w *e1*,
to shodzimy rekrencyjnie w e1, otrzymując jakieś nowe wyrażenie e1-new.
Natomiast w e2, zaczynamy wchodzić pod nowy binder(wiązanie). I to co chcemy sprawdić czy x = y.
To znaczy, żw wszystkie wystąpienia x w e2 nie są wolne, one są związane przez let'a ktorego teraz analizujemy
Natomiast jesli $/neq$ to schodzimy sobie rekurencyjnie do e2 z tym podstawieniem

*Kiedy może dojść do podstawienia?*
Wtedy, gdy podstawiamy za zmienna, ktora ma w dannym wyrażeniu wolne wystąpienie
> (subst (parse '{let x 2 {let x 1 x}}) 'x (parse '42))
> > (letE 'x (numE 2) (letE 'x (numE 1) (varE 'x)))

Czyli podstawienie 42 zostało zignorowane.
Tutaj *x* wolnych wystąpień nie posiada, dlatego że

'{let x 2 {let x 1 **x**}}) 'x (parse '42)
Za ten x moglibysmy cos wstawic. Ale ten x jest zwiazany prze wystapienie wiazace, jest chroniony przed podstawienie
A tu *y* nie jest zwiazany:
> (subst (parse '{let x 2 {let x 1 y}}) 'y (parse '42))
> >(letE 'x (numE 2) (letE 'x (numE 1) (numE 42)))

### Przechwycenia zmiennej
> (subst (parse '{let x 1 y}) 'y (parse 'x))
(letE 'x (numE 1) (varE 'x))
Konstrukcja wiążąca zmienna przechwytuje do swojego zasięgu wiązania zmienną **x**, ktora w tym wyrazeniu, nie jest zwiazana.

Operacja podstawienia przechodzi cale wyrazenie az to liści. To wyrażenie może być dowolne duże, i my musimy znależć gdzie są te zmiennem za które powinnismy podstawić.
To jest operacja NIEEFEKTYWNA!

Jak nie podstawienie to co? **Środowisko**

### Indeksy de'Brauna

Liczymy stopień zagniezdzenia let'ów. Nie potrzebujemy juz nazw zmiennych
A zmienna jest reprezentowana, jako konstruktor, ktory bierze ten adres (liczba). Czyli jak daleko jestem od mojego let'a?

## Domknięcia (reprezentacja procedur)
Zamiast budować procedury, jako funkcje z meta języka, będziemy budować domknięcia.

(define-type Value
  (numV [n : Number])
  (boolV [b : Boolean])
  (funV [x : Symbol] [e : Exp] [env : Env]))

x - nazwa parametru formalnego
e - ciało procedury
env - środowisko w którym jest wywoływana funkcja
Gdybyśmy tego środowiska tam nie dołożyli, to nasz interpreter implementowałby **"dynamiczne wiązanie zmiennych"**, czyli funkcja nie zapamietuje wartosci i siega po nie w momencie aplikacji.
Jednak chcemy mieć **"statyczne wiązanie zmiennych"**, czyli
Funkcja zapamiętuje wartości zmiennych wolnych z momentu swojej definicji, i te wartości wykorzystuje pózniej gdy jest aplikowana

##### Rekurencja
Nie skończywszy danej definicji, już jej używamy. "Samoodniesienie"

(define (fact n)
  (if (= n 0)
      1
      (* n (fact (- n 1)))))