# FLP -- Lambda kalkul
## Pevny bod
- prezentacia lambda calcul 30-33 slide
- pomocka aby si mohol duplikovat/replikovat/rekurzivne pracovat s funkciou
- napr. klasicky mas sucet 2 cisel, ale s vyuzitim pevneho bodu mozes scitat hocikolko cisel
cize mozes spravit `SUM 1 2 3 4 5 6 7 8 9`
miesto len `SUM 1 2`

k - pevny bod
E - vyraz
Y - operator pevneho bodu

Y E = k
E k = k
E (Y E) = Y E

## Cheatsheet

LET True = λxy . xy
LET False = λxy . yx

LET NOT = λa . a (λs.False) (λt.True) -- negace

LET AND = λab . a (λs.b) (λt.False) -- konjunkce
LET OR = λab . a (λs.True) (λt.b) -- disjunkce
LET EQ = λab . a (λs.b) (λt.NOT b) -- ekvivalence
LET XOR = λab . a (λs.NOT b) (λt.b) -- negace ekvivalence
LET IMP = λab . a (λs.b) (λt.True) -- implikace
LET NAND = λab . a (λs.NOT b) (λt. True) -- negace konjunkce
LET NOR = λab . a (λs. False) (λt.NOT b) -- negace disjunkce
LET NIMP = λab . a (λs. NOT b) (λt. False) -- negace implikace
LET OIMP = λab . a (λs. True) (λt. NOT b) -- obrácená implikace
LET NOIMP = λab . a (λs. False) (λt. b) -- negace obrácené implikace
LET A = λab . a -- identita prvniho argumentu
LET B = λab . b -- identita druheho argumentu
LET NA = λab . NOT a -- negace identity prvniho argumentu
LET NB = λab . NOT b -- negace identity druheho argumentu
LET TAUT = λab . True -- tautologie
LET CONT = λab . False -- kontradikce

LET TERNARY = λabc . a (λs.b) (λt.c) -- ternarni operator

LET EQU =  \x y . x (\s . y) (\r . (NOT y))

-- Peanova aritmetika 
LET GTE = λab . iszero(sub b a)
LET LTE = λab . iszero(sub a b)
LET EQ = λab . iszero(sub a b) ? iszero(sub b a) : false

LET GT = λab . TERNARY (EQ a b) (False) (GTE a b)
LET LT = λab . TERNARY (EQ a b) (False) (LTE a b)

<!--  -->

Vlastnosť operátoru pevného bodu -- `Y E = E (Y E)`
Definícia LT v λ-kalkule s použitím operátora pevného bodu (`Y`), `iszero` a `prev`:

LET ?: = λ x y z . x y z
LET LTfn = λ f x y . (iszero y) ? False : ((iszero x) ? True : (f (prev x) (prev y))) 
LET LT = Y LTfn

## 2023/2024
### 1. opravny termin
1. /6b/ Demonstrujte vlastnost operátoru pevného bodu. V lambda-kalkulu pomocí operátoru pevného bodu definujte lambda-výraz `SUB`, který odečte dvě celá nezáporná čísla. K dispozici máte tedy nezáporná celá čísla, `iszero`, `succ`, `prev`, nicméně neznáte od ničeho z toho realizaci a nemůžete ji tedy přímo využít pro váš výraz, jen jako hotové věci tradičního chování. Pokud něco dalšího potřebujete, tak si to musíte vhodně dodefinovat. Demonstrujte dostatečně názorně, že `SUB 2 1 = 1`.

-- Pevný bod: E k = k
-- Operátor pevného bodu: Y E = k
-- Tedy: E (Y E) = Y E
LET True = \ x y . x
LET False = \ x y . y
LET SUB = Y (\ f a b. (iszero b) a (f (prev a) (prev b)))

SUB 2 1 =
(Y (\ f a b. (iszero b) a (f (prev a) (prev b)))) 2 1 =|vlastnost Y
((\ f a b. (iszero b) a (f (prev a) (prev b))) SUB) 2 1 |=beta
(\ a b. (iszero b) a (SUB (prev a) (prev b))) 2 1 |=2beta
(iszero 1) 2 (SUB (prev 2) (prev 1)) =|iszero 1 is False
(\ x y . y) 2 (SUB 1 0) =|2beta

SUB 1 0 =
(Y (\ f a b. (iszero b) a (f (prev a) (prev b)))) 1 0 =|vlastnost Y
((\ f a b. (iszero b) a (f (prev a) (prev b))) SUB) 1 0 |=beta
(\ a b. (iszero b) a (SUB (prev a) (prev b))) 1 0 |=2beta
(iszero 0) 1 (SUB (prev 1) (prev 0)) =|iszero 0 is True
(\ x y . x) 1 (SUB 0 0) =|2beta
1

### Riadny termin

Bonus: V lambda kalkule definovať `EM`, čo reprezentuje konštruktor prázdneho zoznamu `[]` , potom definovať `CONS` (konštruktor zoznamu cez `:`), `HD`, `TL` (`head`, `tail`) a ukázať, že platí:
`HD (TL CONS b (CONS a (EM))) = a`

## 2021/2022
### Predtermin

Vlastnosť operátoru pevného bodu -- `Y E = E (Y E)`
Definícia LT v λ-kalkule s použitím operátora pevného bodu (`Y`), `iszero` a `prev`:

LET LT = Y 
    ( \ f x y . iszero x 
        ? (iszero y ? False : True)
        : (iszero y ? False : f (prev x) (prev y))
    )

respektive:

LET ?: = λ x y z . x y z
LET LTfn = λ f x y . (iszero y) ? False : ((iszero x) ? True : (f (prev x) (prev y))) 
LET LT = Y LTfn

### 1. opravný
- POW x n - x ^ n, zadané True, dolplniť false, ternarny operator a

E k = k vlastnost pevného bodu
Y E = k funkce operátoru pevného bodu
E (Y E) = Y E vlastnost operátoru
LET True = \ x y . x y
LET False = \ x y . y
LET (?:) = \ c t f . c (\ x . t) f
LET POW = Y (\ f x n . iszero n ? 1 : mul x (f x (prev n)) )

<!-- ### 2. opravný -->

## 2020/2021
### riadny
definovať xor, true false podla seba

LET True = \ x y . x
LET False = \ x y . y
LET XOR = \ a b . a (b False True) b

-- konkretny priklad (nebol treba)
XOR True False = 
(\ a b . a (b False True) b) True False =
(\ b . True (b False True) b) False =
True (False False True) False  =
(\ x y . x )(False False True) False  =
(\y . (False False True)) False =
False False True =
(\ x y . y ) False True =
(\ y . y )  True =
True

### 2. opravný termín
/2b/ Napísať výraz, kde 2 premenné sú volné a zároveň aj viazané
- vrámci jedného výrazu (NIE 2 rôznych výrazov).

-- napr.:
(\x . (\b a . a b) a b)
-- Pozn.: vrámci (\b a . a b) sú a b viazané

/4b/ Napísať príklad pre platnú a neplatnú substitúciu
- vrámci jedného výrazu (NIE 2 rôznych výrazov).

-- napr.:
(\x y z. x y) a z
-- Pozn.: subtitucia a je platná ale substitúcia z nie

## 2019/2020
### předtermín
Bylo definovaný `True` jako `\xy.xy`.
Muselo se definovat `False` libovolným způsobem.
Dál bylo potřeba definovat ternární operátor `? :`.
A v poslední řadě definovat funkci `eq`, která porovnává dvě celá čísla. U toho bylo možné využít funkce `iszero` a `prev`. Tohle bylo potřeba implementovat pomocí operátoru pevného bodu.

máme: celá čísla, iszero, prev

LET True = \ x y . x y
LET False = \ x y . y
LET (?:) = \ c t f . c (\ z. t) f

LET eq = Y (\ f x y .         
        iszero x
            ? (iszero y ? True : False)      
            : (iszero y ? False : f (prev x) (prev y))
        )

## 2018/2019
LT bude asi funkcia less <

E k = k
Y E = k
Y E = E (Y E)

LET True = \ x y. x
LET False = \ x y. y

LET LT = Y(\f x y. iszero y False (iszero x True (f (prev x) (prev y))))

## 2017/2018
/6b/ Op. pevneho bodu - MINUS x y. Nadefinovat True + False. K dispozici isZero, prev. Pripadne si dodefinovat dalsi funkce.

LET True = \ x y . x
LET False = \ x y . y
LET (?:) = \ c t f . c t f

    Y E = k
    E k = k
    Y E = E k = E (Y E)
    
LET minus = Y (\ f x y . iszero x ? 0 : (iszero y ? x : f (prev x) (prev y) ))

## 2016/2017
Ukázat vlastnost operátoru pevného bodu. V lamda kalkulu definovat násobení (MUL) s dvěma parametry pomocí prev, add, iszero a ternárního operátoru (6b)

k - pevny bod
E - vyraz
Y - operator pevneho bodu

    Y E = k
    E k = k
    E (Y E) = Y E
    
LET mul = \ a b . (iszero a ? 0 : (iszero b ? 0 : mf a b 0))
LET mf = Y (\ f a b r . iszero a ? r : f (pred a) b (add r b))

## 2015/2016
Popsat operátor pevného bodu, jeho vlastnost.
Pomocí něj a předdefinovaných funkcí isZero, add a ternárního operátoru vytvořit výraz SUM (funkce fungují tak jak čekáme, ale mají nám neznámou implementaci, taky čísla mají neznámou implementaci).
Výraz SUM vezme dvě čísla, x a y, a pokud je y=0, vrátí x, jinak vrátí SUM (x+y) (tedy částečně aplikovaného sama sebe).
Ukázat vyhodnocení SUM 2 3 0.

Pro vyraz E je pevny bod k: E k = k
Operator pevneho bodu Y: Y E = k = E (Y E)

LET G = \ f x y. iszero y ? x : f (add x y)
LET SUM = Y G

SUM 2 3 0 =  
    = (Y G) 2 3 0 
    = (G (Y G)) 2 3 0 
    = (G SUM) 2 3 0 
    = ((\ f x y. iszero y ? x : f (add x y )) SUM) 2 3 0 
    = (iszero 3 ? 2 : SUM (add 2 3)) 0 
    = (SUM 5) 0 = SUM 5 0 
    = (Y G) 5 0 
    = (G (Y G)) 5 0 
    = (G SUM) 5 0 
    = ((\ f x y. iszero y ? x : f (add x y )) SUM) 5 0 
    = iszero 0 ? 5 : SUM (add 5 0) 
    = 5

### 1. opravný

Mějme definováno True jako: ``True = \ x y . x y``.
Definujte False standardního významu dle libosti. S jejích pomoci definujte IMP (implikace zleva doprava) standardního významu.
Redukujte po krocích```IMP True False = False```

LET True = \ x y . x y
LET False = \ x y . y
LET IMP = \ x y . x (\ z . y) True

IMP True False =  
    = (\ x y . x (\ z . y) True) True False
    = (\ y . True (\ z . y) True) False 
    = True (\ z . False) True 
    = (\ x y . x y) (\ z . False) True 
    = (\ y . (\ z . False) y) True 
    = (\ z . False) True 
    =  False

## 2014/2015
### Řádny
Definicia vlastnosti operatoru pevneho bodu.
Potom pomocou tohoto operatoru, iszero a prev nadefinovat minus, ktore berie 2 cisla a odcita ich a - b, pricom vysledok je nezaporny (tj. ==0 ak je b vacsie ako a).
Mali sme zohladnit, ze iszero, prev a cisla maju neznamu definiciu, ale znamy vyznam. True a False je mozne si nadefinovat podla seba.

let T =  \ x y . x
let F =  \ x y . y

nechť Y je operátor pevného bodu, E je lambda-výraz a 
k je pevný bod pro E, potom:
Y E = k = E k
Y E = E (Y E) ~ k = E k

LET minus = Y (\ f x y. iszero y ? x : (f (prev x) (prev y)))

### 1. opravný

LET True  = \ x y. x y
LET False = \ x y. y

LET NOR = \ a b. a (\i.False) (b (\k.False) True)

NOR True False =
    (\ a b. a (\i.False) (b (\k.False) True)) True False ->Beta
    (\ b. True (\i.False) (b (\k.False) True)) False ->Beta
    True (\i.False) (False (\k.False) True) =
    (\ x y. x y) (\i.False) (False (\k.False) True) ->Beta
    (\ y. (\i.False) y) (False (\k.False) True) ->Beta
    (\i.False) (False (\k.False) True) ->Beta
    False

## 2013/2014
pevny bod, nadefinovat GE

Y E = E (Y E)

LET gef = \ f x y . (iszero x ? iszero y : (iszero y ? True : f (prev x) (f prev y)))
let GE = Y gef