progress
This commit is contained in:
parent
e985f35185
commit
8ce0d1fcb6
5 changed files with 216 additions and 81 deletions
57
bidir/bidir.ts
Normal file
57
bidir/bidir.ts
Normal file
|
|
@ -0,0 +1,57 @@
|
|||
import { isTypeInContext } from "./contexts";
|
||||
import { ContextEntry, Term, Type } from "./data";
|
||||
|
||||
function check(
|
||||
ctx: ContextEntry[],
|
||||
term: Term,
|
||||
type: Type
|
||||
): [boolean, ContextEntry[]] {
|
||||
switch (term.kind) {
|
||||
case "var":
|
||||
break;
|
||||
case "unit":
|
||||
return [type.kind === "unit", ctx];
|
||||
case "lambda": {
|
||||
// Get A and B first
|
||||
if (type.kind !== "arrow") return [false, ctx];
|
||||
const { input: A, output: B } = type;
|
||||
}
|
||||
case "app":
|
||||
break;
|
||||
case "annot":
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
function synthesize(ctx: ContextEntry[], term: Term): [Type, ContextEntry[]] {
|
||||
switch (term.kind) {
|
||||
case "var": {
|
||||
const res = lookupTypeVariable(ctx, term.name);
|
||||
if (!res) throw new Error("wtf?");
|
||||
return [res, ctx];
|
||||
}
|
||||
case "unit":
|
||||
return [{ kind: "unit" }, ctx];
|
||||
case "lambda": {
|
||||
}
|
||||
case "app":
|
||||
break;
|
||||
case "annot": {
|
||||
// Require that the type exists
|
||||
if (!isTypeInContext(term.type, ctx))
|
||||
throw new Error("type doesn't exist");
|
||||
|
||||
// Require that the term checks against the type
|
||||
const [result, outputCtx] = check(ctx, term.term, term.type);
|
||||
if (!result) throw new Error("invalid annotation: term doesn't check");
|
||||
|
||||
return [term.type, outputCtx];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
function synthesizeApp(
|
||||
ctx: ContextEntry[],
|
||||
funcType: Type,
|
||||
term: Term
|
||||
): [Type, ContextEntry[]] {}
|
||||
18
bidir/contexts.ts
Normal file
18
bidir/contexts.ts
Normal file
|
|
@ -0,0 +1,18 @@
|
|||
// Helper functions for dealing with contexts
|
||||
|
||||
import { ContextEntry, Type } from "./data";
|
||||
import { isEqual } from "lodash";
|
||||
|
||||
/** Γ |- A (is the given type in this context?) */
|
||||
export function isTypeInContext(type: Type, ctx: ContextEntry[]): boolean {
|
||||
for (const entry of ctx) {
|
||||
switch (entry.kind) {
|
||||
case "termAnnot":
|
||||
if (isEqual(entry.type, type)) return true;
|
||||
break;
|
||||
default:
|
||||
continue;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
42
bidir/data.ts
Normal file
42
bidir/data.ts
Normal file
|
|
@ -0,0 +1,42 @@
|
|||
/**
|
||||
* Terms e ::= x | () | λx. e | e e | (e : A)
|
||||
* Types A, B, C ::= 1 | α | ^α | ∀α. A | A → B
|
||||
* Monotypes τ, σ ::= 1 | α | ^α | τ → σ
|
||||
* Contexts Γ, ∆, Θ ::= · | Γ, α | Γ, x : A
|
||||
* | Γ, ^α | Γ, ^α = τ | Γ, I^α
|
||||
* Complete Contexts Ω ::= · | Ω, α | Ω, x : A
|
||||
* | Ω, ^α = τ | Ω, I^
|
||||
*/
|
||||
|
||||
export type Term =
|
||||
| { kind: "var"; name: string }
|
||||
| { kind: "unit" }
|
||||
| { kind: "lambda"; name: string; body: Term }
|
||||
| { kind: "app"; func: Term; arg: Term }
|
||||
| { kind: "annot"; term: Term; type: Type };
|
||||
|
||||
export type Type =
|
||||
| { kind: "unit" }
|
||||
| { kind: "var"; name: string }
|
||||
| { kind: "existential"; name: string }
|
||||
| { kind: "poly"; name: string; type: Type }
|
||||
| { kind: "arrow"; input: Type; output: Type };
|
||||
|
||||
export type Monotype =
|
||||
| { kind: "unit" }
|
||||
| { kind: "var"; name: string }
|
||||
| { kind: "existential"; name: string }
|
||||
| { kind: "arrow"; input: Monotype; output: Monotype };
|
||||
|
||||
export type ContextEntry =
|
||||
| { kind: "typeVar"; name: string }
|
||||
| { kind: "termAnnot"; name: string; type: Type }
|
||||
| { kind: "existentialVar"; name: string }
|
||||
| { kind: "existentialSolved"; name: string; type: Monotype }
|
||||
| { kind: "marker"; name: string };
|
||||
|
||||
export type CompleteContextEntry =
|
||||
| { kind: "typeVar"; name: string }
|
||||
| { kind: "termAnnot"; name: string; type: Type }
|
||||
| { kind: "existentialSolved"; name: string; type: Monotype }
|
||||
| { kind: "marker"; name: string };
|
||||
5
extraexercises.agda
Normal file
5
extraexercises.agda
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
module extraexercises where
|
||||
|
||||
open import Data.Nat
|
||||
open import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq.≡-Reasoning
|
||||
175
hwk1.typ
175
hwk1.typ
|
|
@ -1,26 +1,36 @@
|
|||
#set document(title: "Homework 1", author: "Michael Zhang <zhan4854@umn.edu>")
|
||||
#set page("us-letter")
|
||||
#import "@preview/prooftrees:0.1.0": *
|
||||
|
||||
= Homework 1
|
||||
|
||||
Michael Zhang \<zhan4854\@umn.edu\>
|
||||
|
||||
|
||||
#let c(body) = {
|
||||
set text(gray)
|
||||
body
|
||||
}
|
||||
|
||||
= Problem 1
|
||||
$#math.op("f")\(x)$
|
||||
|
||||
== Problem 1
|
||||
|
||||
$top : "Set"$
|
||||
|
||||
$"case"_top$
|
||||
|
||||
#c[Define `funsplit` in terms of `apply`.]
|
||||
|
||||
$ "funsplit"(f, d) &equiv d("apply"(f, (x) x)) $
|
||||
$ "funsplit"(f, d) &equiv d((x) "apply"(f, x)) $
|
||||
|
||||
In the case of $f = lambda b$ the following evaluation occurs:
|
||||
|
||||
$ "funsplit"(lambda b, d) &equiv d( "apply"(lambda b, (x) x)) \
|
||||
&equiv d(((x)x)(b)) \
|
||||
$ "funsplit"(lambda b, d) &equiv d((x) "apply"(lambda b, x)) \
|
||||
&equiv d((x) (b(x))) \
|
||||
&equiv d(b) $
|
||||
|
||||
NOTE: Is it "cheating" in some sense, to use the identity abstraction $(x) x$ in the place of the last parameter to $"apply"$?
|
||||
|
||||
= Problem 2
|
||||
== Problem 2
|
||||
|
||||
#c[Assuming that you have Eq sets at your disposal, use only rules (without appealing to the One True Language) to prove:
|
||||
|
||||
|
|
@ -91,112 +101,115 @@ $ #tree(
|
|||
) $
|
||||
|
||||
$ #tree(
|
||||
axi[$x = y in NN [x in NN, y in NN]$],
|
||||
uni(right_label: "(3, 6)")[$"suc"(x) = "suc"(y) in NN [x in NN, y in NN]$],
|
||||
axi[$x in NN$],
|
||||
axi[$y in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$],
|
||||
bin(right_label: "(5)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN$],
|
||||
uni(right_label: "(3)")[$"suc"("natrec"(x, 0, (u, v) "suc"(v))) = "suc"(x) in NN$],
|
||||
uni(right_label: "natrec")[$"natrec"("suc"(x), 0, (u, v) "suc"(v))) = "suc"(x) in NN$],
|
||||
) $
|
||||
|
||||
$ #tree(
|
||||
$ #pad(left: -4em, tree(
|
||||
axi(pad(bottom: .2em, [
|
||||
$x in NN$ \
|
||||
$"Eq"(NN, "natrec"(n, 0, (u, v) "suc"(v)), n) "set" [n in NN]$ \
|
||||
$"eq"_"0" in "Eq"(NN, "natrec"(0, 0, (u, v) "suc"(v)), 0)$ \
|
||||
$"eq"_"suc" (x, y) in "Eq"(NN, "natrec"("suc"(x), 0, (u, v) "suc"(v)), "suc"(x)) [x in NN, y in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)]$ \
|
||||
])),
|
||||
uni[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$],
|
||||
) $
|
||||
uni(right_label: "(7, 9, 10)")[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$],
|
||||
)) $
|
||||
|
||||
#tree(
|
||||
axi[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$],
|
||||
uni(right_label: "(5)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],
|
||||
uni(right_label: "(5, 11)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],
|
||||
uni(right_label: [#sym.plus.circle])[$plus.circle(x, 0) = x in NN [x in NN]$],
|
||||
)
|
||||
|
||||
#pagebreak()
|
||||
// #pagebreak()
|
||||
|
||||
Then, we can use this:
|
||||
// Then, we can use this:
|
||||
|
||||
#set math.equation(numbering: none)
|
||||
// #set math.equation(numbering: none)
|
||||
|
||||
#tree(
|
||||
axi[$0 in NN$],
|
||||
uni(right_label: "(1)")[$0 = 0 in NN$],
|
||||
uni(right_label: "(3)")[$"eq"_0 in "Eq"(NN, 0, 0)$],
|
||||
)
|
||||
// #tree(
|
||||
// axi[$0 in NN$],
|
||||
// uni(right_label: "(1)")[$0 = 0 in NN$],
|
||||
// uni(right_label: "(3)")[$"eq"_0 in "Eq"(NN, 0, 0)$],
|
||||
// )
|
||||
|
||||
Using $C(x) = NN$ and the substitution-in-elements rule, we can prove that suc distributes over equivalence:
|
||||
// Using $C(x) = NN$ and the substitution-in-elements rule, we can prove that suc distributes over equivalence:
|
||||
|
||||
#tree(
|
||||
axi[$"suc"(x) in C(x) [x in NN]$],
|
||||
axi[$x = y in NN$],
|
||||
bin[$"suc"(x) = "suc"(y) in NN$],
|
||||
)
|
||||
// #tree(
|
||||
// axi[$"suc"(x) in C(x) [x in NN]$],
|
||||
// axi[$x = y in NN$],
|
||||
// bin[$"suc"(x) = "suc"(y) in NN$],
|
||||
// )
|
||||
|
||||
Then, convert this to Eq:
|
||||
// Then, convert this to Eq:
|
||||
|
||||
#tree(
|
||||
axi[$"suc"(x) = "suc"(y) in NN$],
|
||||
axi[$x = y in NN$],
|
||||
bin[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y))$],
|
||||
)
|
||||
// #tree(
|
||||
// axi[$"suc"(x) = "suc"(y) in NN$],
|
||||
// axi[$x = y in NN$],
|
||||
// bin[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y))$],
|
||||
// )
|
||||
|
||||
We can form a lambda term over eq objects using $lambda$-introduction:
|
||||
// We can form a lambda term over eq objects using $lambda$-introduction:
|
||||
|
||||
#tree(
|
||||
axi[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y)) ["eq"_"xy" in "Eq"(NN, x, y), x in NN, y in NN]$],
|
||||
uni[$lambda(("eq"_"xy") "eq"_"xy-suc") in "Eq"(NN, x, y) arrow.r "Eq"(NN, "suc"(x), "suc"(y))$],
|
||||
)
|
||||
// #tree(
|
||||
// axi[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y)) ["eq"_"xy" in "Eq"(NN, x, y), x in NN, y in NN]$],
|
||||
// uni[$lambda(("eq"_"xy") "eq"_"xy-suc") in "Eq"(NN, x, y) arrow.r "Eq"(NN, "suc"(x), "suc"(y))$],
|
||||
// )
|
||||
|
||||
This gives us what we need to perform induction over nats:
|
||||
// This gives us what we need to perform induction over nats:
|
||||
|
||||
#tree(
|
||||
axi[$"natrec"(x, "eq"_0, (u, v) "apply"(lambda(("eq"_"xy") "eq"_"xy-suc"), v)) [x in NN]$],
|
||||
uni[]
|
||||
)
|
||||
// #tree(
|
||||
// axi[$"natrec"(x, "eq"_0, (u, v) "apply"(lambda(("eq"_"xy") "eq"_"xy-suc"), v)) [x in NN]$],
|
||||
// uni[]
|
||||
// )
|
||||
|
||||
#tree(
|
||||
axi[$"i'm fucking stupid" equiv (x) "natrec"(x, 0, (u, v) "suc"(v))$],
|
||||
uni[],
|
||||
)
|
||||
// #tree(
|
||||
// axi[$"i'm fucking stupid" equiv (x) "natrec"(x, 0, (u, v) "suc"(v))$],
|
||||
// uni[],
|
||||
// )
|
||||
|
||||
#tree(
|
||||
axi[$"eq" in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$],
|
||||
uni[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],
|
||||
uni(right_label: "macro")[$plus.circle(x, 0) = x in NN [x in NN]$],
|
||||
)
|
||||
// #tree(
|
||||
// axi[$"eq" in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$],
|
||||
// uni[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],
|
||||
// uni(right_label: "macro")[$plus.circle(x, 0) = x in NN [x in NN]$],
|
||||
// )
|
||||
|
||||
---
|
||||
#pagebreak()
|
||||
// ---
|
||||
// #pagebreak()
|
||||
|
||||
#{
|
||||
let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$]
|
||||
// #{
|
||||
// let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$]
|
||||
|
||||
tree(
|
||||
axi[$"natrec"(x, "refl", (u, v) ("ap" v)) [x in NN]$],
|
||||
uni[$split1 equiv x in NN [x in NN]$],
|
||||
)
|
||||
// tree(
|
||||
// axi[$"natrec"(x, "refl", (u, v) ("ap" v)) [x in NN]$],
|
||||
// uni[$split1 equiv x in NN [x in NN]$],
|
||||
// )
|
||||
|
||||
tree(
|
||||
// axi[$c in "Eq"(NN, split1, 0), x)$],
|
||||
axi[$split1 equiv x in NN [x in NN]$],
|
||||
uni(right_label: "macro")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
|
||||
)
|
||||
// tree(
|
||||
// // axi[$c in "Eq"(NN, split1, 0), x)$],
|
||||
// axi[$split1 equiv x in NN [x in NN]$],
|
||||
// uni(right_label: "macro")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
|
||||
// )
|
||||
|
||||
tree(
|
||||
axi[$c in "Eq"(NN, plus.circle(x, 0), x)$],
|
||||
uni[$plus.circle(x, 0) equiv x in NN [x in NN]$],
|
||||
)
|
||||
// tree(
|
||||
// axi[$c in "Eq"(NN, plus.circle(x, 0), x)$],
|
||||
// uni[$plus.circle(x, 0) equiv x in NN [x in NN]$],
|
||||
// )
|
||||
|
||||
tree(
|
||||
axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
|
||||
)
|
||||
// tree(
|
||||
// axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
|
||||
// )
|
||||
|
||||
tree(
|
||||
axi[$split1 equiv x [x in NN]$],
|
||||
)
|
||||
// tree(
|
||||
// axi[$split1 equiv x [x in NN]$],
|
||||
// )
|
||||
|
||||
tree(
|
||||
axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
|
||||
axi[$split1 equiv x [x in NN]$],
|
||||
bin(right_label: "trans")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
|
||||
)
|
||||
}
|
||||
// tree(
|
||||
// axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
|
||||
// axi[$split1 equiv x [x in NN]$],
|
||||
// bin(right_label: "trans")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
|
||||
// )
|
||||
// }
|
||||
Loading…
Reference in a new issue