Here is the same simple task — add one to a number — computed two completely different ways. On the left, a tiny Turing machine crawls along a tape of 1s and flips a symbol. On the right, the lambda calculus applies its successor function by pure substitution. Pick a number and step through both.
<p class="hint">The same task computed two ways: <b>add one</b> to a number n. Left, a Turing machine moves a head over a tape of 1s and appends one more. Right, the lambda calculus applies the <b>successor</b> to a Church numeral by substitution. Pick n, then step through both — they always agree.</p>
<div class="pick">
n =
<button class="np" data-n="0" type="button">0</button>
<button class="np" data-n="1" type="button">1</button>
<button class="np" data-n="2" type="button">2</button>
<button class="np" data-n="3" type="button">3</button>
</div>
<div class="cols">
<div class="panel">
<h4>Turing machine</h4>
<div id="tape" class="tape"></div>
<div class="tm-state" id="tmstate">state: start</div>
</div>
<div class="panel">
<h4>Lambda calculus</h4>
<div id="lam" class="lam"></div>
<div class="tm-state" id="lamstate">successor n</div>
</div>
</div>
<div class="status" id="status">Pick n, then step.</div>
<div class="btns">
<button id="step" type="button">Step</button>
<button id="run" type="button">Run to end</button>
<button id="reset" type="button" class="ghost">Reset</button>
</div>
<div class="result" id="result"></div>
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
.pick { font: 600 15px system-ui; margin: 0 0 .8rem; display: flex; gap: .4rem; align-items: center; }
.np { padding: .3rem .7rem; border: 1px solid #1d3557; background: #fff; color: #1d3557; border-radius: 7px; cursor: pointer; font: 600 14px system-ui; }
.np.on { background: #1d3557; color: #fff; }
.cols { display: grid; grid-template-columns: 1fr 1fr; gap: .8rem; }
.panel { border: 1px solid #cdd9e3; border-radius: 10px; padding: .7rem; background: #f6f9fb; min-height: 120px; }
.panel h4 { margin: 0 0 .6rem; font-size: .85rem; color: #1d3557; letter-spacing: .03em; text-transform: uppercase; }
.tape { display: flex; gap: 3px; flex-wrap: wrap; }
.cell { width: 30px; height: 34px; display: flex; align-items: center; justify-content: center;
font: 700 16px ui-monospace, monospace; background: #fff; border: 1px solid #cdd9e3; border-radius: 6px; position: relative; }
.cell.head { border-color: #e63946; border-width: 2px; }
.cell.head::after { content: "▲"; position: absolute; bottom: -16px; color: #e63946; font-size: 11px; }
.lam { font: 600 14px ui-monospace, monospace; color: #1d3557; line-height: 1.7; word-break: break-word; }
.lam .hot { background: #fde68a; border-radius: 3px; padding: 0 2px; }
.tm-state { font: 600 12px ui-monospace, monospace; color: #5a6b7b; margin-top: 1.4rem; }
.status { font-size: 1rem; font-weight: 600; margin: .7rem 0 .3rem; min-height: 1.4em; }
.status.ok { color: #0a7d33; }
.result { font: 700 15px system-ui; color: #0a7d33; min-height: 1.4em; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-top: .3rem; }
button#step, button#run { font: 600 14px system-ui; padding: .45rem .9rem; border: 1px solid #1d3557; background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// The Church-Turing thesis says different models of computation compute the
// same functions. Here both compute succ(n) = n + 1.
//
// TURING MACHINE (unary): tape holds n ones then a blank '_'. The head walks
// right over the 1s; on reaching the blank it writes a 1 and halts. Result =
// n+1 ones. (Classic unary successor.)
//
// LAMBDA CALCULUS: a Church numeral n is \f.\x. f(f(...x)) with n applications.
// succ = \n.\f.\x. f (n f x). Applying succ adds exactly one more f. We render
// the reduction symbolically and report the resulting numeral's count.
let n = 0, mode = null;
let tape = [], head = 0, tmState = 'scan', tmDone = false;
let lamSteps = [], lamIdx = 0;
const $ = id => document.getElementById(id);
function init(k){
n = k; mode = 'ready'; tmDone = false;
// Turing tape: n ones + one blank, head at 0
tape = Array(n).fill('1'); tape.push('_'); head = 0; tmState = 'scan';
// Lambda reduction script for succ n
const body = churchBody(n); // f (f (... x)) with n applications
lamSteps = [
'succ ' + churchLabel(n),
'(\\n.\\f.\\x. f (n f x)) (' + churchLabel(n) + ')',
'\\f.\\x. f (' + churchLabel(n) + ' f x)',
'\\f.\\x. f (' + body + ')',
'\\f.\\x. ' + churchBody(n+1),
churchLabel(n+1)
];
lamIdx = 0;
$('status').textContent = 'Pick n, then step.'; $('status').className = 'status';
$('result').textContent = '';
render();
}
function churchLabel(k){ return k + ' = \\f.\\x. ' + churchBody(k); }
function churchBody(k){ // f (f (... x)) with k applications of f
let s = 'x';
for(let i=0;i<k;i++) s = 'f (' + s + ')';
return s;
}
function render(){
// tape
const t = $('tape'); t.innerHTML = '';
tape.forEach((sym,i)=>{
const d = document.createElement('div');
d.className = 'cell' + (i===head ? ' head' : '');
d.textContent = sym;
t.appendChild(d);
});
$('tmstate').textContent = fmt('state: %v% (head@%head%)', { v: tmDone ? 'halt' : tmState, head: head });
// lambda
$('lam').textContent = lamSteps[lamIdx];
$('lamstate').textContent = fmt('step %lamIdx%%v% / %length%', { lamIdx: lamIdx, v: 1, length: lamSteps.length });
}
// One TM step: scan right over 1s; at blank, write 1 and halt.
function tmStep(){
if(tmDone) return;
if(tape[head] === '1'){ head++; }
else { tape[head] = '1'; tape.push('_'); tmDone = true; tmState = 'halt'; }
}
function tmCount(){ return tape.filter(s=>s==='1').length; }
function step(){
if(mode === null){ return; }
if(!tmDone) tmStep();
if(lamIdx < lamSteps.length-1) lamIdx++;
render();
if(tmDone && lamIdx === lamSteps.length-1) finish();
else { $('status').textContent = 'Stepping…'; $('status').className = 'status'; }
}
function run(){ let guard=0; while((!tmDone || lamIdx<lamSteps.length-1) && guard++<50) step(); }
function finish(){
const tm = tmCount(), lam = n+1;
const agree = tm === lam;
$('status').textContent = agree
? fmt('✓ Both models computed %n% + 1 = %tm%', { n: n, tm: tm })
: fmt('Mismatch (%tm% vs %lam%)', { tm: tm, lam: lam });
$('status').className = 'status' + (agree ? ' ok' : '');
$('result').textContent = agree
? fmt('Turing tape has %tm% ones; lambda numeral is %lam%. Same answer.', { tm: tm, lam: lam })
: '';
console.log('n=' + n, '| TM ones =', tm, '| lambda =', lam, '| agree =', agree);
}
document.querySelectorAll('.np').forEach(b=>b.addEventListener('click',()=>{
document.querySelectorAll('.np').forEach(x=>x.classList.remove('on'));
b.classList.add('on'); init(parseInt(b.dataset.n,10));
}));
$('step').addEventListener('click', step);
$('run').addEventListener('click', run);
$('reset').addEventListener('click', ()=>{ if(mode) init(n); });
// start with n = 0 selected
document.querySelector('.np[data-n="0"]').classList.add('on');
init(0);
<p class="hint">The same task computed two ways: <b>add one</b> to a number n. Left, a Turing machine moves a head over a tape of 1s and appends one more. Right, the lambda calculus applies the <b>successor</b> to a Church numeral by substitution. Pick n, then step through both — they always agree.</p>
<div class="pick">
n =
<button class="np" data-n="0" type="button">0</button>
<button class="np" data-n="1" type="button">1</button>
<button class="np" data-n="2" type="button">2</button>
<button class="np" data-n="3" type="button">3</button>
</div>
<div class="cols">
<div class="panel">
<h4>Turing machine</h4>
<div id="tape" class="tape"></div>
<div class="tm-state" id="tmstate">state: start</div>
</div>
<div class="panel">
<h4>Lambda calculus</h4>
<div id="lam" class="lam"></div>
<div class="tm-state" id="lamstate">successor n</div>
</div>
</div>
<div class="status" id="status">Pick n, then step.</div>
<div class="btns">
<button id="step" type="button">Step</button>
<button id="run" type="button">Run to end</button>
<button id="reset" type="button" class="ghost">Reset</button>
</div>
<div class="result" id="result"></div>
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
.pick { font: 600 15px system-ui; margin: 0 0 .8rem; display: flex; gap: .4rem; align-items: center; }
.np { padding: .3rem .7rem; border: 1px solid #1d3557; background: #fff; color: #1d3557; border-radius: 7px; cursor: pointer; font: 600 14px system-ui; }
.np.on { background: #1d3557; color: #fff; }
.cols { display: grid; grid-template-columns: 1fr 1fr; gap: .8rem; }
.panel { border: 1px solid #cdd9e3; border-radius: 10px; padding: .7rem; background: #f6f9fb; min-height: 120px; }
.panel h4 { margin: 0 0 .6rem; font-size: .85rem; color: #1d3557; letter-spacing: .03em; text-transform: uppercase; }
.tape { display: flex; gap: 3px; flex-wrap: wrap; }
.cell { width: 30px; height: 34px; display: flex; align-items: center; justify-content: center;
font: 700 16px ui-monospace, monospace; background: #fff; border: 1px solid #cdd9e3; border-radius: 6px; position: relative; }
.cell.head { border-color: #e63946; border-width: 2px; }
.cell.head::after { content: "▲"; position: absolute; bottom: -16px; color: #e63946; font-size: 11px; }
.lam { font: 600 14px ui-monospace, monospace; color: #1d3557; line-height: 1.7; word-break: break-word; }
.lam .hot { background: #fde68a; border-radius: 3px; padding: 0 2px; }
.tm-state { font: 600 12px ui-monospace, monospace; color: #5a6b7b; margin-top: 1.4rem; }
.status { font-size: 1rem; font-weight: 600; margin: .7rem 0 .3rem; min-height: 1.4em; }
.status.ok { color: #0a7d33; }
.result { font: 700 15px system-ui; color: #0a7d33; min-height: 1.4em; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-top: .3rem; }
button#step, button#run { font: 600 14px system-ui; padding: .45rem .9rem; border: 1px solid #1d3557; background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// The Church-Turing thesis says different models of computation compute the
// same functions. Here both compute succ(n) = n + 1.
//
// TURING MACHINE (unary): tape holds n ones then a blank '_'. The head walks
// right over the 1s; on reaching the blank it writes a 1 and halts. Result =
// n+1 ones. (Classic unary successor.)
//
// LAMBDA CALCULUS: a Church numeral n is \f.\x. f(f(...x)) with n applications.
// succ = \n.\f.\x. f (n f x). Applying succ adds exactly one more f. We render
// the reduction symbolically and report the resulting numeral's count.
let n = 0, mode = null;
let tape = [], head = 0, tmState = 'scan', tmDone = false;
let lamSteps = [], lamIdx = 0;
const $ = id => document.getElementById(id);
function init(k){
n = k; mode = 'ready'; tmDone = false;
// Turing tape: n ones + one blank, head at 0
tape = Array(n).fill('1'); tape.push('_'); head = 0; tmState = 'scan';
// Lambda reduction script for succ n
const body = churchBody(n); // f (f (... x)) with n applications
lamSteps = [
'succ ' + churchLabel(n),
'(\\n.\\f.\\x. f (n f x)) (' + churchLabel(n) + ')',
'\\f.\\x. f (' + churchLabel(n) + ' f x)',
'\\f.\\x. f (' + body + ')',
'\\f.\\x. ' + churchBody(n+1),
churchLabel(n+1)
];
lamIdx = 0;
$('status').textContent = 'Pick n, then step.'; $('status').className = 'status';
$('result').textContent = '';
render();
}
function churchLabel(k){ return k + ' = \\f.\\x. ' + churchBody(k); }
function churchBody(k){ // f (f (... x)) with k applications of f
let s = 'x';
for(let i=0;i<k;i++) s = 'f (' + s + ')';
return s;
}
function render(){
// tape
const t = $('tape'); t.innerHTML = '';
tape.forEach((sym,i)=>{
const d = document.createElement('div');
d.className = 'cell' + (i===head ? ' head' : '');
d.textContent = sym;
t.appendChild(d);
});
$('tmstate').textContent = fmt('state: %v% (head@%head%)', { v: tmDone ? 'halt' : tmState, head: head });
// lambda
$('lam').textContent = lamSteps[lamIdx];
$('lamstate').textContent = fmt('step %lamIdx%%v% / %length%', { lamIdx: lamIdx, v: 1, length: lamSteps.length });
}
// One TM step: scan right over 1s; at blank, write 1 and halt.
function tmStep(){
if(tmDone) return;
if(tape[head] === '1'){ head++; }
else { tape[head] = '1'; tape.push('_'); tmDone = true; tmState = 'halt'; }
}
function tmCount(){ return tape.filter(s=>s==='1').length; }
function step(){
if(mode === null){ return; }
if(!tmDone) tmStep();
if(lamIdx < lamSteps.length-1) lamIdx++;
render();
if(tmDone && lamIdx === lamSteps.length-1) finish();
else { $('status').textContent = 'Stepping…'; $('status').className = 'status'; }
}
function run(){ let guard=0; while((!tmDone || lamIdx<lamSteps.length-1) && guard++<50) step(); }
function finish(){
const tm = tmCount(), lam = n+1;
const agree = tm === lam;
$('status').textContent = agree
? fmt('✓ Both models computed %n% + 1 = %tm%', { n: n, tm: tm })
: fmt('Mismatch (%tm% vs %lam%)', { tm: tm, lam: lam });
$('status').className = 'status' + (agree ? ' ok' : '');
$('result').textContent = agree
? fmt('Turing tape has %tm% ones; lambda numeral is %lam%. Same answer.', { tm: tm, lam: lam })
: '';
console.log('n=' + n, '| TM ones =', tm, '| lambda =', lam, '| agree =', agree);
}
document.querySelectorAll('.np').forEach(b=>b.addEventListener('click',()=>{
document.querySelectorAll('.np').forEach(x=>x.classList.remove('on'));
b.classList.add('on'); init(parseInt(b.dataset.n,10));
}));
$('step').addEventListener('click', step);
$('run').addEventListener('click', run);
$('reset').addEventListener('click', ()=>{ if(mode) init(n); });
// start with n = 0 selected
document.querySelector('.np[data-n="0"]').classList.add('on');
init(0);
They look nothing alike: one shuffles symbols on a tape, the other rewrites an expression. Yet for every input they land on the same answer. That is the Church-Turing thesis in miniature — different notations for computation, identical computational power. Stretch this from "+1" to any effective procedure and the agreement still holds.
Comments
Loading comments...