Pro informaci ostatnich.
Dneska jsem byl na zkousce a mel jsem dokazat, ze je lambda kalkul bezesporny.
Delal jsem to tak, jak je na slidech, tzn. pomoci Church-Rosserovy vety.
Pak se me jeste zeptal, jak by se to dokazalo v lambda kalkulu, kde neplati Chuch-Rosserova vlastnost, to jsem nevedel. Rekl jsem jen, ze na prednasce rikal, ze nejvetsi prinos te vety byl prave v tom, ze to byl prvni zpusob, jak dokazat, ze je ten lambda kalkul bezesporny. Tak mi rekl, ze se to musi delat pomoci semantiky, pak uz mi doslo, ze je potreba sestrojit model (jestli se tomu tady taky tak rika) a dokazat to pomoci nej.
BTW lambda kalkuly, kde ten Church-Rosser neplati pry fakt existuji, aspon to rikal :)
