###### tags: `MP`
# tercja III, wykład 2

## Dokładamy zmienne do języka

### Idea

W najpostszej wersji dokładanie zmiennych można zrobić instrukcją let.

Jeśli będziemy dokładać funkcje do języka to będzie tu wyglądało prawie u=identycznie jak mechanizm wiązania zmiennych.

Na razie (w wersji z wykładu) mamy `let` z pojedynczym wiązaniem, czyli `{let x 1 {+ x 1}}`.

1. Jaki jest zasięg wiązania? (scope)
2. Co to znaczy, że x zostanie związany z wartością tego wyrażenia?
3. Czy nazwa x ma znaczenia (i jak nie ma, to jak to można wykorzystać)?
Wyrażenia `{let x 1 {+ x 1}}` i `{let y 1 {+ y 1}}` prawdopodobnie powinny być równe ($\alpha$-równoważność). Musimy to mieć na uwadze. **ALE jeśli mamy `{let x z {+ x 1}}` to nie możemy zmienić `z` na `z'`**

### O parserze nie opowiadamy, tam się nic specjalnego nie dzieje.

### Więcej o zasięgu wiązania

Zdefiniujemy sobie funkcję, która zwraca zmienne wolne z wyrażenia. Do tego użyjemy zbiorów (listy opakowane, żeby ładniej się na to patrzyło).

1. Jak mamy zmienną wolną to dodajemy do zbioru.
2. Jak mamy `{let x e1 e2}` to dodajemy z e1 i (e2 z usuniętym x)

Zauważmy, że jak mamy coś takiego:

{let x 2
	{let x x 1}}

to wbrew pozorom nie ma problemu (bo i tak ten x zostanie dodany).

To mamy już co wiążemy.

### Co to znaczy związać x z wartością wyrażenia?

Ewaluator z wykładu jest tak zrobiony, jak się tego nie pisze, ale jest dobry do rozważań teoretycznych.

Zakładamy, że ewaluator jest uruchomiony na zamkniętym wyrażeniu (nie ma zmiennych wolnych w naszym wyrażeniu). Więc jak będą takie, to rzucamy błąd.

Interpreter będzie działać tak, że zadba, żeby nie powstało wyrażenie ze zmiennymi wolnymi. Robimy to tak, że liczymy wartość tego, co mamy podstawić a następnie robimy z tego wyrażenie.

To co mamy nie działało by w takim przypadku:
Podstawiamy za y x:

{let x 1 {+ y x}} ; -> {let x 1 {+ x x}} a to nie to co chcieliśmy

;jak przemoanujemy x na z:
{let z 1 {+ y z}} ;-> {let z 1 {+ x z}}

Rozwiązanie: zmiana nazwy zmiennej (zanim dokonamy podstawienia)

### Co teraz?

Przez `let` mamy problem taki, że nasze wyrażenie nie jest już takie jak wcześniej (trawersujemy wyrażenia) i przez to nie możemy robić już indukcji strukturalnej.

## Środowisko

Wprowadzamy środowisko rozumiane trochę jako odroczone podstawienie zmiennych. W środowisku trzymamy też inne rzeczy, na przykład procedury racketowe czy inne rzeczy.

Dla naszego języka z wykładu środowisko będzie wiązać nazwy zmiennych z wartościami.

Nasze środowisko to będą listy (listy wiązań, czyli symbol + wartość).

Będziemy potrzebować:
* puste środowisko
* rozszerzanie środowiska (dołożenie wiązania)
* szukanie nazwy w środowisku

### Zmienia nam się sygnatura funkcji eval

**Od teraz nie będzemy już się pozbywać środowiska z eval.**

1. Numer, operator i if wyglądają podobnie (tylko jak trzeba to przekazujemy środowisko)
2. jak mamy zmienną to zastępujemy jej wartością
3. jak mamy let to:
* liczymy wartość
* dodajemy do środowiska zmienną i wartość
* drugą część ewaluujemy z rozszerzonym środowiskiem

Będzie działać dobrze, ponieważ środowisko zwraca najnowszą "deklarację" danej zmiennej (przez to, jak to zaprogramowaliśmy), więc najnowsze nadpisanie będzie zwracane, więc to co chcemy.

### Jak powinna działać $\alpha$-równoważność?

1. Jak dwie rzeczy mają różną strukturę, to wiadomo, że są różne
2. Co jeśli mają podobną strukturę?
* Przykład: `{+ x 1}` i `{+ y 1}` nie musza być równoważne, ale jeśli mamy `{let x 2 {+ x 1}` oraz `{let y 2 {+ y 1}` są równoważne
* Potrzebujemy coś w postaci środowiska, co by nam zapamiętało połączenia między zmiennymi

**Ważne** nie można bezmyślnie zamienić nazw z jednego z drugim, bo problem jest taki, że możemy mieć użytą w drugim zmienną z taką nazwą i zacznie się psuć (trzeba uważać albo coś)

### Co się dzieje w takim przypadku?

Start:

{let x 1
	{let y x}
		{let z x {+ z y}}}

`[]` - puste środowisko

Co się dzieje ze środowiskiem?

`[]`
`[(x, 1)]`
`[(y, 2), (x, 1)]`
`[(z, 1), (y, 2), (x, 1)]`

Może wystarczy, że będziemy myśleć o tym, który element listy musimy pobrać?

Może skoro nazwy nie mają znaczenia to możemy się ich pozbyć? Zapisywalibyśmy wtedy tylko informację, z którego miejsca mamy wziąć naszą watość.

### Bez "zmiennych"

Będziemy sobie zapisywać jak daleko mamy wartości od naszego bindera, czyli nasz poprzedni przykład wyglądałby tak:

{let x 1
	{let y 2
		{let z x {+ z y}}}}
		
{let 1
	{let 2
		{let (ind 1) 
			{+ (ind 0) (ind 1)}}}}; indeksy de Bruijn'a (/de brauna/)
			

Wtedy nasze środowisko to: `[1, 2, 1]`

Tego się używa w kompilatorach, jak chcemy się pozbyć zmiennych.

Podstawenie na indeksach jest nieprzyjazne, więc nie robimy tego.

Jak przetłumaczymy dwie rzeczy to jesteśmy w stanie powiedzieć, czy dane wyrażenia są takie same (mamy dobrą definicję $\alpha$-równoważności).

## Jak mamy już let-y to możemy też mieć lambdy

Przy lambdach najpierw wyliczamy wartość, którą wstawiamy do lambdy a potem coś tam dalej zrobimy. Moglibyśmy też go nie liczyć i będzemy to wyrażenie liczyć zawsze, gdy będzie nam potrzebna wartość x.

## A co z funkcjami?

Funkcja ma brać wartośc i zwracać wartość (value będzie wtedy typem w rekurencyjnym).

## Ciekawy przypadek:

`{lambda (x) {x x}}` jest jeszcze spoko, ale
`{{lambda (x) {x x} {lambda (x) {x x}}` już się zapętli.
Ale można coś tutaj dołożyć (w przyszłym tygodniu to zrobimy) i będzie można dzięki temu wyrazić rekursję.

"Taka aplikacja {x x} jest źródłem zła, ale możemy sobie z tego zła wyciąć coś co będzie nam służyć"

Na kolejnym wykładzie będzie "jak nie oszukiwać", czyli jak interpretować funkcje bez użycia lambdy z metajęzyka i używając tylko prostszych wyrażeń.