lambda_calculus.ts

// http://www.kb.ecei.tohoku.ac.jp/~sumii/class/keisanki-software-kougaku-2005/lambda.pdf

type Abstraction<I extends AnyVariable, T extends AnyExpr> = [1, I, T];
type Application<T extends AnyExpr, U extends AnyExpr> = [2, T, U];
type Expr<I extends AnyVariable, T extends AnyExpr, U extends AnyExpr> = AnyVariable | Abstraction<I, T> | Application<T, U>;

type AnyVariable = string;
interface AnyAbstraction extends Abstraction<AnyVariable, AnyExpr> {};
interface AnyApplication extends Application<AnyExpr, AnyExpr> {};
type AnyExpr = AnyVariable | AnyAbstraction | AnyApplication;

function isVariable(e: AnyExpr): e is AnyVariable {
    return typeof e === "string";
}

function isAbstraction(e: AnyExpr): e is AnyAbstraction {
    return Array.isArray(e) && e[0] === 1;
}

function isApplication(e: AnyExpr): e is AnyApplication {
    return Array.isArray(e) && e[0] === 2;
}

const abstract = <I extends AnyVariable, T extends AnyExpr> (i: I, e: T): Abstraction<I, T> => [1, i, e];

const apply = <T extends AnyExpr, U extends AnyExpr> (e1: T, e2: U): Application<T, U> => [2, e1, e2];

function show(e: AnyExpr): string {
    if (isVariable(e)) {
        return e;
    } else if (isAbstraction(e)) {
        return `(\\${show(e[1])}. ${show(e[2])})`;
    } else if (isApplication(e)) {
        return `(${show(e[1])} ${show(e[2])})`;
    } else {
        throw new Error("invalid argument");
    }
}

function trace(e: AnyExpr): AnyExpr {
    console.log(show(e));
    return e;
}

function genGensym() {
    let gCounter = 0;
    return () => {
        ++gCounter;
        return `g${gCounter}`;
    }
}

const gensym = genGensym();

function substitute(e2: AnyExpr, x: AnyVariable, e1: AnyExpr): AnyExpr {
    if (isVariable(e1)) {
        return e1 === x ? e2 : e1;
    } else if (isAbstraction(e1)) {
        const s = gensym();
        const [_t, i, e] = e1;
        return abstract(s, substitute(e2, x, substitute(s, i, e)))
    } else if (isApplication(e1)) {
        const [_t, e11, e12] = e1;
        return apply(substitute(e2, x, e11), substitute(e2, x, e12));
    } else {
        throw new Error("invalid argument");
    }
}

const defaultStrategy = (e1: AnyExpr, e2: AnyExpr): AnyExpr | undefined => {
    const res0 = (() => {
        if (isAbstraction(e1)) {
            const [_t, x, e0] = e1;
            return substitute(e2, x, e0);
        } else {
            return undefined;
        }
    })();
    if (res0 !== undefined) {
        return res0;
    }
    const e1v = step(e1);
    if (e1v !== undefined) {
        return apply(e1v, e2);
    }
    const e2v = step(e2);
    if (e2v !== undefined) {
        return apply(e1, e2v);
    }
    return undefined;
}

function step(e: AnyExpr, strategy = defaultStrategy): AnyExpr | undefined {
    if (isVariable(e)) {
        return undefined;
    } else if (isAbstraction(e)) {
        const [_t, x, e0] = e;
        const e0v = step(e0);
        if (e0v !== undefined) {
            return abstract(x, e0v);
        }
        return undefined;
    } else if (isApplication(e)) {
        const [_t, e1, e2] = e;
        return strategy(e1, e2);
    } else {
        throw new Error("invalid argument");
    }
}

type RepeatHandler = (e: AnyExpr, depth: number) => void;

function repeat(e: AnyExpr, handler: RepeatHandler | undefined = undefined, strategy = defaultStrategy, limit = 65536, depth = 0): AnyExpr {
    if (handler !== undefined) {
        handler(e, depth);
    }
    if (depth >= limit) {
        throw new Error("invalid depth");
    }
    const ev = step(e, strategy);
    if (ev !== undefined) {
        return repeat(ev, handler, strategy, limit, depth + 1);
    } else {
        return e;
    }
}

const log: RepeatHandler = (e, depth) => console.log(`${depth}: ${show(e)}`);

function L<I1 extends AnyVariable, T extends AnyExpr>(is: [I1], e: T): Abstraction<I1, T>;
function L<I1 extends AnyVariable, I2 extends AnyVariable, T extends AnyExpr>(is: [I1, I2], e: T): Abstraction<I1, Abstraction<I2, T>>;
function L<I1 extends AnyVariable, I2 extends AnyVariable, I3 extends AnyVariable, T extends AnyExpr>(is: [I1, I2, I3], e: T): Abstraction<I1, Abstraction<I2, Abstraction<I3, T>>>;
function L<I1 extends AnyVariable, I2 extends AnyVariable, I3 extends AnyVariable, I4 extends AnyVariable, T extends AnyExpr>(is: [I1, I2, I3, I4], e: T): Abstraction<I1, Abstraction<I2, Abstraction<I3, Abstraction<I4, T>>>>;
function L<I extends AnyVariable, T extends AnyExpr>(is: I[], e: T): Abstraction<I, T> {
    let res: AnyAbstraction | undefined = undefined;
    if (is.length === 0) {
        throw new Error("invalid argument");
    }
    for (let idx = is.length - 1; idx >= 0; --idx) {
        if (typeof res !== "undefined") {
            res = abstract(is[idx], res);
        } else {
            res = abstract(is[idx], e);
        }
    }
    return res as Abstraction<I, T>;
}

function A<T1 extends AnyExpr, T2 extends AnyExpr>(e1: T1, e2: T2): Application<T1, T2>;
function A<T1 extends AnyExpr, T2 extends AnyExpr, T3 extends AnyExpr>(e1: T1, e2: T2, e3: T3): Application<Application<T1, T2>, T3>;
function A<T1 extends AnyExpr, T2 extends AnyExpr, T3 extends AnyExpr, T4 extends AnyExpr>(e1: T1, e2: T2, e3: T3, e4: T4): Application<Application<Application<T1, T2>, T3>, T4>;
function A<T extends AnyExpr, U extends AnyExpr>(e1: T, e2: U, ...e3s: AnyExpr[]): AnyApplication {
    let res: AnyApplication | undefined = undefined;
    const es = [e1, e2, ...e3s];
    for (let idx = 1; idx < es.length; ++idx) {
        if (typeof res !== "undefined") {
            res = apply(res, es[idx]);
        } else {
            res = apply(es[idx - 1], es[idx]);
        }
    }
    return res as AnyApplication;
}

const ZERO = L(["f", "x"], "x");
const ONE = L(["f", "x"], A("f", "x"));
const TWO = L(["f", "x"], A("f", A("f", "x")));
const SUCC = L(["n", "f", "x"], A("f", A("n", "f", "x")));
const PLUS = L(["m", "n"], A("n", SUCC, "m"));
const MULT = L(["m", "n", "f"], A("m", A("n", "f")));
const EXP = L(["m", "n"], A("n", "m"));
const PRED = L(["n", "f", "x"], A("n", L(["g", "h"], A("h", A("g", "f"))), L(["u"], "x"), L(["u"], "u")));
const MINUS = L(["m", "n"], A("n", PRED, "m"));

const TRUE = L(["x", "y"], "x");
const FALSE = L(["x", "y"], "y"); // = ZERO
const AND = L(["p", "q"], A("p", "q", FALSE));
const OR = L(["p", "q"], A("p", TRUE, "q"));
const NOT= L(["p"], A("p", FALSE, TRUE));
const IFTHENELSE = L(["p", "x", "y"], A("p", "x", "y"));
const ISZERO = L(["n"], A("n", L(["x"], FALSE), TRUE));
const LEQ = L(["m", "n"], A(ISZERO, A(MINUS, "m", "n")));
const EQ = L(["m", "n"], A(AND, A(LEQ, "m", "n"), A(LEQ, "n", "m")));
const CONS = L(["s", "b", "f"], A("f", "s", "b"));
const CAR = L(["p"], A("p", TRUE));
const CDR = L(["p"], A("p", FALSE));
const NIL = L(["x"], TRUE);
const NULL = L(["p"], A("p", L(["x", "y"], FALSE)));

const S = L(["x", "y", "z"], A(A("x", "z"), A("y", "z"))); // = A(IOTA, A(IOTA, A(IOTA, A(IOTA, IOTA))))
const K = L(["x", "y"], "x"); // = TRUE = A(IOTA, A(IOTA, A(IOTA, IOTA)))
const I = L(["x"], "x"); // = A(S, K, K) = A(IOTA, IOTA)
const IOTA = L(["x"], A("x", S, K));

const _y = L(["x"], A("f", A("x", "x")));
const Y = L(["f"], A(_y, _y));
const _z = L(["x"], A("f", L(["y"], A("x", "x", "y"))));
const Z = L(["f"], A(_z, _z));

function exprToNumberImpl(e: AnyExpr, f: AnyVariable, x: AnyVariable): number | undefined {
    if (isApplication(e)) {
        const [_t, e1, e2] = e;
        if (e1 === f) {
            const n = exprToNumberImpl(e2, f, x);
            return n !== undefined ? n + 1 : undefined;
        } else {
            return undefined;
        }
    } else if (isVariable(e)) {
        return (e === x) ? 0 : undefined;
    } else {
        return undefined;
    }
}

function exprToNumber(e: AnyExpr): number | undefined {
    if (isAbstraction(e)) {
        const [_t1, f, e1] = e;
        if (isAbstraction(e1)) {
            const [_t1, x, e2] = e1;
            return exprToNumberImpl(e2, f, x);
        } else {
            return undefined;
        }
    } else {
        return undefined;
    }
}

function numberToExpr(n: number, f: AnyVariable = "f", x: AnyVariable = "x"): AnyExpr {
    let v: AnyExpr = x;
    for (let i = 0; i < n; ++i) {
        v = A(f, v);
    }
    return L([f, x], v);
}

const fact = L(["f", "n"], A(IFTHENELSE, A(ISZERO, "n"), ONE, A(MULT, "n", A("f", A(MINUS, "n", ONE)))));
const expr = A(Y, fact, numberToExpr(3));
console.log(show(expr));
const result = repeat(expr);
console.log(show(result));
console.log(exprToNumber(result));