25 lines
841 B
Text
25 lines
841 B
Text
|
#import "../common.typ": *
|
||
|
|
#import "@preview/prooftrees:0.1.0": *
|
||
|
|
#show: doc => conf("Foundations", doc)
|
||
|
|
|
||
|
|
== Lecture 1
|
||
|
|
|
||
|
|
Skipped.
|
||
|
|
|
||
|
|
== Lecture 2
|
||
|
|
|
||
|
|
Variables $in.rev x, y, z ::= "foo" | "bar" | "baz" | ...$ \
|
||
|
|
Constant $in.rev C ::= "true" | "false"$ \
|
||
|
|
Term $in.rev M, N ::= X | M N | lambda x . M | C | ifthenelse(M, N_1, N_2)$
|
||
|
|
|
||
|
|
Eval Ctx $in.rev E ::= square | E M | ifthenelse(E, N_1, N_2)$ \
|
||
|
|
Environment $in.rev Gamma ::= $ \
|
||
|
|
Judgment $::= Gamma tack.r M : A$
|
||
|
|
|
||
|
|
#tree(axi[], uni[$Gamma tack.r "true" : "bool"$])
|
||
|
|
#tree(axi[], uni[$Gamma tack.r "false" : "bool"$])
|
||
|
|
#tree(axi[$Gamma tack.r M : "bool"$], axi[$Gamma tack.r N_1 : tau$], axi[$Gamma tack.r N_2 : tau$], tri[$Gamma tack.r ifthenelse(M, N_1, N_2) : tau$])
|
||
|
|
|
||
|
|
*Lemma (Progress).* If $dot tack.r M : A$ is derivable, then $M$ is a value, or $M mapsto M'$.
|
||
|
|
|
||
|
|
_Proof._ Induction on derivation.
|