aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/equation.ts9
-rw-r--r--src/lambda-calculus.ts114
-rw-r--r--src/utils/theorem.ts7
3 files changed, 122 insertions, 8 deletions
diff --git a/src/equation.ts b/src/equation.ts
index 0ec25d6..cc668b1 100644
--- a/src/equation.ts
+++ b/src/equation.ts
@@ -1,4 +1,4 @@
-import { Op, Rewrite, ChainRewrites, Sym, Equation, VerifyEquation, assert, ApplyRewrite, Evaluate, OpToStr } from './utils/theorem';
+import { Op, Rewrite, ChainRewrites, Sym, Equation, VerifyEquation, assert, ApplyRewrite, Evaluate, OpToStr, SubstEq } from './utils/theorem';
export namespace equation {
type F<X extends Op> = { op: 'F', a: X };
@@ -9,7 +9,6 @@ export namespace equation {
export type Congruence<A extends Op, B extends Op> = Rewrite<Equation<A, B>, Equation<F<A>, F<B>>>;
- export type SubstituteEq<O extends Equation<Op, Op>> = Rewrite<O['a'], O['b']>
export interface SubstituteEq_Proof<A extends Op, B extends Op> {
type: 'rewrite',
known: {
@@ -18,7 +17,7 @@ export namespace equation {
left: Equation<F<A>, F<B>>; // f(a) = f(b)
right: ChainRewrites<[
Sym<Congruence<A, B>>, // a = b
- SubstituteEq<this['known']['a = b']>, // b = b
+ SubstEq<this['known']['a = b']>, // b = b
Reflexivity<B>,
], this['left']>;
};
@@ -36,8 +35,8 @@ export namespace equation {
},
left: Equation<Equation<A, B>, Equation<B, C>>; // (a = b) = (b = c)
right: ChainRewrites<[
- SubstituteEq<this['known']['a = b']>, // (b = b) = (b = c)
- SubstituteEq<ApplyRewrite<this['known']['b = c'], Symmetry<B, C>>>, // (b = b) = (c = b)
+ SubstEq<this['known']['a = b']>, // (b = b) = (b = c)
+ SubstEq<ApplyRewrite<this['known']['b = c'], Symmetry<B, C>>>, // (b = b) = (c = b)
Reflexivity<B>, // true = (b = b)
Reflexivity<B>, // true = true
Reflexivity<'true'>,
diff --git a/src/lambda-calculus.ts b/src/lambda-calculus.ts
new file mode 100644
index 0000000..bbd2d1e
--- /dev/null
+++ b/src/lambda-calculus.ts
@@ -0,0 +1,114 @@
+import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, Subst, ApplyRewrite, Evaluate, OpToStr, SubstEq } from './utils/theorem';
+
+export type Abs<x extends Op, o extends Op> = { op: '->', a: x, b: o }; // \x. o
+export type Ap<F extends Op, x extends Op> = { op: '$', a: F, b: x }; // F(x)
+export type Comp<F extends Op, G extends Op> = { op: '.', a: F, b: G }; // F . G
+export type Id<x extends Op = 'x'> = Abs<x, x> // \x. x
+export type Const<x extends Op = 'x', y extends Op = 'y'> = Abs<x, Abs<y, x>> // \x. \y. x
+export type Inv<F extends Op> = { op: 'inv', a: F }
+
+export namespace composition {
+ export type Abstraction<x extends Op, y extends Op, v extends Op> = Rewrite<Ap<Abs<x, y>, v>, y>;
+
+ export type Composition<F extends Op, G extends Op, x extends Op> = Rewrite<Ap<Comp<F, G>, x>, Ap<F, Ap<G, x>>>;
+
+ // Identity
+ export type Identity<x extends Op> = Rewrite<Ap<Id, x>, x>;
+ export namespace proof {
+ export interface Identity_Proof<x extends Op> {
+ type: 'rewrite';
+ left: Equation<Ap<Id<x>, x>, x>; // id(x) = x
+ right: ChainRewrites<[
+ Abstraction<x, x, x>, // x = x
+ Refl,
+ ], this['left']>;
+ }
+
+ export interface Identity_Composition_Proof<F extends Op, x extends Op> {
+ type: 'rewrite';
+ left: Equation<Ap<Comp<F, Id>, x>, Ap<F, x>>; // (f . id)(x) = f(x)
+ right: ChainRewrites<[
+ Composition<F, Id, x>, // f(id(x)) = f(x)
+ Identity<x>, // f(x) = f(x)
+ Refl,
+ ], this['left']>;
+ }
+
+ export type identity = [
+ assert<VerifyEquation<Identity_Proof<'x'>>>,
+ assert<VerifyEquation<Identity_Composition_Proof<'F', 'x'>>>,
+ ]
+ }
+
+ // Associativity
+ export type Associativity<F extends Op, G extends Op, H extends Op> = Rewrite<
+ Comp<Comp<F, G>, H>,
+ Comp<F, Comp<G, H>>
+ >
+ export namespace proof {
+ export interface Assoc_Proof<F extends Op, G extends Op, H extends Op, x extends Op> {
+ type: 'rewrite';
+ left: Equation<Ap<Comp<Comp<F, G>, H>, x>, Ap<Comp<F, Comp<G, H>>, x>>; // ((f . g) . h)(x) = (f . (g . h))(x)
+ right: ChainRewrites<[
+ Composition<Comp<F, G>, H, x>, // (f . g)(h(x)) = (f . (g . h))(x)
+ Composition<F, G, Ap<H, x>>, // f(g(h(x))) = (f . (g . h))(x)
+ Composition<F, Comp<G, H>, x>, // f(g(h(x))) = f((g . h)(x))
+ Composition<G, H, x>, // f(g(h(x))) = f(g(h(x)))
+ Refl,
+ ], this['left']>;
+ }
+ export type associativity = [
+ assert<VerifyEquation<Assoc_Proof<'F', 'G', 'H', 'x'>>>,
+ ]
+ }
+
+ // Identity
+ export type Transitivity<x extends Op, y extends Op, z extends Op> = Rewrite<Comp<Abs<y, z>, Abs<x, y>>, Abs<x, z>>;
+ export namespace proof {
+ export interface Transitivity_Proof<x extends Op, y extends Op, z extends Op> {
+ type: 'rewrite';
+ left: Equation<Ap<Comp<Abs<y, z>, Abs<x, y>>, x>, Ap<Abs<x, z>, x>>; // ((\y -> z) . (\x -> y))(x) = (\x -> z)(x)
+ right: ChainRewrites<[
+ Composition<Abs<y, z>, Abs<x, y>, x>, // (\y -> z) $ (\x -> y)(x) = (\x -> z)(x)
+ Abstraction<x, y, x>, // (\y -> z) $ y = (\x -> z)(x)
+ Abstraction<y, z, y>, // z = (\x -> z)(x)
+ Abstraction<x, z, x>, // z = z
+ Refl,
+ ], this['left']>;
+ }
+ export type transitivity = [
+ // OpToStr<Evaluate<Transitivity_Proof<'x', 'y', 'z'>>>,
+ assert<VerifyEquation<Transitivity_Proof<'x', 'y', 'z'>>>,
+ ]
+ }
+
+ // Inverse functions
+ export type Inverse<x extends Op, y extends Op> = Rewrite<Inv<Abs<x, y>>, Abs<y, x>>;
+ export namespace proof {
+ export interface Composition_Inverse_Proof<F extends Op, G extends Op> {
+ type: 'rewrite',
+ known: {
+ 'f': Equation<F, Abs<'y', 'z'>>,
+ 'g': Equation<G, Abs<'x', 'y'>>,
+ },
+ left: Equation<Inv<Comp<F, G>>, Comp<Inv<G>, Inv<F>>>, // inv(f . g) = inv(g) . inv(f)
+ right: ChainRewrites<[
+ SubstEq<this['known']['f']>,
+ SubstEq<this['known']['f']>, // inv((\y -> z) . g) = inv(g) . inv(\y -> z)
+ SubstEq<this['known']['g']>,
+ SubstEq<this['known']['g']>, // inv((\y -> z) . (\x -> y)) = inv(\x -> y) . inv(\y -> z)
+ Inverse<'x', 'y'>,
+ Inverse<'y', 'z'>, // inv((\x -> y) . (\y -> z)) = (\z -> y) . (\y -> x)
+ Transitivity<'x', 'y', 'z'>, // inv(\x -> z) = (\z -> y) . (\y -> x)
+ Transitivity<'z', 'y', 'x'>, // inv(\x -> z) = \z -> x
+ Inverse<'x', 'z'>, // \z -> x = \z -> x
+ Refl
+ ], this['left']>,
+ }
+ export type inverse = [
+ // OpToStr<Evaluate<Composition_Inverse_Proof<'F', 'G'>>>,
+ assert<VerifyEquation<Composition_Inverse_Proof<'F', 'G'>>>,
+ ]
+ }
+}
+
diff --git a/src/utils/theorem.ts b/src/utils/theorem.ts
index a4dd2e9..be19b94 100644
--- a/src/utils/theorem.ts
+++ b/src/utils/theorem.ts
@@ -6,9 +6,9 @@ export type OpToStr<O extends Op> =
O extends string
? O
: O extends { op: string, a: infer a extends string, b: infer b extends string } ? `(${a} ${O['op']} ${b})`
- : O extends { op: string, a: infer a extends DyadicOp, b: infer b extends string } ? `(${OpToStr<a>} ${O['op']} ${b})`
- : O extends { op: string, a: infer a extends string, b: infer b extends DyadicOp } ? `(${a} ${O['op']} ${OpToStr<b>})`
- : O extends { op: string, a: infer a extends DyadicOp, b: infer b extends DyadicOp } ? `(${OpToStr<a>} ${O['op']} ${OpToStr<b>})`
+ : O extends { op: string, a: infer a extends DyadicOp | MonadicOp, b: infer b extends string } ? `(${OpToStr<a>} ${O['op']} ${b})`
+ : O extends { op: string, a: infer a extends string, b: infer b extends DyadicOp | MonadicOp } ? `(${a} ${O['op']} ${OpToStr<b>})`
+ : O extends { op: string, a: infer a extends DyadicOp | MonadicOp, b: infer b extends DyadicOp | MonadicOp } ? `(${OpToStr<a>} ${O['op']} ${OpToStr<b>})`
: O extends { op: string, a: infer a extends string } ? `${O['op']}(${a})`
: O extends { op: string, a: infer a extends DyadicOp } ? `${O['op']}(${OpToStr<a>})`
: never;
@@ -30,6 +30,7 @@ export interface Rewrite<left extends Op, right extends Op, Typ extends RwType =
export type Sym<R extends RewriteBase> = Rewrite<R['right'], R['left'], R['type']>;
export type Subst<A extends Op, B extends Op> = Rewrite<A, B>
+export type SubstEq<O extends Equation<Op, Op>> = Rewrite<O['a'], O['b']>
export type ApplyRewrite<O extends Op, R extends RewriteBase> =
R['type'] extends 'imperative' ? (R & { left: O })['right']