# JP 2

[JP 1](https://hackmd.io/QbsRQ4d0TB2zi3Bn_o9Qow)

## Zadanie 1




Dla $t = v: v \Downarrow v \implies v \rightarrow^{*} v$

Dla $t = succ(t_1):$

Chcemy pokazać:
$$
succ(t_1) \Downarrow succ(nv_1) \implies succ(t_1) \rightarrow^*succ(nv_1)
$$

Wiemy z reguł dla dużych kroków, że dla takiej postaci pasuje tylko następująca reguła -- $\frac{t_1 \Downarrow nv_1}{succ \, (t_1) \Downarrow succ \, (nv_1)}$. Z zasady indukcji wiemy, że $t_1 \rightarrow^{*} nv_1$. Korzystając z lematu mamy wiec ze $succ(t_1) \rightarrow^{*} succ(nv_1)$.

Lemat (który dowodzi całość):
$$
t_1 \rightarrow^{*} t_2
\implies
succ \, (t_1) \rightarrow^{*} succ \, (t_2)
$$

Dla $t = \texttt{if } t_1 \texttt{ then } t_2 \texttt{ else } t_3$:

Chcemy pokazać:
$$
\texttt{if } t_1 \texttt{ then } t_2 \texttt{ else } t_3 \Downarrow v_2 \implies
\texttt{if } t_1 \texttt{ then } t_2 \texttt{ else } t_3 \rightarrow^{*} v
$$

Analogicznie jak poprzednio, tylko trochę inne lematy.

Lemat(y):
$$
t_1 \rightarrow^{*} true \, \land \, t_2 \rightarrow^{*} t_x
\implies
t \rightarrow^{*} t_x
$$
$$
t_1 \rightarrow^{*} false \, \land \, t_3 \rightarrow^{*} t_x
\implies
t \rightarrow^{*} t_x
$$

Inne przypadki się sprowadzają do powyższych.

$$(\Leftarrow)$$

Dla $t = succ(t_1):$

Chcemy pokazać:
$$
succ(t_1) \rightarrow^{*} succ(nv_1)
\implies
succ(t_1) \Downarrow succ(nv_1)
$$

Z determinizmu $\rightarrow^{*}$ mamy, że $t_1 \rightarrow^{*} nv_1$. Z indukcji otrzymujemy, że $t_1 \Downarrow nv_1$, a korzystając z odpowiedniej reguły otrzymujemy tezę. $\left(\frac{t_1 \Downarrow nv_1}{succ \, (t_1) \Downarrow succ \, (nv_1)}\right)$

## Zadanie 2


W pierwszym pytaniu przykładowa formuła dla której relacja ewaluacji jednokrokowej nie jest deterministyczna:
$\texttt{IF (FALSE) THEN (TRUE) ELSE (IF (TRUE) THEN (FALSE) ELSE (TRUE))}$

Chcemy pokazać, że dla każdego t
$$
t \rightarrow^* v \Leftrightarrow t \rightarrow_1^* v
$$

W prawo oczywiste.
Dowód w lewo:
$$
t = \texttt{IF } t_0 \texttt{ THEN } t_1 \texttt{ ELSE } t_2
$$

Jeśli $t_0 \rightarrow^{*}_1 v_0$ to z indukcji $t_0 \rightarrow^{*} v_0$ (analogicznie $t_1$, $t_2$). Nowa reguła nie wpłynie nam na $t_0$ i $t_1$. Stąd, jeśli $t_0 \rightarrow^{*}_1 TRUE$, to $t_0 \rightarrow^{*} TRUE$, a wtedy z indukcji w obu relacjach uzyskamy z $t$ wynik dla $t_1$ (wszystkie kroki dla $t_2$ są zbędne).
W przeciwnym przypadku, jeśli w obu relacjach $t_0$ ewaluuje się do $FALSE$, to w pierwszej relacji zwrócimy $t_2$, a w drugiej tknięte przez nową operację $t_2'$. Ale zauważmy, że teraz dowolna operacja wykonana na $t_2'$ jest też dozwolona na $t_2$, więc możemy je z indukcji wykonać na $t_2$ w danym momencie.

## Zadanie 3

Niech $\rightarrow^*_w$ będzie tą nową relacją

Chcemy pokazać, że dla każdego t
$$
t \rightarrow^* s \Leftrightarrow t \rightarrow^*_w wrong
$$
gdzie $s$ jest stuck, czyli jest w $postaci\;normalnej$, ale nie jest $value$.

Wypiszmy reguły dla stuck, a następnie powtórzmy dowód z zadania 1.

Lemat:
s -> wrong

s: value x
s: if t1 then t2 else t3
t1

## Zadanie 4

type term =
    | True | False | Zero
    | IsZero of term
    | Succ of term
    | Pred of term
    | IfElse of term * term * term

type numerical =
    | Z
    | S of numerical

type value =
    | T | F | N of numerical | Error

(* Zakładamy, że t jest termem typu jak ten wyżej *)
let rec eval t =
    match t with
        | True -> T
        | False -> F
        | Zero -> N Z
        | IsZero t ->
            let v = eval t in
            (match v with
                | N Z -> T
                | N (S v) -> F
                | T | F | Error -> Error)
        | Succ t -> 
            let v = eval t in
            (match v with
                | N v -> N (S v)
                | T | F | Error -> Error)
        | Pred t ->
            let v = eval t in
            (match v with
                | N Z -> N Z
                | N (S v) -> N v
                | T | F | Error -> Error)
        | IfElse (t1, t2, t3) ->
            let v1 = eval t1 in
            (match v1 with
                | T -> eval t2
                | F -> eval t3
                | N _ | Error -> Error)
;;

## Zadanie 5

Reguły małych kroków:
$$
\frac{}{false \texttt{ AND } t_2 \rightarrow false}
$$

$$
\frac{}{true \texttt{ AND } t_2 \rightarrow t_2}
$$

$$
\frac{t_1 \rightarrow t_1'}{t_1 \texttt{ AND } t_2 \rightarrow t_1' \texttt{ AND } t_2}
$$

$$
\frac{}{true \texttt{ OR } t_2 \rightarrow true}
$$

$$
\frac{}{false \texttt{ OR } t_2 \rightarrow t_2}
$$

$$
\frac{t_1 \rightarrow t_1'}{t_1 \texttt{ OR } t_2 \rightarrow t_1' \texttt{ OR } t_2}
$$

type term =
    | True | False | Zero
    | IsZero of term
    | Succ of term
    | Pred of term
    | IfElse of term * term * term
    | And of term * term
    | Or of term * term

type numerical =
    | Z
    | S of numerical

type value =
    | T | F | N of numerical | Error

(* Zakładamy, że t jest termem typu jak ten wyżej *)
let rec eval t =
    match t with
        | True -> T
        | False -> F
        | Zero -> N Z
        | IsZero t ->
            let v = eval t in
            (match v with
                | N Z -> T
                | N (S v) -> F
                | T | F | Error -> Error)
        | Succ t -> 
            let v = eval t in
            (match v with
                | N v -> N (S v)
                | T | F | Error -> Error)
        | Pred t ->
            let v = eval t in
            (match v with
                | N Z -> N Z
                | N (S v) -> N v
                | T | F | Error -> Error)
        | IfElse (t1, t2, t3) ->
            let v1 = eval t1 in
            (match v1 with
                | T -> eval t2
                | F -> eval t3
                | N _ | Error -> Error)
        | And (t1, t2) ->
            let v1 = eval t1 in
            (match v1 with
                | T -> eval t2
                | F -> F
                | N _ | Error -> Error)
        | Or (t1, t2) ->
            let v1 = eval t1 in
            (match v1 with
                | F -> eval t2
                | T -> T
                | N _ | Error -> Error);;

## Zadanie 6

type term =
    | True | False | Zero
    | IsZero of term
    | Succ of term
    | Pred of term
    | IfElse of term * term * term

let rec build symbols =
    let symbol :: tail = symbols in
    match symbol with
    | "Zero" -> Zero, tail
    | "True" -> True, tail
    | "False" -> False, tail
    | "Succ" -> 
        let tree, new_tail = build tail in
        Succ tree, new_tail
    | "Pred" -> 
        let tree, new_tail = build tail in
        Pred tree, new_tail
    | "IsZero" -> 
        let tree, new_tail = build tail in
        IsZero tree, new_tail
    | "If" ->
        let condition, tail1 = build tail in
        let body_true, tail2 = build tail1 in
        let body_false, tail3 = build tail2 in
        IfElse (condition, body_true, body_false), tail3
    | "Then" | "Else" -> build tail
    | _ -> raise (Failure "Incorrect input")
    
build ["Succ"; "Zero"];;
build ["If"; "IsZero"; "Zero"; "Then"; "True"; "Else"; "If"; "True"; "Then"; "Succ"; "Zero"; "Else"; "Succ"; "Succ"; "Zero"];;
build ["If"; "If"; "False"; "Then"; "IsZero"; "Zero"; "Else"; "True"; "Then"; "Zero"; "Else"; "False"];;