Takze mam po skuske a som rad, ze to mam za sebou
O1:Netypovany lambda kalkul, definicia, vyhodnotenie
O2:Konstrukcia let, definicia, vyuzitie
Pr.Dokaz, ze |consts(t)|<=size(t).
Skusal ma Mihaly, priklad som celkom mal a aj on bol spokojny. Sem tam nejaka otazka na doplnenie ale ok. Konstrukcia let som si len par veci pamatal, nieco som si aj zle pamatal, no naviedol ma na spravny smer a tak som to nejak celkom ok dopovedal potom. A Lambda kalkul som si pomylil s NBL a vsetko o NBL som pisal.. A potom mi povedal ze syntax je ta ista len nieco chyba v lambda kalkule. Uplne mi vypadlo, no potom som tam dal, ze je tam abstakcia a este ze tam ma byt tt. A este sa spytal, ze do kedy redukujeme term. Tiez som nevedel.. Okno.. No pomohol mi a bola to proste hodnota. A tak sumarum ze priklad bol dobre, konstrukcia let tiez a ze na kalkul som nakoniec prisiel, tak ci staci Bcko. a ja ze samorejme. Takze B(82). Drzim prsty!!!
A este co som si vsimol otazky od vedla:
Pr. urobit typovaci strom a konstany z termu...
Otazka: Detypovanie(erase), definicia a asi vyuzitie
