/* canvas */ const WHITE = 0; const BLACK = 1; const UNKNOWN = 2; const canvas = window.canvas; const screen = canvas.getContext("2d"); const root = { x: [0, canvas.width], y: [0, canvas.height] }; const drawAt = (x, y, color) => { screen.fillStyle = color == WHITE ? "white" : color == BLACK ? "black" : "grey"; screen.fillRect(x[0], y[0], x[1], y[1]); }; const drawTopLeft = (ctx, color) => { const newX = [ctx.x[0], ctx.x[1] / 2]; const newY = [ctx.y[0], ctx.y[1] / 2]; drawAt(newX, newY, color); return { x: newX, y: newY }; }; const drawTopRight = (ctx, color) => { const newX = [ctx.x[1] / 2, ctx.x[1]]; const newY = [ctx.y[0], ctx.y[1] / 2]; drawAt(newX, newY, color); return { x: newX, y: newY }; }; const drawBottomLeft = (ctx, color) => { const newX = [ctx.x[0], ctx.x[1] / 2]; const newY = [ctx.y[1] / 2, ctx.y[1]]; drawAt(newX, newY, color); return { x: newX, y: newY }; }; const drawBottomRight = (ctx, color) => { const newX = [ctx.x[1] / 2, ctx.x[1]]; const newY = [ctx.y[1] / 2, ctx.y[1]]; drawAt(newX, newY, color); return { x: newX, y: newY }; }; /* lambda calculus */ const abs = (body) => { if (body === null) return null; return { type: "abs", body }; }; const app = (left) => (right) => { if (left === null || right === null) return null; return { type: "app", left, right }; }; const idx = (idx) => { if (idx === null) return null; return { type: "idx", idx }; }; const namedAbs = (name, body) => { if (body === null) return null; return { type: "named-abs", name, body }; }; const higherOrderAbs = (f) => { if (f === null) return null; return { type: "higher-order-abs", f }; }; const higherOrderApp = (a) => { if (a === null) return () => null; else if (a.type == "higher-order-abs") return a.f; else return app(a); }; const show = (term) => { if (term === null) return ""; switch (term.type) { case "abs": return `\\${show(term.body)}`; case "app": return `(${show(term.left)} ${show(term.right)})`; case "idx": return `${term.idx}`; } }; const parse = (str) => { if (!str) return [{}, ""]; const head = str[0]; const tail = str.slice(1); switch (head) { case "\\": const [body, _tail] = parse(tail); return [abs(body), _tail]; case "(": const [left, tail1] = parse(tail); const [right, tail2] = parse(tail1.slice(1)); return [app(left)(right), tail2.slice(1)]; case ")": alert("fatal"); return []; default: let num = ""; while (str && str[0] >= "0" && str[0] <= "9") { num += str[0]; str = str.slice(1); } return [idx(parseInt(num)), str]; } }; /* lambda screen */ // [[1]]=w, [[0]]=b, other=g const toColor = (term) => { if ( term.type === "abs" && term.body.type === "abs" && term.body.body.type === "idx" ) return term.body.body.idx === 1 ? WHITE : term.body.body.idx === 0 ? BLACK : UNKNOWN; return UNKNOWN; }; // [((((0 tl) tr) bl) br)] const seemsScreeny = (term) => { if ( term.type === "abs" && term.body.type === "app" && term.body.left.type === "app" && term.body.left.left.type === "app" && term.body.left.left.left.type === "app" && term.body.left.left.left.left.type === "idx" && term.body.left.left.left.left.idx === 0 ) return true; return false; }; const draw = (ctx, term) => { if (!("type" in term)) return; drawTopLeft(ctx, toColor(term.body.left.left.left.right)); drawTopRight(ctx, toColor(term.body.left.left.right)); drawBottomLeft(ctx, toColor(term.body.left.right)); drawBottomRight(ctx, toColor(term.body.right)); }; const clearScreen = () => { screen.clearRect(0, 0, canvas.width, canvas.height); }; /* beta reduction */ let MAX = 0; let depth = 0; let canceled = false; const cancelReduction = () => { if (depth++ > MAX && !canceled) { MAX **= 1.5; if ( !confirm( `This takes awfully long (${depth} steps!). The reduction potentially won't converge. Do you want to continue?\nWarning: This might crash your browser!`, ) ) { canceled = true; return true; } } return canceled; }; const toTerm = () => { depth = 0; const go = (env) => (t) => { if (cancelReduction()) return null; if (t === null) return null; switch (t.type) { case "app": return app(go(env)(t.left))(go(env)(t.right)); case "named-abs": return abs(go([t.name, ...env])(t.body)); case "idx": return idx(t.idx in env ? env[t.idx] : t.idx); default: alert("fatal error"); return null; } }; return go([]); }; const toNamedTerm = () => { depth = 0; const go = (d) => (t) => { if (cancelReduction()) return null; if (t === null) return null; switch (t.type) { case "app": return app(go(d)(t.left))(go(d)(t.right)); case "higher-order-abs": return namedAbs(d, go(d + 1)(t.f(idx(d)))); case "idx": return idx(t.idx); default: alert("fatal error"); return null; } }; return go(0); }; const toHigherOrder = () => { depth = 0; const go = (env) => (t) => { if (cancelReduction()) return null; if (t === null) return null; switch (t.type) { case "app": return higherOrderApp(go(env)(t.left))(go(env)(t.right)); case "abs": return higherOrderAbs((x) => go([x, ...env])(t.body)); case "idx": if (t.idx in env) return env[t.idx]; else return idx(t.idx); default: alert("fatal error"); return null; } }; return go([]); }; const reduce = (t) => { MAX = 16384; canceled = false; try { return toTerm()(toNamedTerm()(toHigherOrder()(t))); } catch (e) { console.error(e); alert(e); return null; } }; /* interface */ window.reductionMode.addEventListener("change", () => { const state = window.reductionMode.value; if (state === "auto") { window.slider.disabled = true; window.slider.style.opacity = 0; } else if (state === "slider") { window.slider.disabled = false; window.slider.style.opacity = 100; } else if (state === "click") { window.slider.disabled = true; window.slider.style.opacity = 0; } }); window.examples.addEventListener("change", () => { clearScreen(); window.term.value = window.examples.value; }); window.render.addEventListener("click", () => { draw( root, reduce( parse(`(${window.term.value} \\((((0 \\\\1) \\\\1) \\\\1) \\\\1)`)[0], ), ); });