Skip to content

Instantly share code, notes, and snippets.

@mheiber

mheiber/proving stuff in typescript.ts

Last active August 11, 2024 16:01
Show Gist options
  • Save mheiber/731a1e3a736487338d7a7e79d4b94408 to your computer and use it in GitHub Desktop.
Save mheiber/731a1e3a736487338d7a7e79d4b94408 to your computer and use it in GitHub Desktop.
Download ZIP
proving stuff in typescript.ts
Raw
proving stuff in typescript.ts
// We prove this theorem: forall A,B,C. A \/ B -> C <-> (A -> C) /\ (B -> C)
// by representing the theorem as a type and showing the type is inhabited.
// To show type inhabitation, we make a value of the type.
// Note: this proof actually demonstrates something practical in programming:
// part of why the visitor pattern can be helpful in OO languages that don't have
// much support for sum types ("or"/algebraic data types) but do have product types ("and"/records).
// https://cs.stackexchange.com/questions/139003/is-there-a-relationship-between-visitor-pattern-and-demorgans-law
type Theorem<A, B, C> = Iff<
((either: Or<A, B>) => C),
And<(a: A) => C, (b: B) => C>
>;
type Or<T, U> =
| {tag: 'orLeft', value: T}
| {tag: 'orRight', value: U};
type And<A, B> = {andLeft: A, andRight: B};
type If<A, B> = (a: A) => B
type Iff<A, B> = And<If<A, B>, If<B, A>>;
// 'forall' is interpreted as a generic function
// uses some helpers below
function proof<A, B, C>(): Theorem<A, B, C> {
const leftToRight: (fn: (either: Or<A, B>) => C) => And<If<A, C>, If<B, C>> =
(or_to_c) => ({
andLeft: a => or_to_c(orIntroLeft(a)),
andRight: b => or_to_c(orIntroRight(b)),
});
const rightToLeft: (and: And<If<A, C>, If<B, C>>) => (either: Or<A, B>) => C =
({andLeft, andRight}) => (or: Or<A, B>): C => {
switch (or.tag) {
case 'orLeft':
const a: A = or.value;
return andLeft(a);
case 'orRight':
const b: B = or.value;
return andRight(b);
default:
or satisfies never;
return or;
}
}
return {andLeft: leftToRight, andRight: rightToLeft};
}
// helpers to create an `Or` and take apart an `Or`.
// We don't create such helpers for `And`
// because creating and taking apart objects is easy in TypeScript
function orIntroLeft<A, B>(orLeft: A): Or<A, B> {
return {tag: 'orLeft', value: orLeft};
}
function orIntroRight<A, B>(orRight: B): Or<A, B> {
return {tag: 'orRight', value: orRight};
}
// We proved a theorem by showing that a type was inhabited.
// This deep connection between logic and type theory
// is the insight of https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
// and https://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf.
// The latter is hard to read due to notation, imo. The first chapter of the (free)
// HoTT book I find much more accessible, and better at comparing with set theory.
// https://homotopytypetheory.org/book/ (no topology in the first chapter).
// A bunch more proofs that show the relationships between theorems of classical logic
// and when we have to assume excluded middle/double-negation-elimmination
type Not<T> = (t: T) => never;
type ExcludedMiddle<T> = Or<T, Not<T>>;
const todo = Symbol('todo'); // helpful when proving bit-by-bit, since there is only one value of this type
// not provable (without infinite-looping, throwing, assuming something equivalent, or otherwise cheating)
function proofOfExcludedMiddle<T>(t: T): ExcludedMiddle<T> {
return todo; // ??
}
type Person = {height: number, punctual: boolean};
const aPerson: Person = {height: 1, punctual: true};
// But of course it would be super weird if we could summon an excluded middle for any type
// out of thin air
function useExcludedMiddleOfPerson(em: ExcludedMiddle<Person>): boolean {
switch (em.tag) {
case "orLeft":
// where could this person come from?
const person = em.value;
return person.punctual;
case "orRight":
return em.value(aPerson);
default:
em satisfies never;
return em;
}
}
// "Faustian bargain"
function proofOfNotNotExcludedMiddle<T>(): Not<Not<ExcludedMiddle<T>>> {
return (notExcludedMiddle) => notExcludedMiddle(orIntroRight((t: T) => notExcludedMiddle(orIntroLeft(t))))
}
const notNotExcludedMiddleOfPerson: Not<Not<ExcludedMiddle<Person>>> = proofOfNotNotExcludedMiddle();
notNotExcludedMiddleOfPerson((em: ExcludedMiddle<Person>): never => {
switch (em.tag) {
case "orLeft":
// it looks like we get a Person value out of nowhere,
// but really it's the person we provide in the "orRight" case
const _p: Person = em.value;
console.log(_p)
return todo; // ???
case "orRight":
const notPerson: Not<Person> = em.value;
notPerson(aPerson);
default:
em satisfies never
return em;
}
})
type DoubleNegationIntro<A> = (a: A) => Not<Not<A>>
function proofOfDoubleNegationIntro<A>(): DoubleNegationIntro<A> {
return (a: A): Not<Not<A>> => (notA: Not<A>): never => notA(a);
}
type DoubleNegationElim<A> = (notNot: Not<Not<A>>) => A;
function proofOfDoubleNegationElim<A>(excludedMiddle: ExcludedMiddle<A>): DoubleNegationElim<A> {
return (notNot: Not<Not<A>>): A => {
switch (excludedMiddle.tag) {
case 'orLeft':
const a: A = excludedMiddle.value;
return a;
case 'orRight':
const notA: Not<A> = excludedMiddle.value;
return notNot(notA); // use of exfalso
default:
excludedMiddle satisfies never;
return excludedMiddle;
}
}
}
type CounterexamplePrinciple<A, B> = If<Not<If<A, B>>, And<A, Not<B>>>
function proofOfCounterexamplePrinciple<A, B>(excludedMiddle: <T>() => ExcludedMiddle<T>): CounterexamplePrinciple<A, B> {
return (notIf: Not<If<A, B>>): And<A, Not<B>> => {
const emA = excludedMiddle<A>();
const emB = excludedMiddle<B>();
switch(emA.tag) {
case "orLeft": {
const a: A = emA.value;
switch (emB.tag) {
case "orLeft": {
const b: B = emB.value;
return notIf((_) => b);
}
case "orRight": {
const notB: Not<B> = emB.value;
return {andLeft: a, andRight: notB};
}
default:
emB satisfies never;
return emB;
}
}
case "orRight": {
const notA: Not<A> = emA.value;
const aToB = (a: A): never => notA(a);
return notIf(aToB); // exfalso
}
default:
emA satisfies never;
return emA;
}
}
}
type HalfDeMorgansLaw<A, B> = (or: Or<Not<A>, Not<B>>) => Not<And<A, B>>;
type DeMorgansLaw<A, B> = Iff<Not<And<A, B>>, Or<Not<A>, Not<B>>>
function proofOfHalfDemorgansLaw<A, B>(): HalfDeMorgansLaw<A, B> {
return (or: Or<Not<A>, Not<B>>): Not<And<A, B>> => {
switch (or.tag) {
case "orLeft":
const notA: Not<A> = or.value;
return (and: And<A, B>) => notA(and.andLeft);
case "orRight":
const notB: Not<B> = or.value;
return (and: And<A, B>) => notB(and.andRight);
default:
or satisfies never;
return or;
}
}
}
function proofOfDemorgansLaw<A, B>(excludedMiddle: <T>() => ExcludedMiddle<T>): DeMorgansLaw<A, B> {
return {
andLeft: (notBoth: Not<And<A, B>>): Or<Not<A>, Not<B>> => {
const emA = excludedMiddle<A>();
const emB = excludedMiddle<B>();
switch(emA.tag) {
case "orLeft": {
const a: A = emA.value;
switch (emB.tag) {
case "orLeft": {
const b: B = emB.value;
return notBoth({andLeft: a, andRight: b})
}
case "orRight": {
const notB: Not<B> = emB.value;
return orIntroRight(notB);
}
default:
emB satisfies never;
return emB;
}
}
case "orRight": {
const notA: Not<A> = emA.value;
return orIntroLeft(notA);
}
}
},
andRight: proofOfHalfDemorgansLaw(),
}
}
type TarskisFormula<A, B> = Or<A, If<A, B>>;
function proofOfTarskisFormula<A, B>(emA: ExcludedMiddle<A>): TarskisFormula<A, B> {
switch (emA.tag) {
case 'orLeft': {
const a: A = emA.value;
return orIntroLeft(a);
}
case 'orRight': {
const notA: Not<A> = emA.value;
return orIntroRight((a: A): B => notA(a) /*exfalso*/);
}
default:
emA satisfies never;
return emA;
}
}
type Linearity<A, B, C> = Or<If<A, B>, If<B, C>>;
function proofOfLinearity<A, B, C>(emB: ExcludedMiddle<B>): Linearity<A, B, C> {
switch (emB.tag) {
case "orLeft": {
const b: B = emB.value;
return orIntroLeft((_: A) => b);
}
case "orRight": {
const notB: Not<B> = emB.value;
return orIntroRight(notB);
}
default:
emB satisfies never;
return emB;
}
}
type ClaviusLaw<A> = If<If<Not<A>, A>, A>;
function proofOfClaviusLaw<A>(emA: ExcludedMiddle<A>): ClaviusLaw<A> {
return (ifNotAA: If<Not<A>, A>): A => {
switch (emA.tag) {
case 'orLeft': {
const a: A = emA.value;
return a;
}
case 'orRight': {
const notA: Not<A> = emA.value;
return ifNotAA(notA);
}
default:
emA satisfies never;
return emA;
}
}
}
function proofOfExcludedMiddleFromDoubleNegationElim<A>(notNotElim: <T>() => DoubleNegationElim<T>): ExcludedMiddle<A> {
return notNotElim<ExcludedMiddle<A>>()(proofOfNotNotExcludedMiddle<A>());
}
type PiercesLaw<A, B> = If<If<If<A, B>, A>, A>;
function proofOfPiercesLaw<A, B>(emA: ExcludedMiddle<A>): PiercesLaw<A, B> {
return (ifIfAA: If<If<A, B>, A>): A => {
switch (emA.tag) {
case 'orLeft': {
const a: A = emA.value;
return a;
}
case 'orRight': {
const notA: Not<A> = emA.value;
return ifIfAA(notA); // exfalso
}
default:
emA satisfies never;
return emA;
}
}
}
type WeakExcludedMiddle<A> = Or<Not<A>, Not<Not<A>>>;
function proofOfWeakExcludedMiddle<A>(emA: ExcludedMiddle<A>): WeakExcludedMiddle<A> {
switch (emA.tag) {
case 'orLeft': {
const a: A = emA.value;
return orIntroRight(proofOfDoubleNegationIntro<A>()(a));
}
case 'orRight': {
const notA: Not<A> = emA.value;
return orIntroLeft(notA);
}
default:
emA satisfies never;
return emA;
}
}
type NotNotDoubleNegationElim<A> = If<Not<Not<Not<Not<A>>>>, Not<Not<A>>>;
function proofOfNotNotDoubleNegationElim<A>(): NotNotDoubleNegationElim<A> {
return (fourNot: Not<Not<Not<Not<A>>>>): Not<Not<A>> =>
(notA: Not<A>): never => {
const threeNot: Not<Not<Not<A>>> = proofOfDoubleNegationIntro<Not<A>>()(notA);
return fourNot(threeNot);
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment