add max depth term
This commit is contained in:
parent
46afe9c7ba
commit
d903bd9a13
@ -9,6 +9,8 @@ import {
|
||||
|
||||
export class InvalidLambdaTermError extends Error {}
|
||||
|
||||
export class MaxRecursionDepthError extends Error {}
|
||||
|
||||
export type DebrujinAbstraction = {
|
||||
abstraction: {
|
||||
param: string;
|
||||
@ -32,7 +34,7 @@ export type DebrujinifiedLambdaTerm =
|
||||
|
||||
export const debrujinify = (
|
||||
term: LambdaTerm,
|
||||
symbolTable: SymbolTable,
|
||||
symbolTable: SymbolTable
|
||||
): DebrujinifiedLambdaTerm => {
|
||||
if (isVariable(term)) {
|
||||
if (!symbolTable.has(term)) {
|
||||
@ -65,14 +67,14 @@ export const debrujinify = (
|
||||
}
|
||||
|
||||
throw new InvalidLambdaTermError(
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`,
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`
|
||||
);
|
||||
};
|
||||
|
||||
export const substitute = (
|
||||
inTerm: DebrujinifiedLambdaTerm,
|
||||
index: number,
|
||||
withTerm: DebrujinifiedLambdaTerm,
|
||||
withTerm: DebrujinifiedLambdaTerm
|
||||
): DebrujinifiedLambdaTerm => {
|
||||
if ("index" in inTerm) {
|
||||
if (inTerm.index > index) {
|
||||
@ -108,13 +110,13 @@ export const substitute = (
|
||||
}
|
||||
|
||||
throw new InvalidLambdaTermError(
|
||||
`Invalid lambda term: ${JSON.stringify(inTerm)}`,
|
||||
`Invalid lambda term: ${JSON.stringify(inTerm)}`
|
||||
);
|
||||
};
|
||||
|
||||
export const adjustIndices = (
|
||||
term: DebrujinifiedLambdaTerm,
|
||||
delta: number,
|
||||
delta: number
|
||||
): DebrujinifiedLambdaTerm => {
|
||||
if ("index" in term) {
|
||||
return {
|
||||
@ -146,13 +148,17 @@ export const adjustIndices = (
|
||||
}
|
||||
|
||||
throw new InvalidLambdaTermError(
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`,
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`
|
||||
);
|
||||
};
|
||||
|
||||
export const betaReduce = (
|
||||
term: DebrujinifiedLambdaTerm,
|
||||
maxDepth: number,
|
||||
): DebrujinifiedLambdaTerm => {
|
||||
if (maxDepth === 0) {
|
||||
throw new MaxRecursionDepthError("max recursion depth identified");
|
||||
}
|
||||
if ("index" in term) {
|
||||
return term;
|
||||
}
|
||||
@ -162,7 +168,7 @@ export const betaReduce = (
|
||||
|
||||
return {
|
||||
abstraction: {
|
||||
body: betaReduce(body),
|
||||
body: betaReduce(body, maxDepth - 1),
|
||||
param,
|
||||
},
|
||||
};
|
||||
@ -170,7 +176,9 @@ export const betaReduce = (
|
||||
|
||||
if ("application" in term) {
|
||||
const { left } = term.application;
|
||||
const args = term.application.args.map(betaReduce);
|
||||
const args = term.application.args.map((term) =>
|
||||
betaReduce(term, maxDepth - 1)
|
||||
);
|
||||
|
||||
return args.reduce((acc: DebrujinifiedLambdaTerm, x) => {
|
||||
if ("abstraction" in acc) {
|
||||
@ -194,7 +202,7 @@ export const betaReduce = (
|
||||
}
|
||||
|
||||
throw new InvalidLambdaTermError(
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`,
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`
|
||||
);
|
||||
};
|
||||
|
||||
@ -214,7 +222,7 @@ export const emitDebrujin = (term: DebrujinifiedLambdaTerm): string => {
|
||||
}
|
||||
|
||||
throw new InvalidLambdaTermError(
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`,
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`
|
||||
);
|
||||
};
|
||||
|
||||
@ -225,7 +233,7 @@ export const emitNamed = (term: DebrujinifiedLambdaTerm): string => {
|
||||
|
||||
if ("abstraction" in term) {
|
||||
return `(λ (${term.abstraction.param}) . ${emitNamed(
|
||||
term.abstraction.body,
|
||||
term.abstraction.body
|
||||
)})`;
|
||||
}
|
||||
|
||||
@ -241,18 +249,19 @@ export const emitNamed = (term: DebrujinifiedLambdaTerm): string => {
|
||||
export const interpret = (
|
||||
term: string,
|
||||
symbolTable = new SymbolTable(),
|
||||
allowUnderscores = false,
|
||||
maxDepth = 15,
|
||||
allowUnderscores = false
|
||||
): DebrujinifiedLambdaTerm => {
|
||||
const ast = parse(term, allowUnderscores);
|
||||
const debrujined = debrujinify(ast, symbolTable);
|
||||
|
||||
let prev = debrujined;
|
||||
let next = betaReduce(prev);
|
||||
let next = betaReduce(prev, maxDepth);
|
||||
|
||||
while (emitDebrujin(prev) !== emitDebrujin(next)) {
|
||||
// alpha equivalence
|
||||
prev = next;
|
||||
next = betaReduce(prev);
|
||||
next = betaReduce(prev, maxDepth);
|
||||
}
|
||||
return next;
|
||||
};
|
||||
|
Loading…
x
Reference in New Issue
Block a user