misc_python

Sean's miscellaneous Python code that's not big enough for its own repo.
Log | Files | Refs | README | LICENSE

commit ab203aa9ccb2b323e1c6009a195f2e0da50fa79f
parent 30fdb929977161075c7314f0523ffa0f6ec7e50f
Author: Sean Lynch <seanl@literati.org>
Date:   Tue, 28 Dec 2010 22:53:02 -0800

Add conversion to SKI.

Diffstat:
Mlam.py | 70++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++----------
1 file changed, 60 insertions(+), 10 deletions(-)

diff --git a/lam.py b/lam.py @@ -31,9 +31,15 @@ class Expression(object): def bind(self, name, variable): return self + def contains(self, variable): + return False + def substitute(self, variable, value, cache=None): return self + def t(self): + return self + class FreeVariable(Expression): """A free variable""" @@ -146,6 +152,9 @@ class Application(Expression): return result + def t(self): + return self.left.t()(self.right.t()) + class Lambda(Expression): """A lambda expression""" @@ -170,6 +179,9 @@ class Lambda(Expression): self.body = self.body.bind(name, variable) return self + def contains(self, variable): + return self.variable != variable and self.body.contains(variable) + def de_brujin(self, variables=None, **kwargs): if variables is None: variables = [] @@ -180,6 +192,9 @@ class Lambda(Expression): variables.pop() return result + def is_identity(self): + return self.body == self.variable + def substitute(self, variable, value, cache=None): if self.variable == variable: print "lambda variable renaming" @@ -200,32 +215,66 @@ class Lambda(Expression): return result + def t(self): + if self in (S, K, I): + return self + + if self.body == self.variable: + return I + elif not self.body.contains(self.variable): + return K(self.body.t()) + elif isinstance(self.body, Lambda) and \ + self.body.contains(self.variable): + return Lambda(self.variable, Lambda(self.body.variable, + self.body.body).t()).t() + elif isinstance(self.body, Application): + return S(Lambda(self.variable, self.body.left).t())(Lambda(self.variable, self.body.right).t()) def print_reductions(name, expression): print name reduced = True while reduced: # print expression - print expression.de_brujin(omit_parens=True) + print compress(expression.de_brujin(omit_parens=True)) reduced = expression.beta_reduce() + print compress(expression.t().de_brujin(omit_parens=True)) print +_substitutions = [ + ("[[[2 0 (1 0)]]]", "S"), + ("[[[2 (1 0)]]]", "B"), + ("[[[2 0 1]]]", "C"), + ("[[1 0 0]]", "W"), + ("[[0]]", "F"), + ("[[1]]", "K"), + ("[0]", "I"), + ] + + +def compress(s): + for old, new in _substitutions: + s = s.replace(old, new) + + return s + + +I = Lambda('x', 'x') +K = T = Lambda('x', Lambda('y', 'x')) +F = Lambda('x', I) +S = Lambda('x', Lambda('y', Lambda('z', Application('x', 'z')(Application('y', 'z'))))) +B = Lambda("x", Lambda("y", Lambda("z", ("x", ("y", "z"))))) +C = Lambda("x", Lambda("y", Lambda("z", ("x", "z", "y")))) +W = Lambda("x", Lambda("y", ("x", "y", "y"))) + + def main(): - I = Lambda('x', 'x') - K = T = Lambda('x', Lambda('y', 'x')) - F = Lambda('x', I) - S = Lambda('x', Lambda('y', Lambda('z', Application('x', 'z')(Application('y', 'z'))))) - W = Lambda('x', Application('x', 'x')) - O = W(W) print_reductions("I", I) print_reductions("K", K) print_reductions("F", F) print_reductions("S", S) print_reductions("SKK", S(K)(K)) - print_reductions("W", W) - print_reductions("O", O) zero = F one = Lambda("s", Lambda("z", ("s", "z"))) succ = Lambda("x", Lambda("s", Lambda("z", ("s", ("x", "s", "z"))))) @@ -250,9 +299,10 @@ def main(): times = Lambda("m", Lambda("n", ("m", plus("n"), zero))) g = Lambda("r", Lambda("n", ifthenelse(iszero("n"))(one)(times("n")(("r", "r", sub("n")(one)))))) print_reductions("g", g) - print_reductions("KIO", K(I)(O)) print_reductions("bad", Lambda("y", Lambda("x", ("x", "x"))(Lambda("x", "x")("y")))) print_reductions("g (Y g) three", g(Y(g))(three)) + print "Y" + print compress(Y.t().de_brujin(omit_parens=True)) if __name__ == "__main__":