Initial ideas

author: Marvin Borner 2024-04-04 00:55:34 +0200
committer: Marvin Borner 2024-04-04 00:55:34 +0200
commit: 0575e54f88f481acfdeb0500002c1cfabba29d4c (patch)
tree: 7d8c8cc159dae9acba2598b0dfc693c009c6513f
4 files changed, 456 insertions, 0 deletions
diff --git a/bruijn/Screen.bruijn b/bruijn/Screen.bruijn
new file mode 100644
index 0000000..f132c66
--- /dev/null
+++ b/bruijn/Screen.bruijn
@@ -0,0 +1,76 @@
+# MIT License, Copyright (c) 2024 Marvin Borner
+
+:import std/Combinator .
+
+# white pixel
+w k
+
+# black pixel
+b ki
+
+# returns true if pixel is white
+# TODO: what about recursive structures?
+w? [0]
+
+:test (w? w) ([[1]])
+:test (w? b) ([[0]])
+
+# returns true if pixel is black
+# TODO: what about recursive structures?
+b? [0 b w]
+
+:test (b? w) ([[0]])
+:test (b? b) ([[1]])
+
+# inverts pixel color
+invert c
+
+:test (invert w) (b)
+:test (invert b) (w)
+
+build [[[[[0 4 3 2 1]]]]]
+
+empty build b b b b
+
+# id/getter of top left pixel
+tl [[[[3]]]]
+
+# id/getter of top right pixel
+tr [[[[2]]]]
+
+# id/getter of bottom left pixel
+bl [[[[1]]]]
+
+# id/getter of bottom right pixel
+br [[[[0]]]]
+
+# extracts pixel at position
+get t
+
+:test (get tl (build w b b b)) (w)
+:test (get bl (build b b w b)) (w)
+
+# updates top left pixel
+tl! [[1 [[[[[0 5 3 2 1]]]]]]]
+
+:test (tl! empty w) (build w b b b)
+
+# updates top right pixel
+tr! [[1 [[[[[0 4 5 2 1]]]]]]]
+
+:test (tr! empty w) (build b w b b)
+
+# updates bottom left pixel
+bl! [[1 [[[[[0 4 3 5 1]]]]]]]
+
+:test (bl! empty w) (build b b w b)
+
+# updates bottom right pixel
+br! [[1 [[[[[0 4 3 2 5]]]]]]]
+
+:test (br! empty w) (build b b b w)
+
+# maps each pixel to a function
+map [&[[[[[0 (5 4) (5 3) (5 2) (5 1)]]]]]]
+
+:test (map invert empty) (build w w w w)
diff --git a/index.html b/index.html
new file mode 100644
index 0000000..c186f6c
--- /dev/null
+++ b/index.html
@@ -0,0 +1,49 @@
+<!doctype html>
+<html>
+  <head>
+    <meta charset="UTF-8" />
+    <meta name="viewport" content="width=device-width" />
+    <title>Lambda Screen</title>
+    <link rel="stylesheet" href="style.css" type="text/css" media="all" />
+  </head>
+  <body>
+    <main>
+      <canvas height="800" width="800" id="canvas"></canvas>
+      <div>
+        <div class="inputWrap">
+          Reduction mode:
+          <select id="reductionMode">
+            <option value="auto" selected>Reduce to normal form</option>
+            <option value="slider">Reduce by sliding</option>
+            <option value="click">Reduce by clicking</option>
+          </select>
+        </div>
+        <input type="range" min="0" max="20" value="0" id="slider" />
+      </div>
+      <div>
+        <div class="inputWrap">
+          Load preset:
+          <select id="examples">
+            <option value="" selected disabled hidden></option>
+            <option value="\0">Identity</option>
+            <option value="\\((((0 \\0) \\0) \\0) \\0)">Just black</option>
+            <option
+              value="\(0 \\\\\((((0 \\((6 0) 1)) \\((5 0) 1)) \\((4 0) 1)) \\((3 0) 1)))"
+            >
+              Invert
+            </option>
+          </select>
+        </div>
+        <input
+          type="text"
+          placeholder="e.g. \(0...) or 000110... (BLC)"
+          value=""
+          name="term"
+          id="term"
+        />
+      </div>
+      <button id="render">Render!</button>
+    </main>
+    <script src="script.js"></script>
+  </body>
+</html>
diff --git a/script.js b/script.js
new file mode 100644
index 0000000..f5d1b8a
--- /dev/null
+++ b/script.js
@@ -0,0 +1,281 @@
+/* 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],
+    ),
+  );
+});
diff --git a/style.css b/style.css
new file mode 100644
index 0000000..364ae86
--- /dev/null
+++ b/style.css
@@ -0,0 +1,50 @@
+html, body {
+    padding: 0;
+    margin: 0;
+    width: 100%;
+    background-color: #fafafa;
+}
+
+main {
+    width: min(80vh, 90vw);
+    display: flex;
+    align-items: center;
+    justify-content: space-around;
+    flex-direction: column;
+    margin: 0 auto;
+}
+
+main > * {
+    width: 100%;
+    margin: 16px;
+}
+
+canvas {
+    max-height: min(80vh, 90vw);
+    max-width: 100%;
+    width: auto;
+    flex-basis: auto;
+    border: 1px solid black;
+}
+
+input#slider {
+    width: 100%;
+    opacity: 0;
+}
+
+input#term {
+    width: 100%;
+    font-size: 2em;
+}
+
+button#render {
+    width: 100%;
+    height: 3em;
+    font-size: 2em;
+}
+
+.inputWrap {
+    display: block;
+    margin: 0 auto;
+    width: fit-content;
+}
author	Marvin Borner	2024-04-04 00:55:34 +0200
committer	Marvin Borner	2024-04-04 00:55:34 +0200
commit	0575e54f88f481acfdeb0500002c1cfabba29d4c (patch)
tree	7d8c8cc159dae9acba2598b0dfc693c009c6513f