diff --git a/src/css/style.css b/src/css/style.css
index 2ff3cb2..ab76e98 100644
--- a/src/css/style.css
+++ b/src/css/style.css
@@ -39,7 +39,7 @@ a:visited {
display: grid;
grid-template-rows: auto 1fr auto;
min-width: 600px;
- width: 45%;
+ width: 70%;
margin-left: auto;
margin-right: auto;
padding: 0;
diff --git a/src/engine/TheAbstractionEngine.ts b/src/engine/TheAbstractionEngine.ts
index 9ea5b90..30c3422 100644
--- a/src/engine/TheAbstractionEngine.ts
+++ b/src/engine/TheAbstractionEngine.ts
@@ -55,15 +55,10 @@ export class TheAbstractionEngine {
const player = new Player();
this.game.addEntity(player);
- const box = new FunctionBox({ x: 3, y: 1 }, "λ x . (x)");
- this.game.addEntity(box);
- const box2 = new FunctionBox({ x: 4, y: 1 }, "λ x . (x)");
- this.game.addEntity(box2);
-
const wall = new Wall({ x: 5, y: 3 });
this.game.addEntity(wall);
- const factory = new LambdaFactory({ x: 6, y: 6 }, "λ x . (x)", 10);
+ const factory = new LambdaFactory({ x: 6, y: 6 }, "(λ (x) . x)", 10);
this.game.addEntity(factory);
const lockedDoor = new LockedDoor({ x: 8, y: 8 });
diff --git a/src/engine/entities/LambdaFactory.ts b/src/engine/entities/LambdaFactory.ts
index 4861c6b..0721f80 100644
--- a/src/engine/entities/LambdaFactory.ts
+++ b/src/engine/entities/LambdaFactory.ts
@@ -134,9 +134,7 @@ export class LambdaFactory extends Entity {
private codeEditor(code: string) {
return `
-
+
`;
diff --git a/src/interpreter/SymbolTable.ts b/src/interpreter/SymbolTable.ts
new file mode 100644
index 0000000..e2ff7e1
--- /dev/null
+++ b/src/interpreter/SymbolTable.ts
@@ -0,0 +1,49 @@
+export class UndefinedSymbolError extends Error {}
+
+export class SymbolTable {
+ private knownSymbols: Set;
+ private parent: SymbolTable | null;
+ private depth: number;
+
+ constructor(parent: SymbolTable | null = null) {
+ this.knownSymbols = new Set();
+ this.parent = parent;
+ this.depth = parent ? parent.getDepth() + 1 : 0;
+ }
+
+ public getDepth() {
+ return this.depth;
+ }
+
+ public add(name: string) {
+ this.knownSymbols.add(name);
+ }
+
+ public get(name: string): number {
+ if (this.knownSymbols.has(name)) {
+ return 1;
+ }
+
+ if (this.parent) {
+ return 1 + this.parent.get(name);
+ }
+
+ throw new UndefinedSymbolError(`Undefined variable: ${name}`);
+ }
+
+ public has(name: string): boolean {
+ if (this.knownSymbols.has(name)) {
+ return true;
+ }
+
+ if (this.parent) {
+ return this.parent.has(name);
+ }
+
+ return false;
+ }
+
+ public createChild(): SymbolTable {
+ return new SymbolTable(this);
+ }
+}
diff --git a/src/interpreter/index.ts b/src/interpreter/index.ts
index 20d0327..838253b 100644
--- a/src/interpreter/index.ts
+++ b/src/interpreter/index.ts
@@ -1,2 +1,3 @@
export * from "./parser";
export * from "./interpreter";
+export * from "./SymbolTable";
diff --git a/src/interpreter/interpreter.ts b/src/interpreter/interpreter.ts
index c16984f..0b3ae34 100644
--- a/src/interpreter/interpreter.ts
+++ b/src/interpreter/interpreter.ts
@@ -1,10 +1,255 @@
-import { parse, type LambdaTerm } from ".";
+import {
+ parse,
+ type LambdaTerm,
+ isVariable,
+ isApplication,
+ isAbstraction,
+ SymbolTable,
+} from ".";
-export const evaluate = (_term: LambdaTerm): LambdaTerm => {
- return "";
+export class InvalidLambdaTermError extends Error {}
+
+export type DebrujinAbstraction = {
+ abstraction: {
+ param: string;
+ body: DebrujinifiedLambdaTerm;
+ };
};
-export const interpret = (term: string): LambdaTerm => {
+export type DebrujinApplication = {
+ application: {
+ left: DebrujinifiedLambdaTerm;
+ args: Array;
+ };
+};
+
+export type DebrujinIndex = { name: string; index: number };
+
+export type DebrujinifiedLambdaTerm =
+ | DebrujinAbstraction
+ | DebrujinApplication
+ | DebrujinIndex;
+
+export const debrujinify = (
+ term: LambdaTerm,
+ symbolTable: SymbolTable,
+): DebrujinifiedLambdaTerm => {
+ if (isVariable(term)) {
+ if (!symbolTable.has(term)) {
+ throw new InvalidLambdaTermError(`Undefined variable: ${term}`);
+ }
+ return { index: symbolTable.get(term), name: term };
+ }
+
+ if (isAbstraction(term)) {
+ const newSymbolTable = symbolTable.createChild();
+ newSymbolTable.add(term.abstraction.param);
+
+ const { body, param } = term.abstraction;
+ return {
+ abstraction: {
+ param,
+ body: debrujinify(body, newSymbolTable),
+ },
+ };
+ }
+
+ if (isApplication(term)) {
+ const { left, args } = term.application;
+ return {
+ application: {
+ left: debrujinify(left, symbolTable),
+ args: args.map((arg) => debrujinify(arg, symbolTable)),
+ },
+ };
+ }
+
+ throw new InvalidLambdaTermError(
+ `Invalid lambda term: ${JSON.stringify(term)}`,
+ );
+};
+
+export const substitute = (
+ inTerm: DebrujinifiedLambdaTerm,
+ index: number,
+ withTerm: DebrujinifiedLambdaTerm,
+): DebrujinifiedLambdaTerm => {
+ if ("index" in inTerm) {
+ if (inTerm.index > index) {
+ return adjustIndices(inTerm, -1);
+ }
+ if (index === inTerm.index) {
+ return withTerm;
+ }
+ return inTerm;
+ }
+
+ if ("application" in inTerm) {
+ const { left, args } = inTerm.application;
+
+ return {
+ application: {
+ left: substitute(left, index, withTerm),
+ args: args.map((arg) => substitute(arg, index, withTerm)),
+ },
+ };
+ }
+
+ if ("abstraction" in inTerm) {
+ const { param, body } = inTerm.abstraction;
+ const newBody = substitute(body, index + 1, withTerm);
+
+ return {
+ abstraction: {
+ param,
+ body: newBody,
+ },
+ };
+ }
+
+ throw new InvalidLambdaTermError(
+ `Invalid lambda term: ${JSON.stringify(inTerm)}`,
+ );
+};
+
+export const adjustIndices = (
+ term: DebrujinifiedLambdaTerm,
+ delta: number,
+): DebrujinifiedLambdaTerm => {
+ if ("index" in term) {
+ return {
+ ...term,
+ index: term.index + delta,
+ };
+ }
+
+ if ("application" in term) {
+ const { left, args } = term.application;
+
+ return {
+ application: {
+ left: adjustIndices(left, delta),
+ args: args.map((arg) => adjustIndices(arg, delta)),
+ },
+ };
+ }
+
+ if ("abstraction" in term) {
+ const { body, param } = term.abstraction;
+
+ return {
+ abstraction: {
+ body: adjustIndices(body, delta),
+ param,
+ },
+ };
+ }
+
+ throw new InvalidLambdaTermError(
+ `Invalid lambda term: ${JSON.stringify(term)}`,
+ );
+};
+
+export const betaReduce = (
+ term: DebrujinifiedLambdaTerm,
+): DebrujinifiedLambdaTerm => {
+ if ("index" in term) {
+ return term;
+ }
+
+ if ("abstraction" in term) {
+ const { body, param } = term.abstraction;
+
+ return {
+ abstraction: {
+ body: betaReduce(body),
+ param,
+ },
+ };
+ }
+
+ if ("application" in term) {
+ const { left } = term.application;
+ const args = term.application.args.map(betaReduce);
+
+ return args.reduce((acc: DebrujinifiedLambdaTerm, x) => {
+ if ("abstraction" in acc) {
+ const { body } = acc.abstraction;
+ const newBody = substitute(body, 1, x);
+ return newBody;
+ }
+ if ("application" in acc) {
+ const {
+ application: { left, args },
+ } = acc;
+ return {
+ application: {
+ left,
+ args: [...args, x],
+ },
+ };
+ }
+ return { application: { left: acc, args: [x] } };
+ }, left);
+ }
+
+ throw new InvalidLambdaTermError(
+ `Invalid lambda term: ${JSON.stringify(term)}`,
+ );
+};
+
+export const interpret = (term: string): DebrujinifiedLambdaTerm => {
const ast = parse(term);
- return evaluate(ast);
+ const symbolTable = new SymbolTable();
+ const debrujined = debrujinify(ast, symbolTable);
+
+ let prev = debrujined;
+ let next = betaReduce(prev);
+
+ while (emitDebrujin(prev) !== emitDebrujin(next)) {
+ // alpha equivalence
+ prev = next;
+ next = betaReduce(prev);
+ }
+ return next;
+};
+
+export const emitDebrujin = (term: DebrujinifiedLambdaTerm): string => {
+ if ("index" in term) {
+ return term.index.toString();
+ }
+
+ if ("abstraction" in term) {
+ return `λ.${emitDebrujin(term.abstraction.body)}`;
+ }
+
+ if ("application" in term) {
+ return `(${emitDebrujin(term.application.left)} ${term.application.args
+ .map(emitDebrujin)
+ .join(" ")})`;
+ }
+
+ throw new InvalidLambdaTermError(
+ `Invalid lambda term: ${JSON.stringify(term)}`,
+ );
+};
+
+export const emitNamed = (term: DebrujinifiedLambdaTerm): string => {
+ if ("name" in term) {
+ return term.name;
+ }
+
+ if ("abstraction" in term) {
+ return `(λ (${term.abstraction.param}) . ${emitNamed(
+ term.abstraction.body,
+ )})`;
+ }
+
+ if ("application" in term) {
+ return `(${emitNamed(term.application.left)} ${term.application.args
+ .map(emitNamed)
+ .join(" ")})`;
+ }
+
+ throw new InvalidLambdaTermError(`Invalid lambda term: ${term}`);
};