From ade99f3f1fc2da1d51a82f1376c61ad609d60ff1 Mon Sep 17 00:00:00 2001 From: Akshay Nair Date: Tue, 12 Dec 2023 17:58:46 +0530 Subject: feat: associativity and commutativity for addition --- src/index.ts | 112 +++++++++++++++++++++++++++++------------------------------ src/nat.ts | 15 +++----- src/tests.ts | 58 +++++++++++++------------------ src/util.ts | 24 ++++++++----- 4 files changed, 100 insertions(+), 109 deletions(-) (limited to 'src') 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'; - -export type Add = { op: '+'; a: A; b: B }; -export type Succ = Add<'1', A>; - -export type Identity = Rewrite, A>; -export type Commutativity = Rewrite, Add>; - -export interface Assoc0 { - type: 'rewrite', - left: Add, B>; // (0 + a) + b - right: ChainRewrites<[ - Commutativity<'0', A>, // = (a + 0) + b - Identity, // = a + b - Flip>>, // = (a + b) + 0 - Commutativity, '0'>, // = 0 + (a + b) - ], this['left']>; -}; - -export type Assoc1 = Rewrite, B>, Succ>>; - -export interface Assoc { - type: 'rewrite', - left: Add, C>; // (a + b) + c - right: ChainRewrites<[ - Rewrite>, // = CHEATING - Assoc1, // = succ(a + b) + c - Assoc1, C>, // = succ(a + b + c) - Rewrite, // CHEATING. TODO: figure out recursion - Assoc0, // Induction base case - Rewrite<'0', A>, // CHEATING - Flip>>, // = succ(a) + (b + c) - Rewrite, A>, // = CHEATING - ], this['left']>; -}; - -// type _x = ApplyRewrite, '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) -*/ +import { Add, Multiply, Succ, _0 } from './nat'; +import { Op, Rewrite, ChainRewrites, Flip, Equation, Refl } from './util'; + +export namespace addition { + export type Identity = Rewrite, A>; + export type IdentityR = Rewrite, A>; + + export type SumSucc1 = Rewrite, B>, Succ>> + export type SumSucc2 = Rewrite>, Succ>> + + /// Sum commutativity + export type Commutativity = Rewrite, Add>; + export interface Comm_Base { + type: 'rewrite', + left: Equation, Add>; // 0 + b = b + 0 + right: ChainRewrites<[ + IdentityR, // b = b + 0 + Flip>, // b + 0 = b + 0 + Refl>, // true + ], this['left']>; + }; + export interface Comm_Inductive { + type: 'rewrite', + left: Equation, B>, Add>>; // succ(a) + b = b + succ(a) + right: ChainRewrites<[ + SumSucc1, // succ(a + b) = b + succ(a) + Commutativity, // succ(b + a) = b + succ(a) + SumSucc2, // succ(b + a) = succ(b + a) + Refl>>, // true + ], this['left']>; + }; + + // Sum associativity + export type Associativity = Rewrite, C>, Add>>; + export interface Assoc_Base { + type: 'rewrite', + left: Equation, C>, Add<'0', Add>>; // (0 + b) + c = 0 + (b + c) + right: ChainRewrites<[ + Commutativity<'0', B>, // (b + 0) + c = 0 + (b + c) + Identity, // b + c = 0 + (b + c) + IdentityR>, // b + c = b + c + Refl>, // true + ], this['left']>; + }; + export interface Assoc_Inductive { + type: 'rewrite', + left: Equation, B>, C>, Add, Add>>; // (succ(a) + b) + c = succ(a) + (b + c) + right: ChainRewrites<[ + SumSucc1, // succ(a + b) + c = succ(a) + (b + c) + SumSucc1>, // succ(a + b) + c = succ(a + (b + c)) + SumSucc1, C>, // succ((a + b) + c) = succ(a + (b + c)) + Associativity, // succ(a + (b + c)) = succ(a + (b + c)) + Refl>>>, // true + ], this['left']>; + }; +} diff --git a/src/nat.ts b/src/nat.ts index 86bd318..124c2c6 100644 --- a/src/nat.ts +++ b/src/nat.ts @@ -1,16 +1,9 @@ -declare const prev: unique symbol +import { Op } from "./util"; -export type _nat = number & { [prev]: _nat | null } -export type Succ = number & { [prev]: n } -export type Pred = n extends _0 ? n : n[typeof prev] -export type Nat = _0 | Succ<_nat> +export type Add = { op: '+'; a: A; b: B }; +export type Succ = 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] extends [b] ? ([b] extends [a] ? true : false & { a: a; b: b }) : false & { a: a; b: b }); type assert = T; export type specIdentity = [ assert>, Identity<'B'>>, + ApplyRewrite>, addition.Identity<'B'>>, Add<'A', 'B'> >>, assert, '0'>, Identity>>, + ApplyRewrite, '0'>, addition.Identity>>, Add<'A', 'B'> >>, assert, Flip>>>, + ApplyRewrite, Flip>>>, Add, '0'> >>, assert>>, Identity<'C'>>, + ApplyRewrite>>, addition.Identity<'C'>>, Add<'A', Add<'B', 'C'>> >>, ] export type specCommutativity = [ assert, Commutativity<'A', 'B'>>, + ApplyRewrite, addition.Commutativity<'A', 'B'>>, Add<'B', 'A'> >>, assert, 'C'>, Commutativity<'A', 'B'>>, + ApplyRewrite, 'C'>, addition.Commutativity<'A', 'B'>>, Add, 'C'> >>, assert>, Commutativity<'B', 'C'>>, + ApplyRewrite>, addition.Commutativity<'B', 'C'>>, Add<'A', Add<'C', 'B'>> >>, ] +export type specCommutativityInduction = [ + assert>>, + assert>>, +] + export type specChainRewrites = [ assert, - Identity<'B'>, + addition.Commutativity<'0', 'B'>, + addition.Identity<'B'>, ], Add, 'C'> >, @@ -52,10 +57,10 @@ export type specChainRewrites = [ assert, - Identity<'B'>, - Flip>>, - Commutativity, '0'>, + addition.Commutativity<'0', 'B'>, + addition.Identity<'B'>, + Flip>>, + addition.Commutativity, '0'>, ], Add, 'C'> >, @@ -63,23 +68,8 @@ export type specChainRewrites = [ >>, ] -export type specAssoc0 = [ - assert, 'C'>, Assoc0<'B', 'C'>>, - Add<'0', Add<'B', 'C'>> - >>, - assert>, 'C'>, Assoc0, 'C'>>, - Add<'0', Add, 'C'>> - >>, -] - -export type specAssocN = [ - assert, 'C'>, Assoc<'A', 'B', 'C'>>, - Add<'A', Add<'B', 'C'>> - >>, +export type specAssociativityInduction = [ + assert>>, + assert>>, ] - - 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> = ) : never; -// interface Kind { -// _: V; -// return: unknown; -// } -// type Ap = (K & { _: V })['return']; +export interface Kind { + _: V; + return: R; +} +export type Ap = (K & { _: V })['return']; export type ChainRewrites[], O extends Op> = Rws extends [] ? O - : Rws extends [infer R extends Rewrite, ...infer Rs extends Rewrite[]] - ? ChainRewrites> - : never; + : Rws extends [infer R extends Rewrite, ...infer Rs extends Rewrite[]] + ? ChainRewrites> + : never; + +export type VerifyEquation> = + Eq['right'] extends 'true' ? true : false & Eq['right']; + +export type Eq = ([a] extends [b] ? ([b] extends [a] ? true : false & { lhs: a; rhs: b }) : false & { lhs: a; rhs: b }); + +export type Equation = { op: '=', a: A, b: B }; +export type Refl = Rewrite, 'true'>; -- cgit v1.3.1