diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/index.ts | 104 | ||||
| -rw-r--r-- | src/nat.ts | 15 | ||||
| -rw-r--r-- | src/tests.ts | 58 | ||||
| -rw-r--r-- | src/util.ts | 24 |
4 files changed, 96 insertions, 105 deletions
diff --git a/src/index.ts b/src/index.ts index 575c446..a161134 100644 --- a/src/index.ts +++ b/src/index.ts @@ -1,57 +1,57 @@ -import { Op, Rewrite, ChainRewrites, Flip } from './util'; +import { Add, Multiply, Succ, _0 } from './nat'; +import { Op, Rewrite, ChainRewrites, Flip, Equation, Refl } from './util'; -export type Add<A extends Op, B extends Op> = { op: '+'; a: A; b: B }; -export type Succ<A extends Op> = Add<'1', A>; +export namespace addition { + export type Identity<A extends Op> = Rewrite<Add<A, _0>, A>; + export type IdentityR<A extends Op> = Rewrite<Add<_0, A>, A>; -export type Identity<A extends Op> = Rewrite<Add<A, '0'>, A>; -export type Commutativity<A extends Op, B extends Op> = Rewrite<Add<A, B>, Add<B, A>>; + export type SumSucc1<A extends Op, B extends Op> = Rewrite<Add<Succ<A>, B>, Succ<Add<A, B>>> + export type SumSucc2<A extends Op, B extends Op> = Rewrite<Add<A, Succ<B>>, Succ<Add<A, B>>> -export interface Assoc0<A extends Op, B extends Op> { - type: 'rewrite', - left: Add<Add<'0', A>, B>; // (0 + a) + b - right: ChainRewrites<[ - Commutativity<'0', A>, // = (a + 0) + b - Identity<A>, // = a + b - Flip<Identity<Add<A, B>>>, // = (a + b) + 0 - Commutativity<Add<A, B>, '0'>, // = 0 + (a + b) - ], this['left']>; -}; + /// Sum commutativity + export type Commutativity<A extends Op, B extends Op> = Rewrite<Add<A, B>, Add<B, A>>; + export interface Comm_Base<B extends Op> { + type: 'rewrite', + left: Equation<Add<_0, B>, Add<B, _0>>; // 0 + b = b + 0 + right: ChainRewrites<[ + IdentityR<B>, // b = b + 0 + Flip<Identity<B>>, // b + 0 = b + 0 + Refl<Add<B, _0>>, // true + ], this['left']>; + }; + export interface Comm_Inductive<A extends Op, B extends Op> { + type: 'rewrite', + left: Equation<Add<Succ<A>, B>, Add<B, Succ<A>>>; // succ(a) + b = b + succ(a) + right: ChainRewrites<[ + SumSucc1<A, B>, // succ(a + b) = b + succ(a) + Commutativity<A, B>, // succ(b + a) = b + succ(a) + SumSucc2<B, A>, // succ(b + a) = succ(b + a) + Refl<Succ<Add<B, A>>>, // true + ], this['left']>; + }; -export type Assoc1<A extends Op, B extends Op> = Rewrite<Add<Succ<A>, B>, Succ<Add<A, B>>>; - -export interface Assoc<A extends Op, B extends Op, C extends Op> { - type: 'rewrite', - left: Add<Add<A, B>, C>; // (a + b) + c - right: ChainRewrites<[ - Rewrite<A, Succ<A>>, // = CHEATING - Assoc1<A, B>, // = succ(a + b) + c - Assoc1<Add<A, B>, C>, // = succ(a + b + c) - Rewrite<A, '0'>, // CHEATING. TODO: figure out recursion - Assoc0<B, C>, // Induction base case - Rewrite<'0', A>, // CHEATING - Flip<Assoc1<A, Add<B, C>>>, // = succ(a) + (b + c) - Rewrite<Succ<A>, A>, // = CHEATING - ], this['left']>; -}; - -// type _x = ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, AssocN<'A', 'B', 'C'>> - -/* -Assoc: (a + b) + c = a + (b + c) - -For a = 0, -(0 + b) + c -= (b + 0) + c -- comm -= b + c -- id -= (b + c) + 0 -- flip id -= 0 + (b + c) -- comm - -For a' = succ(a), -(succ(a) + b) + c -= succ(a + b) + c -= succ((a + b) + c) ------ rec -= succ(a + (b + c)) -= succ(a) + (b + c) -*/ + // Sum associativity + export type Associativity<A extends Op, B extends Op, C extends Op> = Rewrite<Add<Add<A, B>, C>, Add<A, Add<B, C>>>; + export interface Assoc_Base<B extends Op, C extends Op> { + type: 'rewrite', + left: Equation<Add<Add<'0', B>, C>, Add<'0', Add<B, C>>>; // (0 + b) + c = 0 + (b + c) + right: ChainRewrites<[ + Commutativity<'0', B>, // (b + 0) + c = 0 + (b + c) + Identity<B>, // b + c = 0 + (b + c) + IdentityR<Add<B, C>>, // b + c = b + c + Refl<Add<B, C>>, // true + ], this['left']>; + }; + export interface Assoc_Inductive<A extends Op, B extends Op, C extends Op> { + type: 'rewrite', + left: Equation<Add<Add<Succ<A>, B>, C>, Add<Succ<A>, Add<B, C>>>; // (succ(a) + b) + c = succ(a) + (b + c) + right: ChainRewrites<[ + SumSucc1<A, B>, // succ(a + b) + c = succ(a) + (b + c) + SumSucc1<A, Add<B, C>>, // succ(a + b) + c = succ(a + (b + c)) + SumSucc1<Add<A, B>, C>, // succ((a + b) + c) = succ(a + (b + c)) + Associativity<A, B, C>, // succ(a + (b + c)) = succ(a + (b + c)) + Refl<Succ<Add<A, Add<B, C>>>>, // true + ], this['left']>; + }; +} @@ -1,16 +1,9 @@ -declare const prev: unique symbol +import { Op } from "./util"; -export type _nat = number & { [prev]: _nat | null } -export type Succ<n extends _nat> = number & { [prev]: n } -export type Pred<n extends _nat> = n extends _0 ? n : n[typeof prev] -export type Nat = _0 | Succ<_nat> +export type Add<A extends Op, B extends Op> = { op: '+'; a: A; b: B }; +export type Succ<A extends Op> = Add<'1', A>; -export type _0 = 0 & { [prev]: null } +export type _0 = '0' export type _1 = Succ<_0> export type _2 = Succ<_1> export type _3 = Succ<_2> -export type _4 = Succ<_3> -export type _5 = Succ<_4> -export type _6 = Succ<_5> -export type _7 = Succ<_6> -export type _8 = Succ<_7> diff --git a/src/tests.ts b/src/tests.ts index d56cb30..f4530b4 100644 --- a/src/tests.ts +++ b/src/tests.ts @@ -1,49 +1,54 @@ -import { Add, Assoc, Assoc0, Assoc1, Commutativity, Identity, Succ } from './index'; -import { ApplyRewrite, ChainRewrites, Flip, Rewrite } from './util'; +import { addition } from './index'; +import { Add } from './nat'; +import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation } from './util'; -type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false & { a: a; b: b }) : false & { a: a; b: b }); type assert<T extends true> = T; export type specIdentity = [ assert<Eq< - ApplyRewrite<Add<'A', Add<'B', '0'>>, Identity<'B'>>, + ApplyRewrite<Add<'A', Add<'B', '0'>>, addition.Identity<'B'>>, Add<'A', 'B'> >>, assert<Eq< - ApplyRewrite<Add<Add<'A', 'B'>, '0'>, Identity<Add<'A', 'B'>>>, + ApplyRewrite<Add<Add<'A', 'B'>, '0'>, addition.Identity<Add<'A', 'B'>>>, Add<'A', 'B'> >>, assert<Eq< - ApplyRewrite<Add<'A', 'B'>, Flip<Identity<Add<'A', 'B'>>>>, + ApplyRewrite<Add<'A', 'B'>, Flip<addition.Identity<Add<'A', 'B'>>>>, Add<Add<'A', 'B'>, '0'> >>, assert<Eq< - ApplyRewrite<Add<'A', Add<'B', Add<'C', '0'>>>, Identity<'C'>>, + ApplyRewrite<Add<'A', Add<'B', Add<'C', '0'>>>, addition.Identity<'C'>>, Add<'A', Add<'B', 'C'>> >>, ] export type specCommutativity = [ assert<Eq< - ApplyRewrite<Add<'A', 'B'>, Commutativity<'A', 'B'>>, + ApplyRewrite<Add<'A', 'B'>, addition.Commutativity<'A', 'B'>>, Add<'B', 'A'> >>, assert<Eq< - ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, Commutativity<'A', 'B'>>, + ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, addition.Commutativity<'A', 'B'>>, Add<Add<'B', 'A'>, 'C'> >>, assert<Eq< - ApplyRewrite<Add<'A', Add<'B', 'C'>>, Commutativity<'B', 'C'>>, + ApplyRewrite<Add<'A', Add<'B', 'C'>>, addition.Commutativity<'B', 'C'>>, Add<'A', Add<'C', 'B'>> >>, ] +export type specCommutativityInduction = [ + assert<VerifyEquation<addition.Comm_Base<'B'>>>, + assert<VerifyEquation<addition.Comm_Inductive<'A', 'B'>>>, +] + export type specChainRewrites = [ assert<Eq< ChainRewrites< [ - Commutativity<'0', 'B'>, - Identity<'B'>, + addition.Commutativity<'0', 'B'>, + addition.Identity<'B'>, ], Add<Add<'0', 'B'>, 'C'> >, @@ -52,10 +57,10 @@ export type specChainRewrites = [ assert<Eq< ChainRewrites< [ - Commutativity<'0', 'B'>, - Identity<'B'>, - Flip<Identity<Add<'B', 'C'>>>, - Commutativity<Add<'B', 'C'>, '0'>, + addition.Commutativity<'0', 'B'>, + addition.Identity<'B'>, + Flip<addition.Identity<Add<'B', 'C'>>>, + addition.Commutativity<Add<'B', 'C'>, '0'>, ], Add<Add<'0', 'B'>, 'C'> >, @@ -63,23 +68,8 @@ export type specChainRewrites = [ >>, ] -export type specAssoc0 = [ - assert<Eq< - ApplyRewrite<Add<Add<'0', 'B'>, 'C'>, Assoc0<'B', 'C'>>, - Add<'0', Add<'B', 'C'>> - >>, - assert<Eq< - ApplyRewrite<Add<Add<'0', Add<'A', 'B'>>, 'C'>, Assoc0<Add<'A', 'B'>, 'C'>>, - Add<'0', Add<Add<'A', 'B'>, 'C'>> - >>, -] - -export type specAssocN = [ - assert<Eq< - ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, Assoc<'A', 'B', 'C'>>, - Add<'A', Add<'B', 'C'>> - >>, +export type specAssociativityInduction = [ + assert<VerifyEquation<addition.Assoc_Base<'B', 'C'>>>, + assert<VerifyEquation<addition.Assoc_Inductive<'A', 'B', 'C'>>>, ] - - diff --git a/src/util.ts b/src/util.ts index 5556f70..f6067ae 100644 --- a/src/util.ts +++ b/src/util.ts @@ -18,14 +18,22 @@ export type ApplyRewrite<O extends Op, R extends Rewrite<Op, Op>> = ) : never; -// interface Kind<V = unknown> { -// _: V; -// return: unknown; -// } -// type Ap<K extends Kind, V> = (K & { _: V })['return']; +export interface Kind<V = unknown, R = unknown> { + _: V; + return: R; +} +export type Ap<K extends Kind, V> = (K & { _: V })['return']; export type ChainRewrites<Rws extends Rewrite<Op, Op>[], O extends Op> = Rws extends [] ? O - : Rws extends [infer R extends Rewrite<Op, Op>, ...infer Rs extends Rewrite<Op, Op>[]] - ? ChainRewrites<Rs, ApplyRewrite<O, R>> - : never; + : Rws extends [infer R extends Rewrite<Op, Op>, ...infer Rs extends Rewrite<Op, Op>[]] + ? ChainRewrites<Rs, ApplyRewrite<O, R>> + : never; + +export type VerifyEquation<Eq extends Rewrite<Op, Op>> = + Eq['right'] extends 'true' ? true : false & Eq['right']; + +export type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false & { lhs: a; rhs: b }) : false & { lhs: a; rhs: b }); + +export type Equation<A extends Op, B extends Op> = { op: '=', a: A, b: B }; +export type Refl<A extends Op> = Rewrite<Equation<A, A>, 'true'>; |