progress
[?]
Oct 23, 2023, 12:39 AM
75TM37DMPXA7YQPWZ4672OA3CUJNHYVIE5UFM2H6FHZMPGVMQS2ACDependencies
Change contents
- edit in hwk1.typ at line 1
#set document(title: "Homework 1", author: "Michael Zhang <zhan4854@umn.edu>") - edit in hwk1.typ at line 4
= Homework 1Michael Zhang \<zhan4854\@umn.edu\> - edit in hwk1.typ at line 9
- replacement in hwk1.typ at line 15
= Problem 1$#math.op("f")\(x)$== Problem 1$top : "Set"$$"case"_top$ - replacement in hwk1.typ at line 25
$ "funsplit"(f, d) &equiv d("apply"(f, (x) x)) $$ "funsplit"(f, d) &equiv d((x) "apply"(f, x)) $ - replacement in hwk1.typ at line 29
$ "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))) \ - edit in hwk1.typ at line 32
NOTE: Is it "cheating" in some sense, to use the identity abstraction $(x) x$ in the place of the last parameter to $"apply"$? - replacement in hwk1.typ at line 33
= Problem 2== Problem 2 - replacement in hwk1.typ at line 104
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$], - replacement in hwk1.typ at line 111
$ #tree($ #pad(left: -4em, tree( - replacement in hwk1.typ at line 118
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)$],)) $ - replacement in hwk1.typ at line 123
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]$], - replacement in hwk1.typ at line 127
#pagebreak()// #pagebreak() - replacement in hwk1.typ at line 129
Then, we can use this:// Then, we can use this: - replacement in hwk1.typ at line 131
#set math.equation(numbering: none)// #set math.equation(numbering: none) - replacement in hwk1.typ at line 133
#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)$],// ) - replacement in hwk1.typ at line 139
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: - replacement in hwk1.typ at line 141
#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$],// ) - replacement in hwk1.typ at line 147
Then, convert this to Eq:// Then, convert this to Eq: - replacement in hwk1.typ at line 149
#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))$],// ) - replacement in hwk1.typ at line 155
We can form a lambda term over eq objects using $lambda$-introduction:// We can form a lambda term over eq objects using $lambda$-introduction: - replacement in hwk1.typ at line 157
#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))$],// ) - replacement in hwk1.typ at line 162
This gives us what we need to perform induction over nats:// This gives us what we need to perform induction over nats: - replacement in hwk1.typ at line 164
#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[]// ) - replacement in hwk1.typ at line 169
#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[],// ) - replacement in hwk1.typ at line 174
#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]$],// ) - replacement in hwk1.typ at line 180
---#pagebreak()// ---// #pagebreak() - replacement in hwk1.typ at line 183
#{let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$]// #{// let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$] - replacement in hwk1.typ at line 186
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]$],// ) - replacement in hwk1.typ at line 191
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]$],// ) - replacement in hwk1.typ at line 197
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]$],// ) - replacement in hwk1.typ at line 202
tree(axi[$plus.circle(x, 0) equiv split1 [x in NN]$],)// tree(// axi[$plus.circle(x, 0) equiv split1 [x in NN]$],// ) - replacement in hwk1.typ at line 206
tree(axi[$split1 equiv x [x in NN]$],)// tree(// axi[$split1 equiv x [x in NN]$],// ) - replacement in hwk1.typ at line 210
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]$],)}[2.5140]// 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]$],// )// } - file addition: extraexercises.agda[3.2]
module extraexercises whereopen import Data.Natopen import Relation.Binary.PropositionalEquality as Eqopen Eq.≡-Reasoning - file addition: bidir[3.2]
- file addition: data.ts[0.3429]
/*** 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 }; - file addition: contexts.ts[0.3429]
// Helper functions for dealing with contextsimport { 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;} - file addition: bidir.ts[0.3429]
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 firstif (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 existsif (!isTypeInContext(term.type, ctx))throw new Error("type doesn't exist");// Require that the term checks against the typeconst [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[]] {}