Skip to content

Instantly share code, notes, and snippets.

@Explosion-Scratch

Explosion-Scratch/.pen.config.json

Created February 21, 2026 19:55
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save Explosion-Scratch/a0faf0d2ba5758b9808bf7d4df9cf040 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save Explosion-Scratch/a0faf0d2ba5758b9808bf7d4df9cf040 to your computer and use it in GitHub Desktop.
Download ZIP
Test Proj
Raw
.pen.config.json
{
"name": "Test Proj",
"version": "1.0.0",
"editors": [
{
"type": "html",
"filename": "index.html",
"settings": {
"doctype": "html5",
"lang": "en"
}
},
{
"type": "css",
"filename": "style.css",
"settings": {
"normalize": false,
"autoprefixer": false,
"tailwind": true
}
},
{
"type": "javascript",
"filename": "script.js",
"settings": {
"moduleType": "module",
"strictMode": true
}
}
],
"globalResources": {
"scripts": [],
"styles": []
},
"autoRun": true,
"previewUrl": "",
"layoutMode": "columns"
}
Raw
index.html
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<title>The Interactive Lambda Calculus</title>
<style>
/* Notion-like Warm Theme */
:root {
--bg-color: #fdfcf8;
--text-color: #37352f;
--text-light: #787774;
--accent-red: #eb5757;
--accent-blue: #2d9cdb;
--accent-green: #0f7b6c;
--accent-purple: #9065b0;
--accent-bg-hover: #efede7;
--code-bg: #f7f6f3;
--border-color: #e1dfdd;
--font-serif: "Merriweather", "Georgia", "Cambria", "Times New Roman", Times, serif;
--font-sans: -apple-system, BlinkMacSystemFont, "Segoe UI", Helvetica, "Apple Color Emoji", Arial, sans-serif, "Segoe UI Emoji", "Segoe UI Symbol";
--font-mono: "SFMono-Regular", Consolas, "Liberation Mono", Menlo, Courier, monospace;
}
* {
box-sizing: border-box;
margin: 0;
padding: 0;
}
body {
background-color: var(--bg-color);
color: var(--text-color);
font-family: var(--font-serif);
line-height: 1.7;
font-size: 18px;
-webkit-font-smoothing: antialiased;
}
.container {
max-width: 800px;
margin: 0 auto;
padding: 80px 20px;
}
h1, h2, h3, h4 {
font-family: var(--font-sans);
font-weight: 700;
color: #2f2f2f;
margin-top: 2em;
margin-bottom: 0.5em;
}
h1 { font-size: 3em; line-height: 1.2; margin-top: 0; margin-bottom: 0.2em; }
h2 { font-size: 1.8em; border-bottom: 1px solid var(--border-color); padding-bottom: 0.3em; }
h3 { font-size: 1.4em; }
p { margin-bottom: 1.5em; }
.subtitle {
font-family: var(--font-sans);
color: var(--text-light);
font-size: 1.2em;
margin-bottom: 3em;
}
code, .math {
font-family: var(--font-mono);
background: var(--code-bg);
padding: 0.2em 0.4em;
border-radius: 3px;
font-size: 0.9em;
color: var(--accent-red);
}
.math-block {
font-family: var(--font-mono);
font-size: 1.3em;
text-align: center;
padding: 1em;
background: white;
border: 1px solid var(--border-color);
border-radius: 8px;
margin: 2em 0;
box-shadow: 0 2px 4px rgba(0,0,0,0.02);
overflow-x: auto;
}
/* Interactive Elements styling */
.interactive-widget {
background: white;
border: 1px solid var(--border-color);
border-radius: 8px;
padding: 30px;
margin: 2em 0;
box-shadow: 0 4px 12px rgba(0,0,0,0.03);
font-family: var(--font-sans);
}
.widget-header {
font-size: 0.9em;
text-transform: uppercase;
letter-spacing: 0.05em;
color: var(--text-light);
margin-bottom: 15px;
font-weight: 600;
}
button {
font-family: var(--font-sans);
background: white;
border: 1px solid var(--border-color);
padding: 8px 16px;
border-radius: 4px;
cursor: pointer;
font-size: 0.95em;
transition: all 0.2s ease;
box-shadow: 0 1px 2px rgba(0,0,0,0.05);
}
button:hover {
background: var(--accent-bg-hover);
}
button:disabled {
opacity: 0.5;
cursor: not-allowed;
}
/* Hover syntax highlighting */
.term {
display: inline-block;
transition: background 0.2s;
padding: 2px;
border-radius: 4px;
cursor: default;
}
.term.abs { color: var(--accent-purple); font-weight: bold; }
.term.var { color: var(--accent-blue); }
.term.app { border-bottom: 2px dashed transparent; }
/* Specific Hover Interactions */
.hover-group[data-hl="x"]:hover .h-x { background: rgba(45, 156, 219, 0.2); }
.hover-group[data-hl="y"]:hover .h-y { background: rgba(15, 123, 108, 0.2); }
.hover-group[data-hl="f"]:hover .h-f { background: rgba(235, 87, 87, 0.2); }
/* Visualizing diagrams */
.diagram-container {
display: flex;
align-items: flex-end;
justify-content: center;
gap: 10px;
padding: 40px 20px;
background: #23242f; /* Dark background from video */
border-radius: 8px;
margin: 2em 0;
font-family: monospace;
overflow: hidden;
}
.v-bar {
width: 8px;
background: white;
position: relative;
transition: all 0.3s;
}
.h-bar {
height: 8px;
background: white;
position: absolute;
top: 0;
left: 0;
transition: all 0.3s;
}
.branch {
border-bottom: 8px solid white;
border-left: 8px solid white;
border-right: 8px solid white;
border-radius: 0 0 8px 8px;
display: flex;
justify-content: space-between;
}
.color-f { color: var(--accent-red); fill: var(--accent-red); stroke: var(--accent-red); background: var(--accent-red) !important;}
.color-x { color: var(--accent-blue); fill: var(--accent-blue); stroke: var(--accent-blue); background: var(--accent-blue) !important;}
.controls { display: flex; gap: 10px; margin-top: 15px; }
.step-description { font-size: 0.95em; color: var(--text-light); margin-top: 15px; min-height: 48px;}
/* Sliders */
input[type=range] {
width: 100%;
margin: 15px 0;
}
.visual-church {
display: flex;
align-items: center;
justify-content: center;
font-size: 2em;
letter-spacing: 0.1em;
min-height: 80px;
}
</style>
</head>
<body>
<div class="container">
<header>
<h1>The Way of the Lambda</h1>
<p class="subtitle">An Interactive Explorer of Pure Computation</p>
</header>
<article>
<p>In the early 1900s, David Hilbert asked a profound question: <em>Is there a universal algorithm that can determine if any mathematical statement is true or false?</em></p>
<p>Before computers even existed, mathematicians needed a formal definition of "computation" to answer this. While Alan Turing invented his famous theoretical tape machine, Alonzo Church took a completely different approach. He didn't build a machine; he built a language.</p>
<p>He called it the <strong>λ-Calculus</strong>. It consists of no numbers, no logic gates, and no plus signs. It is pure symbolic manipulation. Yet, as we will explore, it is capable of computing anything in the universe.</p>
<h2>1. The Three Sacred Rules</h2>
<p>In standard algebra, an expression like <code>y = x² + 5x + 3</code> deals with numbers. In the lambda calculus, we only have three fundamental components to build our strings of symbols:</p>
<ol>
<li><strong>Variables:</strong> Represented by letters (<code>a, b, x, y</code>).</li>
<li><strong>Abstractions (Functions):</strong> A way to define a function. Written as <code>(λx. M)</code>, meaning "a function that takes an input <code>x</code> and returns the expression <code>M</code>".</li>
<li><strong>Applications:</strong> A way to apply a function to an argument. Written as <code>(M N)</code>, meaning "apply function <code>M</code> to argument <code>N</code>".</li>
</ol>
<div class="interactive-widget">
<div class="widget-header">Interactive Syntax Explorer</div>
<p style="font-size: 0.9em; margin-bottom: 20px;">Hover over the components below to see how they bind together. Notice how the <code>λ</code> defines a scope for its variable.</p>
<div class="math-block" style="background: var(--bg-color); border:none; box-shadow:none; padding:0;">
<span class="hover-group" data-hl="x" style="cursor:help;">
(<span class="term abs h-x">λx.</span>
<span class="term app">
<span class="hover-group" data-hl="y" style="display:inline-block">
(<span class="term abs h-y">λy.</span>
<span class="term var h-x">x</span>
<span class="term var h-y">y</span>)
</span>
<span class="term var h-x">x</span>
</span>)
</span>
</div>
<p class="step-description" style="text-align: center;">Hover over an abstraction (λ) to see which variables belong to it.</p>
</div>
<h2>2. Visualizing Computation (Tromp Diagrams)</h2>
<p>Reading deep nests of parentheses is difficult. John Tromp devised a way to visualize these expressions as topological graphs. In his diagrams, variables drop down as vertical lines. Abstractions are horizontal bars catching those lines. Applications are forks branching out.</p>
<div class="interactive-widget" style="background: #1e1e24; color: white; border-color:#333;">
<div class="widget-header" style="color: #888;">Abstract Topologies</div>
<p style="font-size: 0.9em; color:#ccc;">Select a term to see its structural diagram.</p>
<div class="controls">
<button onclick="drawDiagram('identity')" style="background:#333; color:white; border-color:#555;">Identity (λx.x)</button>
<button onclick="drawDiagram('apply')" style="background:#333; color:white; border-color:#555;">Apply (λf.λx.fx)</button>
<button onclick="drawDiagram('omega')" style="background:#333; color:white; border-color:#555;">Omega (λx.xx)</button>
</div>
<div class="diagram-container" id="diagram-mount">
<!-- SVG rendered here via JS -->
</div>
<p id="diagram-desc" style="text-align: center; color: #aaa; font-family:var(--font-sans); font-size: 0.9em;">Click a button above.</p>
</div>
<h2>3. The Engine of Computation: Beta Reduction</h2>
<p>If variables and abstractions are the engine, <strong>Beta Reduction</strong> (β-reduction) is the combustion. It is the only rule for "evaluating" an expression.</p>
<p>When you have an application <code>(λx. Body) Value</code>, you substitute all unbound instances of <code>x</code> inside the <code>Body</code> with the <code>Value</code>. Then, you discard the <code>λx.</code> wrapper.</p>
<div class="interactive-widget">
<div class="widget-header">Beta Reduction Stepper</div>
<p style="font-size: 0.9em;">Let's evaluate a function that applies a given function twice: <code>(λf.λx. f (f x))</code>, applied to an argument <code>INC</code> and value <code>0</code>.</p>
<div class="math-block" id="beta-math-display" style="min-height: 80px; display:flex; align-items:center; justify-content:center;">
<!-- Content inserted by JS -->
</div>
<div class="controls" style="justify-content: center;">
<button id="btn-beta-prev" disabled>Previous Step</button>
<button id="btn-beta-next">Next Step</button>
<button id="btn-beta-reset" style="margin-left: 20px;">Reset</button>
</div>
<p id="beta-desc" class="step-description" style="text-align: center;">Ready to evaluate.</p>
</div>
<h2>4. Inventing Logic from Nothing</h2>
<p>We haven't defined what True or False are. The beauty of λ-calculus is that we don't have to embed them in the hardware; we can define them purely through behavior. What does a boolean <em>do</em>? It chooses between two paths.</p>
<p>Let's define them as selectors. A boolean function takes two arguments. <code>TRUE</code> returns the first argument. <code>FALSE</code> returns the second argument.</p>
<div class="math-block">
TRUE = (λa.λb. a)<br>
FALSE = (λa.λb. b)
</div>
<p>With these definitions, an <code>IF_THEN_ELSE</code> statement is trivial. The boolean itself is the <code>IF</code>. You simply apply the boolean to the <code>THEN</code> and <code>ELSE</code> clauses:</p>
<div class="math-block">
(Condition ThenClause ElseClause)
</div>
<div class="interactive-widget">
<div class="widget-header">Boolean Logic Simulator</div>
<p style="font-size: 0.9em;">Let's create the <code>NOT</code> operator. <code>NOT</code> takes a boolean <code>x</code>. If <code>x</code> is TRUE, it should return FALSE. If <code>x</code> is FALSE, it should return TRUE. So, <code>NOT = (λx. x FALSE TRUE)</code>.</p>
<div style="display:flex; justify-content:center; gap: 20px; margin: 20px 0;">
<button onclick="evalNot('TRUE')">Evaluate: NOT TRUE</button>
<button onclick="evalNot('FALSE')">Evaluate: NOT FALSE</button>
</div>
<div class="math-block" id="not-display" style="font-size: 1.1em; padding: 20px;">
<em>Click a button to trace the evaluation.</em>
</div>
</div>
<h2>5. Church Numerals: Counting without Numbers</h2>
<p>If we can conjure logic from functions, can we conjure arithmetic? Alonzo Church represented numbers as the concept of repetition. The number <em>N</em> is represented by a function that takes another function <code>f</code> and an argument <code>x</code>, and applies <code>f</code> to <code>x</code> exactly <em>N</em> times.</p>
<div class="math-block" style="text-align: left; font-size: 1.1em; padding-left: 20%;">
0 = (λf.λx. x)<br>
1 = (λf.λx. f x)<br>
2 = (λf.λx. f (f x))<br>
3 = (λf.λx. f (f (f x)))
</div>
<div class="interactive-widget">
<div class="widget-header">Church Numeral Generator</div>
<p style="font-size: 0.9em;">Slide to generate Church Numerals. Notice how "Zero" is identical to our definition of "FALSE"!</p>
<input type="range" id="church-slider" min="0" max="6" value="2">
<div style="text-align: center; font-weight: bold; margin-bottom: 10px;">N = <span id="church-n-val">2</span></div>
<div class="math-block visual-church" id="church-display">
λf.λx. f(f(x))
</div>
</div>
<p>From here, you can build addition (by applying <code>f</code> $N$ times, then $M$ times). You can build multiplication (applying $N \times M$ times). You can even build exponentiation simply by applying one number to another: <code>(N M)</code>.</p>
<h2>6. The Abyss: Recursion and the Y-Combinator</h2>
<p>If we want to build a loop, or a function like Factorial, we run into a problem. Factorial requires multiplying <code>N * Factorial(N-1)</code>. But in pure λ-calculus, functions are anonymous. They have no names. How can a function call itself if it doesn't know its own name?</p>
<p>The solution is one of the most mind-bending concepts in computer science: the <strong>Fixed-Point Combinator</strong>, famously known as the Y-Combinator (or Turing's $\Theta$).</p>
<div class="math-block">
Y = (λf. (λx. f (x x)) (λx. f (x x)))
</div>
<p>By passing a function into the Y-Combinator, it structurally replicates that function infinitely deep, evaluating it only as needed. It achieves recursion without self-reference. It creates an infinite tape out of thin air, proving that this simple set of three rules is exactly as powerful as any supercomputer in existence.</p>
<hr style="margin: 4em 0; border: none; border-top: 1px solid var(--border-color);">
<p style="text-align: center; color: var(--text-light); font-size: 0.9em;">
Inspired by the visual explanations of John Tromp and the history of theoretical computer science.
</p>
</article>
</div>
<script>
// --- Widget 2: Diagram Renderer ---
const diagramMount = document.getElementById('diagram-mount');
const diagramDesc = document.getElementById('diagram-desc');
const diagrams = {
'identity': {
desc: "λx.x : A single abstraction catching a single variable.",
svg: `
<svg width="60" height="100" viewBox="0 0 60 100">
<!-- Abstraction bar -->
<rect x="10" y="20" width="40" height="8" fill="white" />
<!-- Variable line -->
<rect x="26" y="20" width="8" height="60" fill="white" />
</svg>`
},
'apply': {
desc: "λf.λx.(f x) : Two abstractions, and an application bridging the two variables.",
svg: `
<svg width="120" height="140" viewBox="0 0 120 140">
<!-- Abstraction f -->
<rect x="20" y="20" width="80" height="8" fill="white" />
<!-- Abstraction x -->
<rect x="60" y="40" width="40" height="8" fill="white" />
<!-- Variable lines -->
<rect x="36" y="20" width="8" height="60" fill="white" class="color-f" />
<rect x="76" y="40" width="8" height="40" fill="white" class="color-x" />
<!-- Application branch -->
<path d="M 36 80 L 36 100 L 76 100 L 76 80" fill="none" stroke="white" stroke-width="8" stroke-linejoin="miter"/>
<rect x="56" y="100" width="8" height="20" fill="white" />
</svg>`
},
'omega': {
desc: "λx.(x x) : A single variable branching out to apply to itself.",
svg: `
<svg width="100" height="140" viewBox="0 0 100 140">
<!-- Abstraction -->
<rect x="10" y="20" width="80" height="8" fill="white" />
<!-- Variable splitting -->
<rect x="26" y="20" width="8" height="40" fill="white" />
<rect x="66" y="20" width="8" height="40" fill="white" />
<rect x="26" y="20" width="48" height="8" fill="white" /> <!-- connector at top to show same var -->
<!-- Application branch -->
<path d="M 26 60 L 26 100 L 66 100 L 66 60" fill="none" stroke="white" stroke-width="8" stroke-linejoin="miter"/>
<rect x="46" y="100" width="8" height="20" fill="white" />
</svg>`
}
};
function drawDiagram(id) {
diagramMount.innerHTML = diagrams[id].svg;
diagramDesc.innerText = diagrams[id].desc;
}
// --- Widget 3: Beta Reduction Stepper ---
const betaStates = [
{
html: `(λ<span style="color:var(--accent-red)">f</span>.λx. <span style="color:var(--accent-red)">f</span> (<span style="color:var(--accent-red)">f</span> x)) <strong>INC</strong> 0`,
desc: "Start. We will apply the function to the argument <code>INC</code>."
},
{
html: `(λx. <strong>INC</strong> (<strong>INC</strong> x)) <span style="color:var(--accent-blue)">0</span>`,
desc: "Beta Reduce! We substituted <code>INC</code> for <code>f</code>. Now we apply it to <code>0</code>."
},
{
html: `<strong>INC</strong> (<strong>INC</strong> <span style="color:var(--accent-blue)">0</span>)`,
desc: "Beta Reduce! We substituted <code>0</code> for <code>x</code>. The lambda expressions are gone."
},
{
html: `<strong>INC</strong> (1)`,
desc: "Evaluate inner expression."
},
{
html: `2`,
desc: "Final Result in Normal Form."
}
];
let betaIndex = 0;
const betaDisplay = document.getElementById('beta-math-display');
const betaDesc = document.getElementById('beta-desc');
const btnPrev = document.getElementById('btn-beta-prev');
const btnNext = document.getElementById('btn-beta-next');
const btnReset = document.getElementById('btn-beta-reset');
function updateBeta() {
betaDisplay.innerHTML = betaStates[betaIndex].html;
betaDesc.innerHTML = betaStates[betaIndex].desc;
btnPrev.disabled = betaIndex === 0;
btnNext.disabled = betaIndex === betaStates.length - 1;
}
btnNext.addEventListener('click', () => { if(betaIndex < betaStates.length - 1) { betaIndex++; updateBeta(); } });
btnPrev.addEventListener('click', () => { if(betaIndex > 0) { betaIndex--; updateBeta(); } });
btnReset.addEventListener('click', () => { betaIndex = 0; updateBeta(); });
// Initialize
updateBeta();
// --- Widget 4: Boolean NOT ---
const notDisplay = document.getElementById('not-display');
const notTraces = {
'TRUE': [
"NOT TRUE",
"(λx. x FALSE TRUE) (λa.λb. a)",
"<span style='color:var(--accent-red)'>(λa.λb. a)</span> FALSE TRUE",
"(λb. <span style='color:var(--accent-red)'>FALSE</span>) TRUE",
"<strong>FALSE</strong>"
],
'FALSE': [
"NOT FALSE",
"(λx. x FALSE TRUE) (λa.λb. b)",
"<span style='color:var(--accent-blue)'>(λa.λb. b)</span> FALSE TRUE",
"(λb. <span style='color:var(--accent-blue)'>b</span>) TRUE <span style='color:#888; font-size:0.8em'>// b binds to second arg</span>",
"<strong>TRUE</strong>"
]
};
function evalNot(input) {
notDisplay.innerHTML = "";
let trace = notTraces[input];
trace.forEach((step, i) => {
setTimeout(() => {
let div = document.createElement('div');
div.innerHTML = step;
div.style.opacity = 0;
div.style.transition = "opacity 0.3s";
notDisplay.appendChild(div);
// trigger layout for animation
setTimeout(() => div.style.opacity = 1, 10);
if(i < trace.length - 1) {
let arrow = document.createElement('div');
arrow.innerHTML = "↓";
arrow.style.color = "#ccc";
arrow.style.fontSize = "0.8em";
notDisplay.appendChild(arrow);
}
}, i * 600); // 600ms stagger
});
}
// --- Widget 5: Church Numerals ---
const churchSlider = document.getElementById('church-slider');
const churchNVal = document.getElementById('church-n-val');
const churchDisplay = document.getElementById('church-display');
function renderChurch(n) {
churchNVal.innerText = n;
if (n == 0) {
churchDisplay.innerHTML = "λf.λx. x";
return;
}
let result = "x";
for(let i=0; i<n; i++) {
result = `f(<span style="color:var(--accent-blue)">${result}</span>)`;
}
churchDisplay.innerHTML = `λ<span style="color:var(--accent-red)">f</span>.λ<span style="color:var(--accent-blue)">x</span>. ${result}`;
}
churchSlider.addEventListener('input', (e) => {
renderChurch(parseInt(e.target.value));
});
// Init church
renderChurch(2);
</script>
</body>
</html>

Comments are disabled for this gist.