This commit is contained in:
Michael Zhang 2024-06-04 18:56:00 -04:00
parent f2eee785d8
commit ecb3ad58e3
9 changed files with 243 additions and 43 deletions

View file

@ -1,28 +1,34 @@
module ahmed.day1 where module ahmed.day1 where
open import Agda.Primitive
open import Data.Nat
open import Data.Fin
open import Data.Product open import Data.Product
data Type : Set where data Type : Set where
Bool : Type Bool : Type
_-→_ : Type Type Type _-→_ : Type Type Type
data Term : Set where data Term (n : ) : Set where
True : Term Var : (m : Fin n) Term n
False : Term True : Term n
If_Then_Else_ : Term Term Term Term False : Term n
λ[_::_]_ : Term Type Term Term If_Then_Else_ : Term n Term n Term n Term n
_∙_ : Term Term Term λ[_::_]_ : Term n Type Term n Term n
_∙_ : Term n Term n Term n
data isValue : Term Set where data isValue (n : ) : Term n Set where
TrueValue : isValue True TrueValue : isValue n True
FalseValue : isValue False FalseValue : isValue n False
LambdaValue : (x : Term) (τ : Type) (e : Term) isValue (λ[ x :: τ ] e) LambdaValue : (x : Term n) (τ : Type) (e : Term n) isValue n (λ[ x :: τ ] e)
Value = Σ Term isValue Value = (n : ) Σ (Term n) (isValue n)
data evaluationContext : Set where data evaluationContext : (n : ) Set where
dot : evaluationContext dot : evaluationContext 0
EIf_Then_Else_ : evaluationContext Term Term evaluationContext EIf_Then_Else_ : {n : } evaluationContext n Term n Term n evaluationContext n
EAppLeft : evaluationContext Term evaluationContext EAppLeft : {n : } evaluationContext n Term n evaluationContext n
EAppRight : Value evaluationContext evaluationContext EAppRight : {n : } Value evaluationContext n evaluationContext n
data isValidValueForType (n : ) (t : Type) : (e : Term n) Set where
TrueV : isValidValueForType n Bool True

View file

@ -2,12 +2,11 @@
#import "@preview/prooftrees:0.1.0": * #import "@preview/prooftrees:0.1.0": *
#show: doc => conf("Logical Relations", doc) #show: doc => conf("Logical Relations", doc)
#let ifthenelse(e, e1, e2) = $"if" #e "then" #e1 "else" #e2$
#let safe = $"safe"$ #let safe = $"safe"$
= Lecture 1, Mon. Jun 3 \@ 14:00 == Lecture 1
== Logical relations === Logical relations
Logical relations are used to prove things about programs Logical relations are used to prove things about programs
@ -31,11 +30,11 @@ Logical relations are used to prove things about programs
You can also relate source terms to target terms in different languages. You can also relate source terms to target terms in different languages.
This can be used to prove compiler correctness. This can be used to prove compiler correctness.
== Type safety / soundness === Type safety / soundness
Unary realizability relations for FFI. "all well-behaved terms from language A can be used in language B without causing problems with either language" Unary realizability relations for FFI. "all well-behaved terms from language A can be used in language B without causing problems with either language"
== STLC === STLC
Statics Statics
@ -123,7 +122,7 @@ $forall(e' . e mapstostar e')$ either $isValue(e')$ or $exists e'' . e' mapsto e
Progress and preservation are a _technique_ for proving type soundness, by just using the two functions over and over. Progress and preservation are a _technique_ for proving type soundness, by just using the two functions over and over.
== Logical relations === Logical relations
$ P_tau(e) $ $ P_tau(e) $
@ -245,7 +244,7 @@ _Proof._ Suppose $e'$ s.t. $e mapstostar e'$ .
#pagebreak() #pagebreak()
= Lecture 2, Tue. Jun 4 \@ 11:00 == Lecture 2
#set enum(numbering: "A.") #set enum(numbering: "A.")
@ -260,7 +259,7 @@ To prove lemma A, we must prove the fundamental property: $Gamma tack.r e:tau ar
$ 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) $
=== Proving A case for $lambda$ ==== Proving A case for $lambda$
Case: Case:
@ -292,7 +291,7 @@ Therefore, $gamma[x mapsto v](e) in Epsilon db(tau_2)$
#TODO Do the app case at home. #TODO Do the app case at home.
== Adding recursive types === Adding recursive types
$ Omega :equiv (lambda x . x " " x) (lambda x . x " " x) $ $ Omega :equiv (lambda x . x " " x) (lambda x . x " " x) $
@ -319,7 +318,7 @@ $ e ::= ... | "fold"(e) | "unfold"(e) $
*NOTE*: Fold usually needs to be annotated with $mu alpha . tau$ in order to guide type checking. *NOTE*: Fold usually needs to be annotated with $mu alpha . tau$ in order to guide type checking.
== Type-checking $Omega$ === Type-checking $Omega$
$ Omega :equiv (lambda (x : ?) . x " " x) (lambda (x : ?) . x " " x) $ $ Omega :equiv (lambda (x : ?) . x " " x) (lambda (x : ?) . x " " x) $
@ -333,7 +332,7 @@ Then re-define $Omega$ to be:
$ Omega' :equiv "SA" ("fold" "SA") $ $ Omega' :equiv "SA" ("fold" "SA") $
== Proving soundness for lambda calculus with recursive types with logical relations === Proving soundness for lambda calculus with recursive types with logical relations
$ v ::= ... | "fold"(v) $ $ v ::= ... | "fold"(v) $
@ -349,7 +348,7 @@ $V db(mu alpha . tau) = { "fold"(v) | forall v in V db(subst(alpha, mu alpha. ta
This is *not* a well-founded relation, because $V$ would depend on itself. This was an open problem (ATTAPL exercise) for a long time. 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 ==== Step Indexing
This shows that this is well founded. This shows that this is well founded.
@ -370,6 +369,6 @@ $V_k db(tau_1 arrow tau_2) = {lambda (x : tau_1) . e | forall (j lt.eq k, v in V
- Use 1 step to do the application, resulting in $j$ steps - Use 1 step to do the application, resulting in $j$ steps
- Eventually reach 0 steps left. - 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)}$ $Epsilon_k db(tau) = { e | forall (j < k, e') arrow.r.double e op(mapsto)^j 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. What $k$ doesn't matter because the entire relations are universally quantified over all $k$s.

View file

@ -6,12 +6,15 @@
#let mapstostar = $op(arrow.r.long.bar)^*$ #let mapstostar = $op(arrow.r.long.bar)^*$
#let subst(x, v, e) = $#e [#v\/#x]$ #let subst(x, v, e) = $#e [#v\/#x]$
#let TODO = text(fill: red)[*TODO*] #let TODO = text(fill: red)[*TODO*]
#let ifthenelse(e, e1, e2) = $"if" #e "then" #e1 "else" #e2$
#let conf(title, doc) = { #let conf(title, doc) = {
show link: underline show link: underline
set page(width: 6in, height: 9in, margin: 0.3in) set page(width: 4.8in, height: 8.4in, margin: 0.3in)
text(size: 30pt)[#title] [
doc = #text(size: 24pt)[#title]
#doc
]
} }

25
downen/notes.typ Normal file
View file

@ -0,0 +1,25 @@
#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.

View file

@ -1,4 +1,5 @@
#include "./ahmed/notes.typ" #include "./ahmed/notes.typ"
#include "./downen/notes.typ"
#include "./pfenning/notes.typ" #include "./pfenning/notes.typ"
#include "./silva/notes.typ" #include "./silva/notes.typ"

View file

@ -1,15 +1,13 @@
#import "../common.typ": * #import "../common.typ": *
#import "@preview/prooftrees:0.1.0": * #import "@preview/prooftrees:0.1.0": *
#import "@preview/algo:0.3.3": algo, i, d, comment, code #import "@preview/algo:0.3.3": algo, i, d, comment, code
#show: doc => conf(doc) #show: doc => conf("Adjoint Functional Programming", doc)
#let n(t) = text(fill: rgb("#aa3333"))[#t] #let n(t) = text(fill: rgb("#aa3333"))[#t]
#let evalto = $arrow.r.hook$ #let evalto = $arrow.r.hook$
#let with = $op(\&)$ #let with = $op(\&)$
= Adjoint Functional Programming == Lecture 1
== Lecture 1. Linear functional programming
- Origins of linearity is from linear logic - Origins of linearity is from linear logic
- from 1987 or before - from 1987 or before
@ -143,7 +141,7 @@ Language to be studied is called "snax"
#pagebreak() #pagebreak()
== Lecture 2 === Lecture 2
Type system Type system
@ -273,7 +271,7 @@ Example of evaluation rule that matches the typing rule:
) )
=== Looking at typing rules as logic ==== Looking at typing rules as logic
#rect[Natural Deduction] #rect[Natural Deduction]

BIN
silva/lec1.jpg Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 675 KiB

View file

@ -1,13 +1,13 @@
#import "../common.typ": * #import "../common.typ": *
#import "@preview/finite:0.3.0" as finite: automaton
#import "@preview/fletcher:0.4.5" as fletcher: diagram, node, edge
#import "@preview/prooftrees:0.1.0": * #import "@preview/prooftrees:0.1.0": *
#show: doc => conf(doc) #show: doc => conf("Program Analysis with Kleene Algebra with Tests", doc)
#let tru = $"true"$ #let tru = $"true"$
#let fls = $"false"$ #let fls = $"false"$
= Program Analysis with Kleene Algebra with Tests == Lecture 1
== Mon Jun 3 \@ 15:40
#quote(block: true)[ #quote(block: true)[
Kleene algebra with tests is an algebraic framework that can be used to reason about imperative programs. It has been applied across a wide variety of areas including program transformations, concurrency control, compiler optimizations, cache control, networking, and more. In these lectures, we will provide an overview of Kleene Algebra with Tests, including the syntax, semantics, and the coalgebraic theory underlying decision procedures for program equivalence. We will illustrate how it can be used as a core framework for program verification, including successful extensions and fundamental limitations. Kleene algebra with tests is an algebraic framework that can be used to reason about imperative programs. It has been applied across a wide variety of areas including program transformations, concurrency control, compiler optimizations, cache control, networking, and more. In these lectures, we will provide an overview of Kleene Algebra with Tests, including the syntax, semantics, and the coalgebraic theory underlying decision procedures for program equivalence. We will illustrate how it can be used as a core framework for program verification, including successful extensions and fundamental limitations.
@ -39,7 +39,7 @@
Study equivalence of uninterpreted simple imperative programs. Study equivalence of uninterpreted simple imperative programs.
=== Regular expressions ==== Regular expressions
Basic elements Basic elements
@ -172,3 +172,161 @@ Merge states of a non-deterministic finite automaton, using the peanut approach.
Alternative #link("https://en.wikipedia.org/wiki/Thompson%27s_construction")[*Thompson's construction*] Alternative #link("https://en.wikipedia.org/wiki/Thompson%27s_construction")[*Thompson's construction*]
#pagebreak()
== Lecture 2
Talking about the other direction from Kleene's theorem.
$ A_e mapsto e $
mapping an automaton $A_e$ to a regular expression $e$.
Let DFA have states $S$ and transition function $S mapsto S^A$. This can be represented by a matrix.
The matrix is indexed on rows and columns by the states. Then in the cell for each row $i$ and column $j$, put all of the letters of the alphabet that can be used to transition between the states. For example, if you can use $a$ and $b$, put $a+b$ in the matrix.
This allows you to do matrix operations in order to do operations on regular expressions. This shows that the transition function actually has more structure than just an arbitrary function.
Repeatedly delete states until 2 states left, replacing the transitions with regular expressions.
What does it mean to delete states?
*State elimination method.* Need at least 3 states.
#automaton(
layout: finite.layout.snake.with(columns: 2),
(
q0: (q1:("a"), q2: "b"),
q1: (q1: "a", q0: "b"),
q2: (q1: "a", q2: "b"),
)
)
Delete q2, by merging its transition $b b^* a$.
#automaton(
final: "q0",
(
q0: (q1: "a + bb*a"),
q1: (q1: "a", q0: "b")
)
)
Matrix method is more robust than the state elimination method.
*Question.* Is it possible to write a finite number of equations to answer the question $e_1 eq.quest e_2$
$(K, 0, 1, +, op(\;), (..)*)$ satisfies the following:
- K is some set
- Semi-ring
- Joint semi-lattice
- + is idempotent ($e + e equiv e$)
- + is commutative ($e + f equiv f + e$)
- + is associative ($(e + f) + g equiv e + (f + g)$)
- + has a 0 element ($e + 0 equiv e$)
- Monoid
- ; is associative ($(e ; g) ; g equiv e ; (f ; g)$)
- ; has a 1 element ($e ; 1 equiv e equiv 1 ; e$)
- ; has an absorbent element ($e ; 0 equiv 0 equiv 0 ; e$)
- ; distributes over +, both from the right and the left
- $e ; (f + g) equiv e ; f + e ; g$ AND $(e + f) ; g equiv e ; g + f ; g$
- \* is a fix point ($e^* equiv 1 + e ; e^*$)
- \* can be unfolded on the left or the right ($e^* equiv 1 + e^* ; e$)
$e^*$ is a _least_ fix point
#rect[$e <= f$ iff $e + f equiv f$]
#tree(
axi[$e;x+f <= x$],
uni[$e^*;f <= x$]
)
This forms an #link("https://en.wikipedia.org/wiki/Axiom_schema")[axiom schema].
#rect[
Exercises:
- $x^* x^* equiv x^*$
- $x^* equiv (x^*)^*$
- $x y equiv y z arrow.r.long.double x^* y equiv y z^*$
- $(a + b)^* equiv (a^* b)^* a^*$
]
Need to do it in 2 steps ($<=, >=$).
This structure is useful because there are many structures like this. For example ${2^(A^*), emptyset, {epsilon}, union, circle.filled, (..)^*}$ the set of all languages is a Kleene algebra.
Other examples:
- #[
Binary relations: $("BRel", emptyset, Delta, union, circle, (..)^*)$
- $Delta$ is the diagonal relation
- The $(..)^*$ is transitive closure
Binary relations satisfies all of the rules of a Kleene algebra.
]
- #[
Square matrices: $("Mat"(k), 0, I, +, times, (..)^*)$
- $times$ is the multiplcation associated with $k$
- #[
The star operation is defined:
$mat(a,b;c,d)^* = mat((a+b d^* c)^*, (a+b d^* c)^* b d^*;
(d+c a^* b)^* c a^*, (d+c a^* b)^*)$
This describes _every_ path from a state to another state, as many times:
#automaton(
(
q0: (q0: "a", q1: "b"),
q1: (q0: "c", q1: "d"),
)
)
]
]
*Kozen '93 result.* If two expressions $e$ and $f$ have the same language, then
$ db(e) equiv db(f) arrow.long.double.l.r e equiv f$
Switching between syntax and semantics.
_Proof method._
For every expression $e$, build an NFA $A_e$. So $e equiv f$ gets $A_e$ and $A_f$.
(Modern proofs will directly go to the DFA).
Determinize the NFAs to get $A'_e$ and $A'_f$.
Then minimize the automata to get $M_e$ and $M_f$.
#image("lec1.jpg")
Every DFA has a _unique_ minimal automaton, modulo renaming the state names.
If $e$ and $f$ represent the same language, then the minimal automata must be isomorphic.
Every $A'_e$ and $M_e$ is a matrix of expressions, and can be proven sound using the axioms of Kleene algebra.
=== Imperative programs
What is missing from $(K, 0, 1, +, op(\;), (..)*)$ for imperative programs?
- State
- Conditionals
Conditionals needs to satisfy a boolean algebra. So we need to combine a Kleene
algebra and a Boolean algebra.
Subset of $K$: $(B, 0, 1, +, ;, overline((..)))$ is a boolean algebra. _Sub-algebra_
- For B, + and ; are thought of as $or$ and $and$
- It needs to additionally satisfy demorgan laws for not
- $overline(a + b) equiv overline(a) ; overline(b)$
- $overline(a \; b) equiv overline(a) + overline(a)$
- $overline(0) equiv 1$
- $overline(overline(a)) equiv a$
- $a ; b equiv b ; a$ (not true normally!!)
This is only true of language without effects or concurrency.
- Threads can be reasoned about in a partially distributive commutative lattice

10
silva/test.fst Normal file
View file

@ -0,0 +1,10 @@
module Test
type re =
| Zero
| One
| Char of int
| Seq of re * re
| Add of re * re
| Star of re