22 - Práce v lambda kalkulu (reprezentace čísel a pravdivostních hodnot a operací nad nimi).
pondělí 21. května 2018
17:14
(Reprezentace čísel a pravdivostních hodnot a operací nad nimi)
Reprezentace pravdivostních hodnot a operací nad nimi
Hodnoty true a false si můžeme definovat následujícím způsobem:
𝐿𝐸𝑇 𝑇𝑟𝑢𝑒=𝜆𝑥𝑦.𝑥
Po aplikaci β redukce nám tedy zůstane jen 𝑦 nebo 𝑥.
Pak operace NOT nad nimi je definovaná následujícím způsobem:
LET Not=λt.t False True
Tedy pokud byla vstupní hodnota True, tak se vrátí False (1. hodnota) a pokud byla vstupní hodnota False, tak se vrátí 2. hodnota, tedy True.
Příklad: 
Not True=λt.t False TrueTrue→𝛽𝑇𝑟𝑢𝑒 𝐹𝑎𝑙𝑠𝑒 𝑇𝑟𝑢𝑒→𝜆𝑥𝑦.𝑥 𝐹𝑎𝑙𝑠𝑒 𝑇𝑟𝑢𝑒→𝛽𝜆𝑦.𝐹𝑎𝑙𝑠𝑒𝑇𝑟𝑢𝑒→𝛽𝑭𝒂𝒍𝒔𝒆 
Další operace pravdivostních hodnot
AND
OR
NOR
Převrácený OR. Tedy pokud jsou obě hodnoty False, tak se vrátí True.
T
T
F
T
F
F
F
T
F
F
F
T
NAND
Vrať False pokud je na vstupu True a True.
T
T
F
T
F
T
F
T
T
F
F
T
IMP
T
T
T
T
F
F
F
T
T
F
F
T
EQ
T
T
T
T
F
F
F
T
F
F
F
T
XOR
T
T
F
T
F
T
F
T
T
F
F
F
IF/THEN/ELSE
Příklady
𝐀𝐍𝐃 𝐓𝐫𝐮𝐞 𝐅𝐚𝐥𝐬𝐞→𝜆𝑢𝑣.𝑢𝑣 𝐹𝑎𝑙𝑠𝑒True False→True False False→λxy.x False False→False
𝑶𝑹 𝑭𝒂𝒍𝒔𝒆 𝑻𝒓𝒖𝒆→𝜆𝑢𝑣.𝑢 𝑇𝑟𝑢𝑒 𝑣 𝐹𝑎𝑙𝑠𝑒 𝑇𝑟𝑢𝑒→𝜆𝑣.𝐹𝑎𝑙𝑠𝑒 𝑇𝑟𝑢𝑒 𝑣𝑇𝑟𝑢𝑒→𝐹𝑎𝑙𝑠𝑒 𝑇𝑟𝑢𝑒 𝑇𝑟𝑢𝑒→𝜆𝑥𝑦.𝑦𝑇𝑟𝑢𝑒 𝑇𝑟𝑢𝑒→𝜆𝑦.𝑦𝑇𝑟𝑢𝑒→𝑇𝑟𝑢𝑒
Reprezentace čísel a operací nad nimi
Pro reprezentaci čísel v lambda kalkulu se používají Peanova (Pínova) čísla:
Nad těmito čísly existují tyto operace (na státnice podle mě stačí znát succ a iszero, ale pro jistotu sem uvádím i některé další):
𝐿𝐸𝑇 𝒔𝒖𝒄𝒄 = 𝜆𝑥𝑔𝑚.𝑥𝑔𝑔𝑚, následník musí přidat k číslu jedno f navíc.
𝐿𝐸𝑇 𝑝𝑟𝑒𝑣 =𝜆𝑥𝑔𝑚. 𝑠𝑛𝑑𝑥𝑝𝑟𝑒𝑓𝑛 𝑔𝑇𝑟𝑢𝑒,𝑚
𝐿𝐸𝑇 𝑎𝑑𝑑= 𝜆𝑎𝑏𝑔𝑚.𝑎𝑔𝑏𝑔𝑚
Pomocné funkce:
𝐿𝐸𝑇 (_,_) = 𝜆𝑓𝑠𝑒.𝑒𝑓𝑠
𝐿𝐸𝑇 𝑓𝑠𝑡 =𝜆𝑝.𝑝 𝑇𝑟𝑢𝑒
𝐿𝐸𝑇 𝑠𝑛𝑑 =𝜆𝑝.𝑝 𝐹𝑎𝑙𝑠𝑒
Příklady
𝐬𝐮𝐜𝐜 𝟎=
𝐬𝐮𝐜𝐜 𝟐=
𝐢𝐬𝐳𝐞𝐫𝐨 𝟎=
0λv.False True
Notes
2. Otazka (předmět) (okruh): Lambda kalkul - Booleovske hodnoty (FLP) (21)
Kdo me primarne zkousel: Krivka
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: Zacal jsem definici True a False, ale chtel napred nejaky zakladni definice co je to lambda kalkul, neco jsem tam vypotil, dost pomahal, ale stacilo mu to co jsem vedel. Pak jsem zadefinoval True a False, chtel jenom zhruba nastinit jak bych udelal implikaci, pak chtel primo udelat OR, neco jsem tam naznacil, rikam ze to jeste neni hotovy a ze se nad tim musim zamyslet, tak mi poradil a rika ze uz je to hotovy a ze mu to staci. 
From <[link]> 
Práce v lambda kalkulu (reprezentace čísel a pravdivostních hodnot a operací nad nimi).
Kdo me primarne zkousel: Křivka
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: Na papieriku bolo napísané, že chce rovno vidieť vyjadrenie true, false, not, and, or a ekvivalenciu. Všetko som hneď písal na tabuľu, u ekvivalencie som začal, že si to vyjadrím ako konjunkciu implikácií a tie si vyjadrím ako disjunknciu. Pýtal sa ma však, či by som to vedel aj nejak lepšie zapísať. To som sa tam pokúšal vymyslieť, ale povedal som, že momentálne to asi nevymyslím. Povedal, že nevadí a stačilo mu to.
From <[link]> 
Kdo me primarne zkousel: Vojnar
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli:
Klasika. Nadefinoval jsem pravdivostí hodnoty. Pak se zeptal na NOT a že mám ukázat jak se vyhodnotí s nějakou hodnotou. Já jsem si ale nebyl úplně jistý jestli si na to vzpomenu zprávně, tak jsem to raději odvodil a už u toho jsem říkal jak to funguje. Pak to stejné u AND.
B
From <[link]> 
Kdo me primarne zkousel: Vojnar
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli:
Chtěl definice TRUE, FALSE a NOT. Potom praktickou ukázku vyhodnocení NOTu a jak se jmenuje operace dosazení (beta-redukce). Potom chtěl slovně popsat, jak by se dělal AND (jenom princip) + říct, že je to short evaluation. Rychlovka, žádné chytáky, toť vše.
From <[link]> 