Skip to content

Instantly share code, notes, and snippets.

@Raynos
Created October 7, 2011 14:03
Show Gist options
  • Save Raynos/1270349 to your computer and use it in GitHub Desktop.
Save Raynos/1270349 to your computer and use it in GitHub Desktop.
var pd = function _pd(props) {
var obj = {};
Object.keys(props).forEach(function (key) {
obj[key] = Object.getOwnPropertyDescriptor(props, key);
});
return obj;
};
pd.merge = function _merge() {
var o = {}
var objs = Array.prototype.slice.call(arguments);
objs.forEach(function (obj) {
Object.keys(obj).forEach(function (key) {
o[key] = obj[key];
});
});
return o;
};
pd.create = function _create(proto, defaults) {
var factory = function _factory(props) {
var o = Object.create(proto, pd(pd.merge(defaults, props)));
proto.constructor && proto.constructor.apply(o, arguments);
return o;
};
factory.proto = proto;
factory.defaults = defaults;
return factory;
};
var lambda = (function() {
var variables = /[^Lλ\s()#\.]/,
lambda = /^[Lλ]([^Lλ\s()#\.])[\.](.+)$/,
bracket = /^[(].+$/,
whitespace = /[\s]/;
var Variable = pd.create({
alpha: function _alpha(target, source) {
if (this.value === source) {
return Variable({ value: target });
} else {
return Variable({ value: this.value });
}
},
constructor: function _constructor() {
this.free = {};
this.free[this.value] = true;
},
equal: function _equal(term) {
return term && this.value === term.value;
},
substitute: function _substitute(variable, term) {
if (this.value === variable) {
return term
}
return this;
},
reduce: function _reduce() { return false; },
toString: function _toString() {
return this.value;
}
}, {
type: "variable"
});
var Application = pd.create({
alpha: function _alpha(target, source) {
return Application({
left: this.left.alpha(target, source),
right: this.right.alpha(target, source)
});
},
constructor: function _constructor() {
this.free = pd.merge(this.left.free, this.right.free);
},
equal: function _equal(term) {
return term && this.left.equal(term.left) && this.right.equal(term.right);
},
substitute: function _substitute(variable, term) {
return Application({
left: this.left.substitute(variable, term),
right: this.right.substitute(variable, term)
});
},
reduce: function _reduce() {
return this.left.term && this.left.term.substitute(
this.left.variable.value,
this.right
);
},
toString: function _toString() {
return this.left.toString() + " " + this.right.toString();
}
}, {
type: "application"
});
var Abstraction = pd.create({
alpha: function _alpha() {
return Abstraction({
variable: Variable({ value: this.variable.value }),
term: this.term.alpha()
});
},
constructor: function _constructor() {
this.free = this.term.free;
this.free[this.variable.value] = false;
},
equal: function _equal(term) {
var source = this.variable.value;
target = term && term.variable && term.variable.value;
return this.term.alpha(target, source).equal(term && term.term);
},
substitute: function _substitute(variable, term) {
var abstraction = this.alpha();
if (this.variable.value === variable) {
return abstraction;
} else if (term.free[this.variable.value]) {
var value = getAvailableVariable(this.term.free);
abstraction = Abstraction({
variable: Variable({ value: value }),
term: this.term.alpha(value, this.variable.value)
});
}
abstraction.term = abstraction.term.substitute(variable, term);
return abstraction;
},
reduce: function _reduce() { return false; },
toString: function _toString() {
return "λ" + this.variable.value + ".(" + this.term.toString() + ")"
}
}, {
type: "abstraction"
});
function getAvailableVariable(free) {
for (var i = 97; i > 0; i++) {
var char = String.fromCharCode(i);
if (free[char] === undefined) {
return char;
}
}
return false;
}
var parser = function _parser(str) {
var tokens = str.trim().split(/\s/);
var term,
previousTerm;
function parseBrackets() {
var brackets = 1,
start = i + 1,
char;
while (brackets !== 0) {
if (i === len) {
console.log("bad brackets");
return false;
}
char = str.charAt(++i);
if (char === '(') {
brackets++;
} else if (char === ')') {
brackets--;
}
}
return parser(str.slice(start, i));
}
function getTerm(str) {
if (variables.test(str)) {
return Variable({ value: char });
} else if (lambda.test(str)) {
var variable = Variable({ value: str.charAt(++i) });
if (!dot.test(str.charAt(++i))) {
return false;
}
var term = parser(str.slice(++i));
return Abstraction({
variable: variable,
term: term
});
} else if (bracket.test(str)) {
return parseBrackets(str);
} else {
console.log("character not recognised");
return false;
}
};
tokens.filter(function(str) {
return !(whitespace.test(str) || str.length === 0);
}).forEach(function (str) {
if (!(term = getTerm(str))) {
return false;
}
if (previousTerm) {
term = Application({
left: previousTerm,
right: term
});
}
previousTerm = term;
});
return term;
};
return {
term: parser
};
})();
var term = lambda.term;
/*
console.log(term(" x "));
console.log(term("Lx.y"));
console.log(term("mnp"));
console.log(term("Lx.ym"));
console.log(term("(m)(np)"));
console.log(term("nm").equal(term("nm")));
console.log(term("Lx.x").equal(term("Ly.y")));
console.log(term("Lx.xz").equal(term("Ly.yz")));
console.log(term("xx").substitute("x", term("y")));
*/
console.log(term("Lx.y").substitute("y", term("x")).toString());
console.log(term("(Lx.xy) z").reduce().toString());
console.log(term("(Lf.Lx.fx) z").reduce().toString());
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment