updates

ahmed/LogicalRelations.agda

@@ -0,0 +1,78 @@
+module Ahmed.LogicalRelations where
+
+open import Data.Empty
+open import Data.Unit
+open import Data.Bool
+open import Data.Nat
+open import Data.Fin
+open import Data.Product
+open import Relation.Nullary using (Dec; yes; no)
+
+data type : Set where
+  bool : type
+  _-→_ : type → type → type
+
+data ctx : Set where
+  nil : ctx
+  _,_ : ctx → type → ctx
+
+data var : ctx → type → Set where
+  zero : ∀ {Γ τ} → var (Γ , τ) τ
+  suc : ∀ {Γ τ₁ τ₂} → var Γ τ₂ → var (Γ , τ₁) τ₂
+
+data term : ctx → type → Set where
+  true : ∀ {Γ} → term Γ bool
+  false : ∀ {Γ} → term Γ bool
+  `_ : ∀ {Γ τ} → var Γ τ → term Γ τ
+  λ[_]_ : ∀ {Γ τ₂} → (τ₁ : type) → (e : term (Γ , τ₁) τ₂) → term Γ (τ₁ -→ τ₂)
+  _∙_ : ∀ {Γ τ₁ τ₂} → term Γ (τ₁ -→ τ₂) → term Γ τ₁ → term Γ τ₂
+
+length : ctx → ℕ
+length nil = zero
+length (ctx , _) = suc (length ctx)
+
+extend : ∀ {Γ Δ}
+  → (∀ {τ} → var Γ τ → var Δ τ)
+  → (∀ {τ₁ τ₂} → var (Γ , τ₂) τ₁ → var (Δ , τ₂) τ₁)
+extend ρ zero = zero
+extend ρ (suc c) = suc (ρ c)
+
+rename : ∀ {Γ Δ}
+  → (∀ {τ} → var Γ τ → var Δ τ)
+  → (∀ {τ} → term Γ τ → term Δ τ)
+rename ρ true = true
+rename ρ false = false
+rename ρ (` x) = ` (ρ x)
+rename ρ (λ[ τ₁ ] c) = λ[ τ₁ ] rename (extend ρ) c
+rename ρ (c ∙ c₁) = rename ρ c ∙ rename ρ c₁
+
+extends : ∀ {Γ Δ}
+  → (∀ {τ} → var Γ τ → term Δ τ)
+  → (∀ {τ₁ τ₂} → var (Γ , τ₂) τ₁ → term (Δ , τ₂) τ₁)
+extends σ zero = ` zero
+extends σ (suc x) = rename suc (σ x)
+
+subst : ∀ {Γ Δ}
+  → (∀ {τ} → var Γ τ → term Δ τ)
+  → (∀ {τ} → term Γ τ → term Δ τ)
+subst ρ true = true
+subst ρ false = false
+subst ρ (` x) = ρ x
+subst ρ (λ[ τ₁ ] x) = λ[ τ₁ ] subst (extends ρ) x
+subst ρ (x ∙ x₁) = subst ρ x ∙ subst ρ x₁
+
+_[_] : ∀ {Γ τ₁ τ₂} → term (Γ , τ₂) τ₁ → term Γ τ₂ → term Γ τ₁
+_[_] {Γ} {τ₁} {τ₂} e e₁ = subst σ e
+  where
+    σ : ∀ {τ} → var (Γ , τ₂) τ → term Γ τ 
+    σ zero = e₁
+    σ (suc x) = ` x
+
+data value : ∀ {Γ τ} → term Γ τ → Set where
+  true : ∀ {Γ} → value {Γ} true
+  false : ∀ {Γ} → value {Γ} false
+  λ[_]_ : ∀ {Γ τ₁ τ₂} {e : term (Γ , τ₁) τ₂} → value (λ[ τ₁ ] e)
+
+data step : ∀ {Γ τ} → term Γ τ → term Γ τ → Set where 
+  β-λ : ∀ {Γ τ₁ τ₂ v} → (e : term (Γ , τ₁) τ₂) → value v
+    → step ((λ[ τ₁ ] e) ∙ v) (e [ v ])

ahmed/day1.agda

@@ -1,26 +1,79 @@
+{-# OPTIONS --prop #-}
 module Ahmed.Day1 where
 
 open import Data.Empty
 open import Data.Unit
+open import Data.Bool
+open import Data.Nat
+open import Data.Fin
+open import Data.Product
 open import Relation.Nullary using (Dec; yes; no)
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; trans; sym; cong; cong-app)
+open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
 
 data type : Set where
   bool : type
-  _-→_ : type -> type -> type
+  _-→_ : type → type → type
 
-data term : Set where
-  true : term
+data ctx : ℕ → Set where
+  nil : ctx zero
+  _,_ : ∀ {n} → ctx n → type → ctx (suc n)
 
-data ctx : Set where
-  nil : ctx
-  cons : ctx -> type -> ctx
+data term : (n : ℕ) → Set where
+  `_ : ∀ {n} → (m : Fin n) → term n
+  true : ∀ {n} → term n
+  false : ∀ {n} → term n
+  λ[_]_ : ∀ {n} → (τ₁ : type) (e : term (suc n)) → term n
+  _∙_ : ∀ {n} → term n → term n → term n
 
-data substitution : Set where
-  nil : substitution
-  cons : substitution -> term -> substitution
+postulate
+  lookup : ∀ {n} → Fin n → ctx n → type
+-- lookup {n} Γ 
 
-isGoodSubstitution : (Γ : ctx) -> (γ : substitution) -> Set
-isGoodSubstitution nil nil = ⊤
-isGoodSubstitution nil (cons γ x) = ⊥
-isGoodSubstitution (cons Γ x) nil = ⊥
-isGoodSubstitution (cons Γ x) (cons γ x₁) = {!   !}
+data typing : ∀ {n} {Γ : ctx n} → term n → type → Set where
+  `_ : ∀ {n Γ τ} → (m : Fin n) → lookup m Γ ≡ τ → typing {n} {Γ} (` m) τ
+  true : ∀ {n Γ} → typing {n} {Γ} true bool
+  false : ∀ {n Γ} → typing {n} {Γ} false bool
+
+data is-value : ∀ {n} → (e : term n) → Set where
+  true : ∀ {n} → is-value {n} true
+  false : ∀ {n} → is-value {n} false
+  λ[_]_ : ∀ {n} → (τ : type) → (e : term (suc n)) → is-value {n} (λ[ τ ] e)
+
+value = ∀ {n} → Σ (term n) (is-value)
+
+lift-term : ∀ {n} → term n → term (suc n)
+lift-term {n} (` m) = ` (suc m)
+lift-term {n} true = true
+lift-term {n} false = false
+lift-term {n} (λ[ τ₁ ] e) = λ[ τ₁ ] lift-term e
+lift-term {n} (e ∙ e₁) = lift-term e ∙ lift-term e₁
+
+subst : ∀ {n} → (e : term (suc n)) → (v : term n) → term n
+subst {n} (` zero) v = v
+subst {n} (` suc m) v = ` m
+subst true v = true
+subst false v = false
+subst (λ[ τ ] e) v = λ[ τ ] subst e (lift-term v)
+subst (e₁ ∙ e₂) v = subst e₁ v ∙ subst e₂ v
+
+data step : ∀ {n} → term n → term n → Set where
+  β-step : ∀ {n τ e e₂} → step {n} ((λ[ τ ] e) ∙ e₂) (subst e e₂)
+
+-- irreducible : ∀ {n} → (e : term) → ∃[ e' ] mapsto e'
+
+-- type-soundness : ∀ {e τ} → 
+
+value-relation : ∀ {n} → (τ : type) → (e : term n) → Set
+expr-relation : ∀ {n} → (τ : type) → (e : term n) → Set
+
+value-relation bool true = ⊤
+value-relation bool false = ⊤
+value-relation (τ₁ -→ τ₂) ((λ[ τ ] e) ∙ v) = expr-relation τ₂ {!   !}
+value-relation _ _ = ⊥
+ 
+expr-relation {n} τ e = {!   !}
+
+semantic-soundness : ∀ {n} (Γ : ctx n) → (τ : type) → (e : term n) → Set  
+-- semantic-soundness {n} Γ τ e = (γ : substitution n) → expr-relation τ {!   !}

ahmed/notes.typ

@@ -3,6 +3,7 @@
 #show: doc => conf("Logical Relations", doc)
 
 #let safe = $"safe"$
+#let ref = "ref"
 
 == Lecture 1
 
@@ -474,4 +475,10 @@ Type = ${ I in "Nat" -> P("CValue")}$
 
 (CValue = Closed values)
 
-$V_(k, S) db("ref" tau) = { l | l in V_(k-1) db(tau) }$
+$V_(k, S) db("ref" tau) = { l | l in V_(k-1) db(tau) }$
+
+#pagebreak()
+
+== Lecture 4
+
+$V_k db(ref tau) = { l | S(L) in V db(tau)}$

bourgeat/notes.typ

@@ -0,0 +1,102 @@
+#import "../common.typ": *
+#import "@preview/prooftrees:0.1.0": *
+#show: doc => conf("Rule-based languages from modular design to modular verification", doc)
+#import "@preview/finite:0.3.0" as finite: automaton
+
+== Lecture 1
+
+*Definition (module).* $(S."type", {R}_(i in S), {v m}, {a m})$
+
+- States
+- $R subset S times S$. these are transitions, very similar to automata
+- $a m subset S times NN times S$. argument methods. One argument always, type natural number. "If I'm in a state, and then I call some action, then I end up in a new state"
+- $v m subset S times NN times NN$. value methods are the only way to observe anything in the system. Observations are always of type nat for now.
+
+*Example (coffee-tea machine).*
+
+#automaton(
+  layout: finite.layout.snake.with(columns: 3),
+  (
+    q1: (q2: "put"),
+    q2: (q3: "coffee", q4: "tea"),
+    q3: (q3: "see"),
+    q4: (q4: "see"),
+  )
+)
+
+This is encoded as: 
+
+$({1, 2, 3, 4}, {}, {
+  "getTea" = {(2, star, 4)},
+  "getCoffee" = {(2, star, 3)},
+  "putMoney" = {(1, 1, 2)},
+}, {
+  "see" = {(3, star, "coffee"), (4, star, "tea")}
+})$
+
+Similarity to automata
+- Finite states
+Differences from automata
+- Sliced transitions between things that change the state of the system and ones that observe the state of the system
+
+We are interested in modeling the basic blocks of hardware as this kind of machine.
+We will write a language to plug together these modules into bigger modules.
+
+*Example (register).*
+
+$ (NN, {}, &{"write" = {(x, y, y) | forall x, y in NN^2}} \
+&{"read" = {(x, z, x) | forall x, z in NN^2}})  $
+
+Infinite transitions are ok but there needs to be a finite number of them.
+
+*Example (infinite atomic memory).* This can't be expressed in hardware.
+
+$ (NN -> NN, {}, &{"write" = {(f, ("idx", v), f') | forall y. "idx" = j -> f j = f' j, f' "idx" = v}}, \
+&{"read" = {(f, "arg", f("arg")) | forall f, "arg"}})
+$
+
+*Example (queue).* $([NN], {}, {"enqueue", "dequeue"}, {"first"})$
+
+== #strike[Equivalence] Refinement
+
+If both sides can be refined into each other then they are equivalent.
+
+- One way is to construct the language of the automata
+
+*Definition (traces of a module/behaviors).*
+
+Silent transition: $s_0 mapsto s_1$
+
+Observations about the state must be added to the trace as well.
+Trace looks like $["enqueue" (1), "first" () -> 1]$ for a queue.
+
+*Definition (Refinement).* A module $M$ refines $M'$ iff $db(M) subset.eq db(M')$.
+
+*Definition (weak simulation).* A module $M$ simulates $M'$
+
+$ M op(subset.sq.eq)_phi M'$
+
+s.t $phi : S_M times S_M'$ (relation between state of $M$ and state of $M'$).
+
+$phi$ witnesses that $M'$ simulates $M$ iff $(m_0, m'_0) in phi$
+
+#let arg = "arg"
+#let sset = "set"
+- Base case: $forall v in cal(V), forall arg, forall sset, (m_0, arg, sset) in v ==> (m'_0, arg, sset)$
+- Inductive case: $forall m in S_M, m' in S_M', (m, m') in phi ==> forall "am" in a_m, forall arg, m mapsto^("am"(arg)) m_2 ==> (m' mapsto^("am"(arg)) m'_2)$
+
+$ (M op(subset.sq.eq)_phi M') ==> db(M) subset db(M') $
+
+=== Composing
+
+Compose $M_1$, $M_2$, and $M_3$ into a bigger module.
+
+#tree(
+  axi[$(m, f("arg"), m') in "enq"_M$],
+  uni[$m."enqE"("arg") --> m'$],
+)
+
+#tree(
+  axi[$(m, f("arg"), m') in "enq"_M$],
+  uni[$m."deq"("arg") --> m'$],
+)

pfenning/notes.typ

@@ -481,4 +481,157 @@ Pointer:
   axi[$Delta tack.r e : arrow.b^k_m A_k$],
   axi[$Gamma , x : A_k tack.r e' : C_r$],
   nary(3)[$Delta Gamma tack.r "match" e with wrap(x) => e' : C_r$],
-)
+)
+
+#pagebreak()
+
+== Lecture 4
+
+SAX : Semi-Axiomatic Sequence Calculus
+
+$ f : A_L -> B_L , x : A_L tack.r C_U $
+
+So we are using linear resources to create an unrestricted resource.
+Can't actually build this because $Gamma >= m$ and $U > L$.
+
+So in this case we woudl want to build:
+
+$ f : A_L -> B_L , x : A_L tack.r arrow.b^U_L C_U $
+
+=== Linear logic
+
+Two modes: $U > L$, $!A = op(arrow.b)^U_L op(arrow.t)^U_L A$
+
+Linear + non-linear logic (LNL) (Benton '95)
+
+#let downshift(a, b) = $op(arrow.b)^#a_#b$
+#let upshift(a, b) = $op(arrow.t)^#b_#a$
+
+JS$._4$ $V > T : square A = op(arrow.b)^V_T op(arrow.t)^V_T A$ (comonad) \
+Lax logic: $T > L : circle A = op(arrow.t)^T_L op(arrow.b)^T_L A$ (monad)
+
+If you wanted proof irrelevance, you would have proof relevance and proof irrelevance as modes.
+
+#pagebreak()
+
+== Lecture 5
+
+#let cell(a,V) = $"cell" #a " " #V$
+#let proc = "proc"
+#let cut = "cut"
+#let write = "write"
+#let read = "read"
+#let call = "call"
+
+Recall:
+
+Types:
+
+$A times B, & A -> B \
+1, \
++{l: A_l}, & \&{l : A_l} \
+arrow.b A, & arrow.t A $
+
+Continuations: $K ::= (x, y) => P | () => P | (l(x) => P_l)_(l in L) | wrap(x) => P$
+
+Values: $V ::= (a, b) | () | k(a) | wrap(a)$
+
+Programs: $P ::= write c S | read c S | cut x P ; Q | id a " " b | call f " " a$
+
+Storable: $S ::= V | K$
+
+=== Dynamics
+
+Format: $cell a_1 V_1, cell a_2 V_2, ..., proc P_1, proc P_2$
+
+- Cells are not ordered, but the procedures are ordered
+- Only writing to empty cells, mutating a cell is a different process
+
+Rules:
+
+- $proc (cut x P(x); Q(x)) mapsto cell(a, square), proc (P(a)), proc (Q(a))$
+- $cell(a, square), proc (write a S) mapsto cell(a, S)$
+- $cell(a, square), cell(b, S) , proc (id a b) mapsto cell(a, V)$
+- $cell(c, S), proc (read c k) mapsto proc (S triangle.r S)$
+  - where
+    - $(a, b) &triangle.r ((x, y) => P(x, y)) = P(a, b) \
+    () &triangle.r (() => P) = P \
+    k(a) &triangle.r (l(x) => P_l(x))_(l in L) \
+    wrap(a) &triangle.r (wrap(x) => P(x)) = P(a)
+    $
+
+Remarks: this is substructural because if you have the left side, then the arrow is a linear arrow.
+
+#let linarrow = $multimap$
+
+#tree(
+  axi[$Gamma,A tack.r B$],
+  uni[$Gamma tack.r A linarrow B$]
+)
+
+#tree(
+  axi[$Gamma, x tack.r P :: (y : B)$],
+  uni[$Gamma tack.r write c ((x, y) => P) :: (c : A linarrow B)$],
+)
+
+#tree(
+  axi[],
+  uni[$A, A linarrow B tack.r B$]
+)
+
+#tree(
+  axi[],
+  uni[$a : A, c : A linarrow B tack.r read c (a,b) :: (b : B)$]
+)
+
+#tree(
+  axi[$Gamma tack.r A$],
+  axi[$Gamma tack.r B$],
+  bin[$Gamma tack.r A & B$],
+)
+
+#tree(
+  axi[],
+  uni[$A & B tack.r A$],
+)
+
+#tree(
+  axi[],
+  uni[$A & B tack.r B$],
+)
+
+#tree(
+  axi[$(forall l in L) (Gamma tack.r P_l : (x : A_l))$],
+  uni[$Gamma tack.r write c (l(x) => P) :: (c : &{l : A_l}_(l in L))$],
+)
+
+#tree(
+  axi[$k in L$],
+  uni[$c : &{l:A_l}_(l in L) tack.r read c (k(a)) :: (a : A_k)$]
+)
+
+The final configuration of a program is all programs are used, all cells are used
+
+$ dot tack.r P :: (d_0 : A) $
+
+Cut elimination is not compatible with some semi-axiomatic sequent calculus.
+
+=== Recover from cut elimination
+
+https://www.cs.cmu.edu/~fp/papers/fscd20a.pdf \
+https://www.cs.cmu.edu/~fp/papers/mfps22.pdf
+
+Can't eliminate all cuts, cannot eliminate cuts that are subformulas (SNIPS) of the things you're trying to prove.
+
+snip rule
+
+#tree(axi[], uni[$underline(A), underline(B) tack.r A times.circle B$])
+
+#tree(axi[], uni[$underline(A) tack.r A plus.circle B$])
+#tree(axi[], uni[$underline(B) tack.r A plus.circle B$])
+
+#tree(
+  axi[$Delta tack.r A$],
+  axi[$Gamma , underline(A) tack.r C$],
+  bin[$Delta, Gamma tack.r C$]
+)