From f2eee785d84e14cf677854a46a900ba67dc68338 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 4 Jun 2024 13:52:15 -0400 Subject: [PATCH] update --- Makefile | 7 ++- ahmed/day1.agda | 3 +- ahmed/notes.typ | 140 +++++++++++++++++++++++++++++++++++++++++++-- common.typ | 6 +- pfenning/notes.typ | 2 + 5 files changed, 149 insertions(+), 9 deletions(-) diff --git a/Makefile b/Makefile index 9dab35a..a74e05e 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,9 @@ -deploy: +SOURCES := $(shell find . -name "*.typ") + +oplss.pdf: oplss.typ $(SOURCES) + typst compile $< + +deploy: oplss.pdf rsync -azr \ --exclude .git \ ./ root@veil:/home/blogDeploy/public/public-files/oplss-2024 \ No newline at end of file diff --git a/ahmed/day1.agda b/ahmed/day1.agda index a3303bd..4d83b7a 100644 --- a/ahmed/day1.agda +++ b/ahmed/day1.agda @@ -24,4 +24,5 @@ data evaluationContext : Set where dot : evaluationContext EIf_Then_Else_ : evaluationContext → Term → Term → evaluationContext EAppLeft : evaluationContext → Term → evaluationContext - EAppRight : Value → evaluationContext → evaluationContext \ No newline at end of file + EAppRight : Value → evaluationContext → evaluationContext + diff --git a/ahmed/notes.typ b/ahmed/notes.typ index 2219eb4..e66be0f 100644 --- a/ahmed/notes.typ +++ b/ahmed/notes.typ @@ -1,11 +1,11 @@ #import "../common.typ": * #import "@preview/prooftrees:0.1.0": * -#show: doc => conf(doc) +#show: doc => conf("Logical Relations", doc) #let ifthenelse(e, e1, e2) = $"if" #e "then" #e1 "else" #e2$ #let safe = $"safe"$ -= Mon. Jun 3 \@ 14:00 += Lecture 1, Mon. Jun 3 \@ 14:00 == Logical relations @@ -195,8 +195,7 @@ Use $gamma$ as a substitution from variables to values. Now define semantic soundness: -$ -Gamma tack.r.double e : tau :equiv forall (gamma in G db(Gamma)) . gamma(e) in Epsilon db(tau)$ +$ Gamma tack.r.double e : tau :equiv forall (gamma in G db(Gamma)) . gamma(e) in Epsilon db(tau) $ Prove: @@ -242,4 +241,135 @@ To prove B: _Proof._ Suppose $e'$ s.t. $e mapstostar e'$ . - Case : $not "irreducible" (e')$ then $exists e'' . e' mapsto e''$ -- Case : $"irreducible" (e')$ then $isValue(e')$ trivially. \ No newline at end of file +- Case : $"irreducible" (e')$ then $isValue(e')$ trivially. + +#pagebreak() + += Lecture 2, Tue. Jun 4 \@ 11:00 + +#set enum(numbering: "A.") + +Recall the lemmas we're proving: + +1. $dot tack.r e : tau arrow.r.double e in Epsilon db(tau)$ +2. $e in Epsilon db(tau) arrow.r.double safe(e)$ + +#set enum(numbering: "1.") + +To prove lemma A, we must prove the fundamental property: $Gamma tack.r e:tau arrow.r.double Gamma tack.r.double e:tau$. "Syntactically well-typed implies semantic well-typed" + +$ Gamma tack.r.double e : tau :equiv forall (gamma in G db(Gamma)) . gamma(e) in Epsilon db(tau) $ + +=== Proving A case for $lambda$ + +Case: + +#tree( + axi[$Gamma , x : tau tack.r e : tau_2$], + uni[$Gamma tack.r lambda (x : tau_1) . e : tau_1 arrow.r tau_2 $] +) + +*Show:* $Gamma tack.r.double lambda (x : tau_1) . e : tau_1 arrow tau_2$. + +Suppose $gamma in G db(Gamma)$. Then we ned to *show*: + +$ &gamma (lambda (x : tau_1). e) in Epsilon db(tau_1 arrow tau_2) \ +equiv &lambda (x:tau_1).gamma(e) in Epsilon db(tau_1 arrow tau_2) +$ + +Suffices to show: $lambda (x:tau_1) gamma(e) in V db(tau_1 arrow tau_2)$. + +Suppose $v in V db(tau_1)$. Then we need to show: + +$ &subst(x, v, gamma(e)) in Epsilon db(tau_2) \ +equiv & gamma[x mapsto v] (e) in Epsilon db(tau_2)$ + +By the induction hypothesis, $Gamma,x:tau_1 tack.r e:tau_2$, so $Gamma,x:tau_1 tack.r.double e:tau_2$. + +Because $gamma[x mapsto v] in G db(#[$Gamma, x : tau_1$])$, we can instantiate $Gamma,x:tau_1$ with $gamma[x mapsto v]$. (basically just translating it over to $gamma$) + +Therefore, $gamma[x mapsto v](e) in Epsilon db(tau_2)$ + +#TODO Do the app case at home. + +== Adding recursive types + +$ Omega :equiv (lambda x . x " " x) (lambda x . x " " x) $ + +Cannot be type-checked in STLC, but adding recursive types allows this to be typechecked. + +$ tau ::= 1 | "bool" | tau_1 arrow tau_2 | alpha | mu alpha . tau $ + +For example: + +- $"tree" = mu alpha . 1 + ("int" times alpha times alpha)$ +- $"intlist" = mu alpha . 1 + ("int" times alpha)$ + +$ e ::= ... | "fold"(e) | "unfold"(e) $ + +#tree( + axi[$Gamma tack.r e : subst(alpha, mu alpha . tau, tau)$], + uni[$Gamma tack.r "fold"(e) : mu alpha . tau $], +) + +#tree( + axi[$Gamma tack.r e : mu alpha . tau $], + uni[$Gamma tack.r "unfold"(e) : subst(alpha, mu alpha . tau, tau)$], +) + +*NOTE*: Fold usually needs to be annotated with $mu alpha . tau$ in order to guide type checking. + +== Type-checking $Omega$ + +$ Omega :equiv (lambda (x : ?) . x " " x) (lambda (x : ?) . x " " x) $ + +With inductive types, we can give the second $x$ some type $alpha$. +Then the first $x$ that calls it would be $alpha arrow tau$ for some $tau$. + +$ "SA" : (mu alpha . alpha arrow tau) arrow tau \ +"SA" :equiv lambda (x : mu alpha . alpha arrow tau) . ("unfold" x) x$ + +Then re-define $Omega$ to be: + +$ Omega' :equiv "SA" ("fold" "SA") $ + +== Proving soundness for lambda calculus with recursive types with logical relations + +$ v ::= ... | "fold"(v) $ + +*NOTE:* Unfold will not be a value. + +$ E ::= ... | "fold" E $ + +New reduction rule: + +$ "unfold"("fold" v) mapsto v $ + +$V db(mu alpha . tau) = { "fold"(v) | forall v in V db(subst(alpha, mu alpha. tau, tau)) }$ + +This is *not* a well-founded relation, because $V$ would depend on itself. This was an open problem (ATTAPL exercise) for a long time. + +=== Step Indexing + +This shows that this is well founded. + +"If i were to run my program for $k$ steps, then I would not be able to tell that $V$ isn't well-founded" + +#rect[$V_k db(tau)$] + +$V_k db("bool") = {"true" , "false"}$ + +$V_k db(mu alpha . tau) = {"fold" v | v in V_(k-1) db(subst(alpha , mu alpha. tau , tau))}$ + +- Doing $"unfold"("fold" x) mapsto x$ "consumes" a step of $k$, so that's why $v$ already consumes a step. + +$V_k db(tau_1 arrow tau_2) = {lambda (x : tau_1) . e | forall (j lt.eq k, v in V_j db(tau_1)) arrow.r.double subst(x, v, e) in Epsilon_j db(tau_2)}$ + +- Think of this as a timeline, starting with $k$ steps left +- $j+1$ is the number of steps left when you get to the application of the lambda +- Use 1 step to do the application, resulting in $j$ steps +- Eventually reach 0 steps left. + +$Epsilon_k db(tau) = { e | forall (j < k, e') arrow.r.double e mapsto e' and "irreducible"(e') arrow.r.double e' in V_(k-j) db(tau)}$ + +What $k$ doesn't matter because the entire relations are universally quantified over all $k$s. \ No newline at end of file diff --git a/common.typ b/common.typ index d8fb59b..ae48437 100644 --- a/common.typ +++ b/common.typ @@ -7,9 +7,11 @@ #let subst(x, v, e) = $#e [#v\/#x]$ #let TODO = text(fill: red)[*TODO*] -#let conf(doc) = { +#let conf(title, doc) = { show link: underline - set page(width: 5in, height: 8in, margin: 0.4in) + set page(width: 6in, height: 9in, margin: 0.3in) + + text(size: 30pt)[#title] doc } diff --git a/pfenning/notes.typ b/pfenning/notes.typ index 16d9f20..7c26c16 100644 --- a/pfenning/notes.typ +++ b/pfenning/notes.typ @@ -141,6 +141,8 @@ Language to be studied is called "snax" uni[$Gamma tack.r k(e) : +{l : A_l}_(l in L)$], ) +#pagebreak() + == Lecture 2 Type system