31:Tbf7,function redchart (t, options) { options = _.defaults(options, { labels: true, dist: 30, strength: -800, height: 400, N: 10, scale: 1, title: '', decay: 0.0228, }); const { nodes, links } = graph(t); nodes.forEach(n => n.r = 5); const labels = nodes.map(n => ({ text: n.term })); const height = options.height; const simulation = d3.forceSimulation(nodes).alphaDecay(options.decay) .force("link", d3.forceLink(links).id(d => d.term).distance(options.dist)) .force("charge", d3.forceManyBody().strength(options.strength)) .force("center", d3.forceCenter((width / 2)/options.scale, (height / 2)/options.scale)); const svg = d3.select(DOM.svg(width, height)); const g_scale = svg.append('g').attr('transform', `scale(${options.scale})`); const g_links = g_scale.append('g'); const g_labels = g_scale.append('g'); const g_nodes = g_scale.append('g'); svg.append("defs").append('marker') .attr('id', 'arrowhead') .attr('viewBox', "0 -10 20 20") .attr('refX', 24) .attr('refY', 0) .attr('markerWidth', 10) .attr('markerHeight', 10) .attr('orient', "auto") .append("path") .attr("d", "M0,-7 L10,0 L0,7") .attr('fill', '#999') .attr('stroke', '#999'); const link = g_links .attr("stroke", "#999") .attr("stroke-opacity", 0.6) .selectAll("path") .data(links) .enter().append("path") .attr("marker-end", "url(#arrowhead)"); const node = g_nodes.selectAll("g.node").data(nodes) .enter() .append('g').attr('class', 'node') .attr("stroke-width", 1.5) .attr('style', 'cursor: pointer;'); node.append("circle") .attr("stroke", "#fff") .attr("r", 5); node.call(drag(simulation)); node.append("title") .text(d => d.term); var label; if (options.labels) { label = g_labels.selectAll("text").data(nodes) .enter().append("text") .attr("dy", -6) .attr("dx", 5) .attr("fill", '#555') .attr('style', 'font-family: monospace; font-size: 12px;') .text(d => d.term) .attr('textLength', d => d.term.length * 6); } const line = d3.line(); simulation.on('tick', function ticked () { link .attr('d', d => line([ [d.source.x, d.source.y], [d.target.x, d.target.y], ])); node.attr('transform', d => `translate(${d.x} ${d.y})`); if (options.labels) { label.attr('transform', d => `translate(${d.x} ${d.y})`); } }); const root = DOM.element('div', { style: 'border-bottom: 1px solid #666;' }); root.appendChild(html`

Reduction graph for:

 ${dispb(t)}

${options.title ? `

${options.title}

` : ''}

`); root.appendChild(svg.node()); return root; }32:T654,function redtable (t, N = 10) { const scale = .8; var term = bruijnify(t); const images = [bruijnbindings(term, scale)]; const prev = [blcb(normalizeb(term))]; var looped = false; while (term = reductionsb(images[0].term)[0]) { const u = blcb(normalizeb(term)); images.unshift(bruijnbindings(term, scale)); if (_.find(prev, p => p == u) || prev.length >= N) { looped = true; break; } prev.unshift(u); } const svgs = images.reverse() .map(svgnode => svgnode.outerHTML) .map(svg => `${svg}`); const beta = `→_β`; const stop = `↛`; const loop = `⟲`; return html`

${svgs[1] ? `${svgs.slice(2).map((svg, i) => ``).join('')}` : ``}

${svgs[0]}	${beta}	${svgs[1]}
	${beta}	${svg} ${i == svgs.length - 3 ? (looped ? loop : stop) : ''}
${svgs[0]} ${stop}

`; }33:T47d,bruijnify_stately = { // STATE // Because it's allowed to write `λaa.b`, we cannot use // the amount of the renamed names in the `renamings` hash table // as `numRenamings`. var renamings = {}, numRenamings = 0; function bruijn (t) { if (t.var != undefined) { if (_.has(renamings, t.var)) { return { var: renamings[t.var] }; } const i = (1 + numRenamings) || 1; renamings = _.set(renamings, t.var, i); numRenamings++; return { var: i }; } if (t.const != undefined) { return t; } if (t.abs != undefined) { renamings = _.set(_.mapValues(renamings, i => i + 1), t.abs, 1); numRenamings++; const body = bruijn(t.body); renamings = _.mapValues(renamings, i => i - 1); _.unset(renamings, t.abs); numRenamings--; return { abs: true, body: body }; } if (t.app != undefined) { const app = bruijn(t.app); const arg = bruijn(t.arg); return { app, arg }; } throw 'Error de-bruijning'; } return t => { renamings = {}; numRenamings = 0; return is_bruijn(t) ? t : bruijn(t); }; }34:T416,bruijnify_pure_fn = { function bruijn (t, renamings = []) { if (t.var != undefined) { if (_.has(renamings, t.var)) { return [{ var: renamings[t.var] }, renamings]; } const i = (1 + _.max(Object.values(renamings))) || 1; const renamings2 = _.set(renamings, t.var, i); return [{ var: i }, renamings2]; } if (t.const != undefined) { return [t, renamings]; } if (t.abs != undefined) { const renamings2 = _.set(_.mapValues(renamings, i => i + 1), t.abs, 1); var [body, renamings3] = bruijn(t.body, renamings2); const renamings4 = _.mapValues(renamings3, i => i - 1); _.unset(renamings4, t.abs); return [ { abs: true, body: body }, renamings4, ]; } if (t.app != undefined) { const [app, renamings2] = bruijn(t.app, renamings); const [arg, renamings3] = bruijn(t.arg, renamings2); return [{ app, arg }, renamings3]; } throw 'Error de-bruijning'; } return t => is_bruijn(t) ? t : bruijn(t)[0]; }35:Tddd,function bruijnbindings (debruijnterm, scale = 1) { const segm = segmentify(debruijnterm); segm.tokens.forEach((t, i) => t.i = i); const bindings = segm.tokens.filter(t => t.lambda); const Nchars = segm.tokens.map(t => t[0]).join(' ').length; const fontSize = 18; const style = `font-size: ${fontSize}px; font-family: monospace;`; // ^ Monospace is crucial, it is used for calculations, and the SVG's `textLength` property is used. const padding = 15; const sinkpx = 6; const tokenSpacing = 10; const charWidth = 9; var numLambdas = 0; const colors = d3.schemeSet1; var x = padding; segm.tokens.forEach(t => { const n = (t[0] + '').length; t.xcenter = x + (n*charWidth)/2; x += (n + 1)*charWidth; if (t[0] == 'λ') { t.color = (t.term ? t.term._color : undefined) || '#aaa'; if (t.term) t.term._color = t.color; // - only color at use -- unused lambda will not have a color // - if a color is specified, use it } else if (t[0] == '(' || t[0] == ')') { t.color = '#aaa'; } else if (t.lambda) { if (t.lambda.color == '#aaa') t.lambda.color = colors[numLambdas++ % colors.length]; t.color = t.lambda.color; // bound variable if (t.lambda.term) t.lambda.term._color = t.lambda.color; } else { // unbound variable } if (t.term && t.term.const) { t.style = 'font-weight: bold;'; } }); const estate = segm.tokens.map(__ => 0); bindings.forEach((t, i) => { const sink = 1 + _.max(estate.slice(t.lambda.i, t.i+1)); t.pts = [ [t.xcenter, padding + 14], [t.xcenter, padding + 14 + sinkpx*sink], [t.lambda.xcenter, padding + 14 + sinkpx*sink], [t.lambda.xcenter, padding + 14], ]; for (var i = t.lambda.i; i <= t.i; i++) { estate[i] = Math.max(estate[i] + 1, sink); } }); const width = Nchars*charWidth + 2*padding; const height = 2*padding + 10 + _.max(estate) * sinkpx; const svg = d3.select(DOM.svg(width*scale, height*scale));//.attr('style', 'background: #fafafa;'); const g = svg.append('g').attr('class', 'zoom').attr('style', style).attr('transform', `scale(${scale})`); const line = d3.line(); svg.append("defs").selectAll('marker.arrow').data(colors) .enter() .append("marker") .attr('class', 'arrow') .attr('id', color => `arrow-${color.slice(1)}`) .attr('viewBox', "0 -5 10 10") .attr('refX', 5) .attr('refY', 0) .attr('markerWidth', 4) .attr('markerHeight', 4) .attr('orient', "auto") .append("path") .attr("d", "M0,-5L10,0L0,5") .attr("class", "arrowHead") .attr('fill', color => color); const text = g.append('text') .attr('class', 'term') .attr('fill', '#000') .attr('x', padding) .attr('y', padding + 8) .attr('textLength', Nchars*charWidth); text.selectAll('tspan.token').data(segm.tokens) .enter() .append('tspan') .attr('class', 'token') .attr('fill', t => t.color || '#000') .attr('style', t => t.style || '') .text(t => t[0] + ' '); g.selectAll('path.binding').data(bindings) .enter() .append('path') .attr('class', 'binding') .attr('stroke', t => t.lambda.color) .attr('stroke-width', '1.5') .attr('fill', 'none') .attr('d', t => line(t.pts)) .attr("marker-end", t => `url(#arrow-${t.lambda.color.slice(1)})`); svg.node().term = segm.term; return svg.node(); }36:T5cc,segmentify = { const brace = (s, b) => { if (s.brace || b) { s.tokens.unshift(['(']); s.tokens.push([')']); } return s; }; // state var lambdas = []; // fn function f (t) { if (t.var != undefined) { const token = [t.var]; const lambda = token.lambda = lambdas[t.var - 1]; const term = _.defaults({ token }, t); token.term = term; return { tokens: [token], term, brace: false }; } if (t.const != undefined) { const token = [t.const]; const term = _.defaults({ token }, t); token.term = term; return { tokens: [token], term, brace: false }; } if (t.abs != undefined) { const token = ['λ']; lambdas.unshift(token); const { tokens: bodytokens, term: body } = f(t.body); lambdas.shift(); const term = _.defaults({ token, body }, t); token.term = term; return { tokens: [token].concat(bodytokens), term, brace: true }; } if (t.app != undefined) { const { tokens: apptokens, term: app, brace: appbrace } = brace(f(t.app)); const { tokens: argtokens, term: arg, brace: argbrace } = brace(f(t.arg), t.arg.app); return { tokens: apptokens.concat(argtokens), term: _.defaults({ app, arg }, t), brace: false, }; } throw 'Uncaught case in segmentify: ' + JSON.stringify(t); } const segmentify = t => { lambdas = []; return f(t); }; return segmentify; }37:T62b,parseb = { function pre (str) { var m; var r = []; var apps = r => r.reduce((t, n) => ({ app: t, arg: n })); var abss = (num, body) => (new Array(num)).fill(true).reverse().slice(1).reduce( (t, v) => ({ abs: v, body: t }), { abs: true, body: body } ); while (str.length > 0) { if (m = str.match(/^([SKI])[ ]*/)) { r.push({ const: m[1] }); str = str.slice(m[0].length); } else if (m = str.match(/^([0-9])[ ]*/)) { r.push({ var: parseInt(m[1]) }); str = str.slice(m[0].length); } else if (m = str.match(/^<([0-9]+)>[ ]*/)) { r.push({ var: parseInt(m[1]) }); str = str.slice(m[0].length); } else if (m = str.match(/^$[ ]*/)) { var [r2, str2] = pre(str.slice(m[0].length)); r.push(r2); str = str2; } else if (m = str.match(/^$[ ]*/)) { return [apps(r), str.slice(m[0].length)]; } else if (m = str.match(/^((?:(?:\\|λ)[ ]*)+)\.?[ ]*/)) { var num = m[1].replace(/ /g, '').length; var [r2, str2] = pre(str.slice(m[0].length)); r.push(abss(num, r2)); return [apps(r), str2]; } else { throw `? <${str}>`; } } return [apps(r),str]; } function parseb (str) { var r, rem; try { [r, rem] = pre(str.trim()); } catch (e) { throw 'Parse error: ' + JSON.stringify(e); } if (rem.length > 0) { throw 'Parse error, remaining: ' + rem; } return r; } return parseb; }38:T824,md`

fold { var^{(x:Var) → C}, const^{(c:Const) → C}, abs^{(x:Var) × C → C}, app^{C × C → C} } : Term -> C

Create a function that folds over the structure of a term. You can do this explicitly, of course, by just writing something like the following:

  function f (t) {
    if (t.var != undefined)   return ... t.var ...;
    if (t.const != undefined) return ... t.const ...;
    if (t.abs != undefined)   return ... t.abs ... f(t.body) ...;
    if (t.app != undefined)   return ... f(t.app) ... f(t.arg) ...;
  }

However, with the fold function, we can write:

  const f = fold({
    var: x        => ... x ...,
    const: c      => ... x ...,
    abs: (x, fb)  => ... x ... fb ...,
    app: (ff, fa) => ... ff ... fa ...,
  })

In Haskell, one would typically write:

  f :: Term -> C
  f (Var x)   = ... x ...
  f (Const c) = ... x ...
  f (Abs x b) = ... x ... f b ...
  f (App s t) = ... f s ... f t ...

(*Actually, the constructor mapping functions get the original term as well, which I ommited from the above for clarity and succinctness.*)`39:T522,parse = { function pre (str) { var m; var r = []; var apps = r => r.reduce((t, n) => ({ app: t, arg: n })); var abss = (vars, body) => vars.reverse().slice(1).reduce( (t, v) => ({ abs: v, body: t }), { abs: vars[0], body: body } ); while (str.length > 0) { if (str.match(/^[SKI]/)) { r.push({ const: str[0] }); str = str.slice(1); } else if (m = str.match(/^([a-z]'*)/)) { r.push({ var: m[1] }); str = str.slice(m[0].length); } else if (str[0] == '(') { var [r2, str2] = pre(str.slice(1)); r.push(r2); str = str2; } else if (str[0] == ')') { return [apps(r),str.slice(1)]; } else if (m = str.match(/^(?:\\|λ)((?:[a-z]'*)+)\./)) { var vars = m[1].split(/(?=[a-z])/); var [r2, str2] = pre(str.slice(m[0].length)); r.push(abss(vars, r2)); return [apps(r), str2]; } else { throw '? ' + str; } } return [apps(r),str]; } function parse (str) { var r, rem; try { [r, rem] = pre(str.replace(/ /g, '')); } catch (e) { throw 'Parse error'; } if (rem.length > 0) { throw 'Parse error'; } return r; } return parse; }3a:[] 2f:{"title":"Lambda reductions","cells":[{"id":0,"value":"md`# Lambda reductions`","pinned":false,"hidden":false,"mode":"ojs"},{"id":4277,"value":"redtable(terms.SKK)","pinned":false,"hidden":false,"mode":"ojs"},{"id":4108,"value":"redchart(N, { scale: .6, labels: false, dist: 2, decay: 0.01, strength: -20, N: 50, height: 600, title: `Cloth-like` })","pinned":false,"hidden":false,"mode":"ojs"},{"id":4281,"value":"N = {\n const t = '(λxy.yyy yyyyy yyyyy xxy)';\n const I = '(λx.x)';\n return bruijnify(parse(`(${t}${t}${I})(${t}${t}${I})`));\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":4525,"value":"G = graph(N)","pinned":false,"hidden":false,"mode":"ojs"},{"id":4422,"value":"md`The reduction graph of s(n) is the n-dimensional cube.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":4312,"value":"function s (n) {\n if (n == 0) return parseb('1');\n const S = parseb('(λ 1) 2');\n return new Array(n).fill(S).reduce((a,b) => ({ app: a, arg: b }));\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":4435,"value":"redchart(s(4), { title: 'Four-dimensional hypercube', decay: 0.005, height: 500, labels: false, strength: -400, dist: 20 })","pinned":false,"hidden":false,"mode":"ojs"},{"id":4310,"value":"redchart(s(3), { title: 'Three-dimensional cube' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":4287,"value":"redchart(bruijnify(parse('((λx.x)y)((λx.xxx)(λy.y))((λx.xx)(λy.y))')), { scale: .6, height: 550, title: `\"Poor man's 3D effect\"` })","pinned":false,"hidden":false,"mode":"ojs"},{"id":4460,"value":"md`BTW, many of these examples are due to:\n\nGrathwohl, Niels Bjørn Bugge, Jeroen Ketema, Jens Duelund Pallesen, and Jakob Grue Simonsen (2011) **\"Anagopos: A Reduction Graph Visualizer for Term Rewriting and Lambda Calculus\"** ([pdf](http://www.diku.dk/~bugge/pubs/files/grathwohl2011-0-paper.pdf))`","pinned":false,"hidden":false,"mode":"ojs"},{"id":4039,"value":"//redchart(bruijnify(parse('(\\\\x.xxx)(\\\\x.xxx)')), { dist: 30, strength: -50 })","pinned":false,"hidden":false,"mode":"ojs"},{"id":4284,"value":"redchart(bruijnify(parse('(λx.x)((λy.(λx.x)x)z)')))","pinned":false,"hidden":false,"mode":"ojs"},{"id":3920,"value":"redchart(bruijnify(terms.SKK))","pinned":false,"hidden":false,"mode":"ojs"},{"id":4555,"value":"md`

redchart : DeBruijnTerm × ChartOptions -> HTMLElement

\n\nDisplays the reduction chart of given term with a force-layout.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":3817,"value":"$31","pinned":false,"hidden":false,"mode":"ojs"},{"id":3835,"value":"drag = simulation => {\n \n function dragstarted(d) {\n if (!d3.event.active) simulation.alphaTarget(0.3).restart();\n d.fx = d.x;\n d.fy = d.y;\n }\n \n function dragged(d) {\n d.fx = d3.event.x;\n d.fy = d3.event.y;\n }\n \n function dragended(d) {\n if (!d3.event.active) simulation.alphaTarget(0);\n d.fx = null;\n d.fy = null;\n }\n \n return d3.drag()\n .on(\"start\", dragstarted)\n .on(\"drag\", dragged)\n .on(\"end\", dragended);\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":4547,"value":"md`

graph : DeBruijnTerm -> { nodes^{[ { term^String } ]}, links^{[ { source^String, target^String } ]} }

\n\nCompiles a reduction graph for a given term, up to a given depth *n*. (The *n*-th graph will be *null*.) Note that this graph may be circular, in which case the nodes of the graph will be re-used (i.e. you may check for object identity ===).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":4523,"value":"function graph (term) {\n const MAX = 600;\n var it = 0;\n \n const cache = {};\n const nodes = [];\n const links = [];\n var cut = false;\n \n const todo = [normalizeb(term)];\n \n while (todo.length > 0) {\n if (it++ >= MAX) {\n cut = true;\n break;\n }\n \n var t = todo.pop();\n var d = dispb(t);\n var u = blcb(t);\n if (cache[u]) continue;\n nodes.push(cache[u] = {\n term: d,\n });\n reductionsb(t).map(normalizeb).forEach(t2 => {\n links.push({ source: d, target: dispb(t2) });\n todo.push(t2);\n });\n }\n \n return { nodes, links, cut };\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":3050,"value":"{\n var N = Object.keys(terms).map(k => k.length).reduce((a,b) => Math.max(a,b));\n return md`

reductionsb : DeBruijnTerm -> [ DeBruijnTerm ]

\n\nReturns the list of terms to which the given De Bruijn term *one-step*-reduces.\n\nExamples:\n\n

${Object.entries(terms).map(([name, term]) => `${_.padStart(name, N)} = ${dispb(bruijnify(term))}  →  ${reductionsb(bruijnify(term)).map(dispb).join(',  ')}`).join('\\n')}

`;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":3246,"value":"bruijnify(terms.nocapture)","pinned":false,"hidden":false,"mode":"ojs"},{"id":3233,"value":"{\n Object.entries(terms).forEach(([name, term]) => {\n _.zip(reductions(term), reductionsb(bruijnify(term))).forEach(([a, b]) => {\n const na = normalizeb(bruijnify(a));\n const nb = normalizeb(b);\n if (dispb(na) != dispb(nb)) {\n throw `${name} = ${disp(a)} : ${dispb(na)} != ${dispb(nb)}`;\n }\n });\n });\n \n return md`Testing whether \\`reductions\\` and \\`reductionsb\\` coincide over \\`bruijnify\\` (and \\`normalizeb\\`) ... **PASSED**`;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":3145,"value":"skk = bruijnify(terms.SKK)","pinned":false,"hidden":false,"mode":"ojs"},{"id":3508,"value":"$32","pinned":false,"hidden":false,"mode":"ojs"},{"id":3698,"value":"redtable(bruijnify(terms.I))","pinned":false,"hidden":false,"mode":"ojs"},{"id":3577,"value":"redtable(terms.SKK)","pinned":false,"hidden":false,"mode":"ojs"},{"id":3579,"value":"redtable(terms.Ω)","pinned":false,"hidden":false,"mode":"ojs"},{"id":3649,"value":"redtable(parse(`(λx.xxx)((λxy.x)(λx.xxx))`))","pinned":false,"hidden":false,"mode":"ojs"},{"id":3660,"value":"redtable(parse('(λx.x)(λx.x)(λx.xx)(λx.xx)'))","pinned":false,"hidden":false,"mode":"ojs"},{"id":3761,"value":"redtable(parse('(λx.xxx)(λx.xxx)'), 5)","pinned":false,"hidden":false,"mode":"ojs"},{"id":3048,"value":"function reductionsb (t) {\n if (t.var) return [];\n if (t.const) return [];\n if (t.abs) {\n return reductionsb(t.body).map(r => _.defaults({ body: r }, t));\n }\n if (t.app) {\n var rs = [];\n if (t.app.abs) {\n rs.push(lift(substb(t.app.body, lift(t.arg, 1)), -1));\n }\n rs = rs.concat(reductionsb(t.app).map(r => _.defaults({ app: r }, t)));\n rs = rs.concat(reductionsb(t.arg).map(r => _.defaults({ arg: r }, t)));\n return rs;\n }\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":1200,"value":"{\n var N = Object.keys(terms).map(k => k.length).reduce((a,b) => Math.max(a,b));\n return md`

reductions : Term -> [ Term ]

\n\nReturns the list of terms to which the given term *one-step*-reduces.\n\nExamples:\n\n

${Object.entries(terms).map(([name, term]) => `${_.padStart(name, N)} = ${disp(term)}  →  ${reductions(term).map(disp).join(',  ')}`).join('\\n')}

`;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":418,"value":"reductions = fold({\n var: () => [],\n const: () => [],\n abs: (v, brs) => brs.map(r => ({ abs: v, body: r })),\n app: (lrs, rrs, t) => {\n var rs = [];\n if (t.app.abs) {\n rs.push(subst(t.app.body, t.app.abs, t.arg));\n }\n rs = rs.concat(lrs.map(r => ({ app: r, arg: t.arg })));\n rs = rs.concat(rrs.map(r => ({ app: t.app, arg: r })));\n return rs;\n },\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":1122,"value":"md`

equal : Term × Term -> Bool

\n\nChecks whether two terms are equal (up to renaming). Essentially, the way this is computed, is by collecting the list of free variables in both terms, and checking that they are of the same size, and are used in the same places.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":753,"value":"equal = {\n const pre = fold2({\n var: (x, y) => [[x], [y]],\n const: (c, d) => [[], []],\n abs: (x, y, body_fvs) => {\n if (!body_fvs) return false;\n for (var i = 0; i < body_fvs[0].length; i++) {\n if (x == body_fvs[0][i] && body_fvs[1][i] != y) return false;\n if (y == body_fvs[1][i] && body_fvs[0][i] != x) return false;\n }\n const fvs = [_.pull(body_fvs[0], x), _.pull(body_fvs[1], y)];\n if (fvs[0].length != fvs[1].length) return false;\n return fvs;\n },\n app: (le_fvs, ri_fvs) => {\n if (!le_fvs || !ri_fvs) return false;\n const fvs = [_.union(le_fvs[0], ri_fvs[0]), _.union(le_fvs[1], ri_fvs[1])];\n if (fvs[0].length != fvs[1].length) return false;\n return fvs;\n },\n neq: () => false,\n });\n \n return (N, M) => !!pre(N, M);\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":3064,"value":"md`

substb : DeBruijnTerm × DeBruijnTerm → DeBruijnTerm

\n\nSubstitutes M for 1 in N.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":3061,"value":"// N[1:=M] = substb(N, M)\nsubstb = {\n var depth = 0;\n \n function substb (N, M) {\n if (N.var) return N.var == depth + 1 ? lift(M, depth) : N;\n if (N.const) return N;\n if (N.abs) {\n depth++;\n const abs = _.defaults({ body: substb(N.body, M) }, N);\n depth--;\n return abs;\n }\n if (N.app) return _.defaults({ app: substb(N.app, M), arg: substb(N.arg, M) }, N);\n }\n \n return (N, M) => {\n depth = 0;\n return substb(N, M);\n };\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":1130,"value":"md`

subst : Term × Var × Term → Term\nsubst(N, x, M) = N[x := M]

\n\nSubstitutes M for x in N, making sure that no names are captured.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":276,"value":"// N[x:=M] = subst(N, x, M)\nfunction subst (N, x, M) {\n if (N.var) return (N.var == x) ? M : N;\n if (N.const) return N;\n if (N.abs) {\n if (N.abs == x) return N;\n const used = _.union(fvs(N), fvs(M));\n // add <'>'s, or else just use a new name\n const options = [1,2,3,4].map(n => _.padEnd(N.abs, n, `'`)).concat('abcdefghijklmnopqrstuvwxyz'.split(''));\n const y = _.find(options, y => used.indexOf(y) < 0);\n return { abs: y, body: subst(rename(N.abs, y)(N.body), x, M) };\n }\n if (N.app) return { app: subst(N.app, x, M), arg: subst(N.arg, x, M) };\n throw 'Subst rrr';\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":356,"value":"rename = (from, to) => fold({\n var: v => ({ var: (v == from) ? to : v }),\n const: (c, t) => t,\n abs: (v, rb, orig) => (v == from) ? orig : ({ abs: v, body: rb }),\n app: (rl, rr) => ({ app: rl, arg: rr }),\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":1089,"value":"{\n const data = Object.entries(terms).map(([name, term]) => [\n name,\n disp(term),\n fvs(term).length ? ('free: ') + fvs(term).join(',') : '',\n ]);\n const widths = data[0].map((x,i) => data.map(row => row[i].length).reduce((a,b) => Math.max(a,b)));\n \n return md`fvs : Term -> Set(Var)\n\nCollects the free (i.e. unbound by an abstraction) variables of a term.\n\nExamples:\n\n

${data.map(([name, t, fvs]) => [\n    `${_.padStart(name, widths[0])}`,\n    '=',\n    _.padEnd(t, widths[1] + 1),\n    fvs,\n  ].join(' ')).join('\\n')}

`;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":548,"value":"fvs = fold({\n var: v => [v],\n const: c => [],\n abs: (v, fvs_b) => _.without(fvs_b, v),\n app: _.union,\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":1441,"value":"md`lift : DeBruijnTerm × ℕ → DeBruijnTerm`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1432,"value":"function lift (t, n, depth = 0) {\n if (t.var) return _.defaults({ var: typeof t.var != 'number' ? t.var : (t.var <= depth ? t.var : (t.var + n)) }, t);\n if (t.const) return t;\n if (t.abs) return _.defaults({ abs: true, body: lift(t.body, n, depth + 1) }, t);\n if (t.app) return _.defaults({ app: lift(t.app, n, depth), arg: lift(t.arg, n, depth) }, t);\n throw 'Error lifting!';\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":1768,"value":"md`bruijnify : Term -> DeBruijnTerm\n\nAn implementation is chosen.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1692,"value":"bruijnify = bruijnify_stately","pinned":false,"hidden":false,"mode":"ojs"},{"id":1760,"value":"md`bruijnify_stately : Term -> DeBruijnTerm\n\nConvert a named term to a De Bruijn term, where cleaner, though possibly more obscure code is achieved through treating the renamings involved as an ambient state, while traversing through the term. Now, of course, the computing strategy has an effect on the renaming. (Javascript is a call-by-value language, but one could conceive the code in an equivalent, but call-by-name, language, in which case the results would be slightly different—though not erroneously so.)`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1664,"value":"$33","pinned":false,"hidden":false,"mode":"ojs"},{"id":1751,"value":"md`bruijnify_pure_fn : Term -> DeBruijnTerm\n\nConvert a named term to a De Bruijn term, passing along the renamings involved in a purely functional manner.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1363,"value":"$34","pinned":false,"hidden":false,"mode":"ojs"},{"id":2612,"value":"is_bruijn = fold({\n var: x => typeof x == 'number',\n const: c => true,\n abs: (x, b) => (x === true && b),\n app: (x, y) => (x && y),\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":2173,"value":"md`

bruijnbindings : DeBruijnTerm → SVGElement

\n\nMakes a pretty picture showing the variable bindings of a De Bruijn term.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2529,"value":"{\n return html`

\n ${Object.entries(terms).map(([name, term]) => `\n

\n ${name} =\n ${bruijnbindings(bruijnify(term), .8).outerHTML}\n

\n `).join('\\n')}\n

`;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":4265,"value":"md`These ones are zoomable:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":4212,"value":"{\n const svg = d3.select(bruijnbindings(N, 1));\n const g = svg.select('g.zoom');\n svg.call(d3.zoom().on('zoom', e => {\n g.attr(\"transform\", d3.event.transform);\n }));\n svg.attr('height', 300);\n return svg.node();\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":4271,"value":"{\n const svg = d3.select(bruijnbindings(bruijnify(terms.SKK)));\n const g = svg.select('g.zoom');\n svg.call(d3.zoom().on('zoom', e => {\n g.attr(\"transform\", d3.event.transform);\n }));\n svg.attr('width', width);\n svg.attr('height', 300);\n return svg.node();\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":1830,"value":"$35","pinned":false,"hidden":false,"mode":"ojs"},{"id":2962,"value":"testt = bruijnify(terms.S)// parseb('λ 9 2 3 ( λ 1 ( λ 1 5 ) ) ( λ 2 1 ) 2 (7 4)')","pinned":false,"hidden":false,"mode":"ojs"},{"id":2842,"value":"bruijnbindings(testt)","pinned":false,"hidden":false,"mode":"ojs"},{"id":2916,"value":"bruijnbindings(normalizeb(testt))","pinned":false,"hidden":false,"mode":"ojs"},{"id":2987,"value":"[terms.I, terms.K, terms.S, terms.SKK].map(bruijnify).map(normalizeb).map(blcb)","pinned":false,"hidden":false,"mode":"ojs"},{"id":3040,"value":"md`blcb : DeBruijnTerm -> BLCString\n\nConverts the term to binary lambda calculus.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2984,"value":"function blcb (t) {\n if (t.var) return new Array(t.var).fill('1').join('') + '0';\n if (t.const) return `[t.const]`;\n if (t.abs) return '00' + blcb(t.body);\n if (t.app) return '01' + blcb(t.app) + blcb(t.arg);\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":3036,"value":"md`normalizeb : DeBruijnTerm -> DeBruijnTerm\n\nEnforces an order on the free variables, thereby normalizing the term.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2922,"value":"normalizeb = {\n var depth = 0, renamings = {}, numRenamed = 0;\n \n function normalizeb (t) {\n if (t.var) {\n if (t.var > depth) { // free variable no. `t.var - depth`\n if (renamings[t.var - depth]) {\n return { var: depth + renamings[t.var - depth] };\n }\n const n = depth + numRenamed + 1;\n renamings[t.var - depth] = n;\n numRenamed++;\n return { var: n };\n }\n return t;\n }\n if (t.const) return t;\n if (t.abs) {\n depth++;\n const abs = { abs: true, body: normalizeb(t.body) };\n depth--;\n return abs;\n }\n if (t.app) {\n return { app: normalizeb(t.app), arg: normalizeb(t.arg) };\n }\n }\n \n return t => {\n depth = 0;\n renamings = {};\n numRenamed = 0;\n const n = normalizeb(t);\n n._i = { depth, renamings, numRenamed };\n return n;\n };\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":2885,"value":"md`dispb : DeBruijnTerm -> String\n\nWe'll be working with De-Bruijn-indexed terms as well. Recall that a term with De Bruijn indices are bound as in the picture below.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1844,"value":"dispb = {\n const brace = (str, b) => b ? `(${str})` : str;\n \n return function dispb (t) {\n if (t.var) return t.var;\n if (t.const) return t.const;\n if (t.abs) return `λ ${dispb(t.body)}`;\n if (t.app) return `${brace(dispb(t.app), t.app.abs)} ${brace(dispb(t.arg), t.arg.app || t.arg.abs)}`;\n }\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":1913,"value":"md`

segmentify : DeBruijnTerm → { tokens^{[ Token ]}, term^{DeBruijnTerm ∪ { token^Token }} }\n  where Token = [ String ] ∪ { lambda^Token, term^Term }

\n\nIn order to draw beautiful pictures showing which lambdas bind which variables, we'll need to keep track of how the displayed term corresponds to the term data. To this end, this function returns the displayed term as (essentially) a list of tokens, and an annotated copy of the term in which each variable, constant and lambda references the corresponding token, and furthermore variables (and variable tokens) reference the abstracting lambda token as well. Each token is just a one-element array, but because it's packaged as an array, it's easy to reference without intermediately knowing it's position in the final token list.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1400,"value":"$36","pinned":false,"hidden":false,"mode":"ojs"},{"id":2024,"value":"{\n const term = parse(`λx.(λy.y(λz.z))(λy.xy)`);\n const segm = segmentify(bruijnify(term));\n const d = md`As an example, the term ${disp(term)} = ${dispb(bruijnify(term))} produces:\n\n| Token indices: | ${segm.tokens.map((t,i) => i).join(' | ')} |\n| --- |\n| Tokens: | ${segm.tokens.join(' | ')} |\n| Abstractions: | ${segm.tokens.map((t,i) => t.lambda ? segm.tokens.indexOf(t.lambda) : '').join(' | ')} |`;\n /*\n const md = segmentify.md = ({ tokens }) => {\n return tokens.map(token => {\n const i = tokens.indexOf(token.lambda);\n return `${token[0]}${token.lambda ? `^${i}` : ''}`;\n });\n };*/\n \n return d;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":2406,"value":"md`

parseb : String -> Term

\n\nWe will also concern ourselves with De Bruijn indexed terms, for which the syntax is:\n

   Var ::= [0-9]+\n  Term ::= Var\n         | [λ\\\\]+ .? Term\n         | Term Term\n         | ( Term )

\n\nSpaces are meaningless except for denoting the boundary between variables, and are ignored.\n\nThrows an exception if not well-formed.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2446,"value":"dispb(parseb('5(λλλ. (21 21<21>2) (5 8))'))","pinned":false,"hidden":false,"mode":"ojs"},{"id":2444,"value":"$37","pinned":false,"hidden":false,"mode":"ojs"},{"id":1081,"value":"_.every(_.zip(Object.values(terms), Object.values(terms).map(disp).map(parse)).map(([s,t]) => equal(s,t)))","pinned":false,"hidden":false,"mode":"ojs"},{"id":2408,"value":"{\n const data = Object.entries(terms).map(([name, term]) => [\n name,\n disp(term),\n ]);\n const widths = data[0].map((x,i) => data.map(row => row[i].length).reduce((a,b) => Math.max(a,b)));\n \n return md`fvs : Term -> Set(Var)\n\nCollects the free (i.e. unbound by an abstraction) variables of a term.\n\nExamples:\n\n

${data.map(([name, t]) => [\n    `  ${_.padEnd(`disp(terms.${name})`, widths[0]+29)}`,\n    '==',\n    '\"' + t + '\"',\n  ].join(' ')).join('\\n')}

`;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":2891,"value":"md`disp : Term -> String`","pinned":false,"hidden":false,"mode":"ojs"},{"id":144,"value":"disp = {\n const brace = (str, b) => b ? `(${str})` : str;\n \n function disp (t) {\n if (t.var) return t.var;\n if (t.const) return t.const;\n if (t.abs) return `λ${t.abs}.${disp(t.body)}`;\n if (t.app) return `${brace(disp(t.app), t.app.abs)}${brace(disp(t.arg), t.arg.app || t.arg.abs)}`;\n }\n \n return t => disp(t).replace(/(λ(?:[a-z]'*)\\.){2,}/g, str => (str+'').replace(/\\.λ/g, ''));\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":957,"value":"md`Perform a fold on structurally equal terms.\n\n

fold2 { var^{(x,y):Var² → C}, const^{(c,d):Const² → C}, abs^{(x,y):Var² × C → C}, app^{C × C → C}, neq^C } : Term² -> C

\n\n(*Similar to fold, the mapping functions get the original terms as arguments, as well.*)`","pinned":false,"hidden":false,"mode":"ojs"},{"id":953,"value":"function fold2 (f) {\n return function go (s, t) {\n if (s.var != undefined && t.var != undefined) return f.var(s.var, t.var, s, t);\n if (s.const != undefined && t.const != undefined) return f.const(s.const, t.const, s, t);\n if (s.abs != undefined && t.abs != undefined) return f.abs(s.abs, t.abs, go(s.body, t.body), s, t);\n if (s.app != undefined && t.app != undefined) return f.app(go(s.app, t.app), go(s.arg, t.arg), s, t);\n return f.neq(s, t);\n };\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":926,"value":"$38","pinned":false,"hidden":false,"mode":"ojs"},{"id":364,"value":"function fold (f) {\n return function go (t) {\n if (t.var != undefined) return f.var(t.var, t);\n if (t.const != undefined) return f.const(t.const, t);\n if (t.abs != undefined) return f.abs(t.abs, go(t.body), t);\n if (t.app != undefined) return f.app(go(t.app), go(t.arg), t);\n throw 'Error folding ' + JSON.stringify(t);\n };\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":2663,"value":"function cases (f) {\n return function (t) {\n if (t.var != undefined) return f.var(t.var, t);\n if (t.const != undefined) return f.const(t.const, t);\n if (t.abs != undefined) return f.abs(t.abs, t.body, t);\n if (t.app != undefined) return f.app(t.app, t.arg, t);\n throw 'Error case-matching ' + JSON.stringify(t);\n };\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":443,"value":"app = (l, r) => ({ app: l, arg: r })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1220,"value":"terms = {\n const terms = {\n nocapture: parse(`(\\\\xy.x) y`),\n nocapture2: parse(`(λxyy'.x)yy'`),\n red: parse('(\\\\x.xa)y'),\n I: parse(`\\\\x'.x'`),\n K: parse(`\\\\xy'.x`),\n S: parse('\\\\x y z. xz(yz)'),\n Sa: parse('(\\\\xyz.xz(yz))a'),\n ω: parse('(λx.xx)'),\n Ω: parse('(λx.xx)(λx.xx)'),\n Ω3: parse('(λx.xxx)(λx.xxx)'),\n fvs: parse('(λc.(λx.axbc))c'),\n '2rs': parse('(λx.(λy.y)x)z'),\n consts: parse('SKI'),\n n6: parse(`λx.(λy.y(λz.z))(λy.xy)abc`),\n doubledigits: parse('λj.abcdefghijklmn'),\n };\n \n terms['3rs'] = parse('(\\\\x.(\\\\y.y)x)((\\\\a.a)b)');\n terms.SKK = app(app(terms.S, terms.K), terms.K);\n \n return terms;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":1002,"value":"md`

parse : String -> Term

\n\nTerm strings must have the form:\n

   Var ::= [a-z]\n         | Var'\n  Term ::= Var\n         | [λ\\\\] Var+ . Term\n         | Term Term\n         | ( Term )

\n\nSpaces are ignored.\n\nThrows an exception if not well-formed.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":999,"value":"$39","pinned":false,"hidden":false,"mode":"ojs"},{"id":922,"value":"md`## Libraries`","pinned":false,"hidden":false,"mode":"ojs"},{"id":4,"value":"import { text, slider } from '@jashkenas/inputs'","pinned":false,"hidden":false,"mode":"ojs"},{"id":484,"value":"_ = require('lodash')","pinned":false,"hidden":false,"mode":"ojs"},{"id":3941,"value":"d3 = require('https://d3js.org/d3.v5.min.js')","pinned":false,"hidden":false,"mode":"ojs"}],"files":"$W3a","stdlib":"1","titling":"auto"}