Module arithmetic

Implementations of natural numbers and arithmetic operators

lambda_calculus.terms.arithmetic.ISZERO: Final = Abstraction(bound='n', body=Application(abstraction=Application(abstraction=Variable(name='n'), argument=Abstraction(bound='x', body=Abstraction(bound='x', body=Abstraction(bound='y', body=Variable(name='y'))))), argument=Abstraction(bound='x', body=Abstraction(bound='y', body=Variable(name='x'))))): Term which evaluates to lambda_calculus.terms.logic.TRUE if its argument is zero, lambda_calculus.terms.logic.FALSE otherwise

lambda_calculus.terms.arithmetic.SUCCESSOR: Final = Abstraction(bound='n', body=Abstraction(bound='f', body=Abstraction(bound='x', body=Application(abstraction=Variable(name='f'), argument=Application(abstraction=Application(abstraction=Variable(name='n'), argument=Variable(name='f')), argument=Variable(name='x')))))): Term evaluating to its argument incremented by one.

lambda_calculus.terms.arithmetic.PREDECESSOR: Final = Abstraction(bound='n', body=Abstraction(bound='f', body=Abstraction(bound='x', body=Application(abstraction=Application(abstraction=Application(abstraction=Variable(name='n'), argument=Abstraction(bound='g', body=Abstraction(bound='h', body=Application(abstraction=Variable(name='h'), argument=Application(abstraction=Variable(name='g'), argument=Variable(name='f')))))), argument=Abstraction(bound='u', body=Variable(name='x'))), argument=Abstraction(bound='u', body=Variable(name='u')))))): Term ealuating to its argument decremented by one.

lambda_calculus.terms.arithmetic.ADD: Final = Abstraction(bound='m', body=Abstraction(bound='n', body=Abstraction(bound='f', body=Abstraction(bound='x', body=Application(abstraction=Application(abstraction=Variable(name='m'), argument=Variable(name='f')), argument=Application(abstraction=Application(abstraction=Variable(name='n'), argument=Variable(name='f')), argument=Variable(name='x'))))))): Term evaluating to the sum of its two arguments.

lambda_calculus.terms.arithmetic.SUBTRACT: Final = Abstraction(bound='m', body=Abstraction(bound='n', body=Application(abstraction=Application(abstraction=Variable(name='n'), argument=Abstraction(bound='n', body=Abstraction(bound='f', body=Abstraction(bound='x', body=Application(abstraction=Application(abstraction=Application(abstraction=Variable(name='n'), argument=Abstraction(bound='g', body=Abstraction(bound='h', body=Application(abstraction=Variable(name='h'), argument=Application(abstraction=Variable(name='g'), argument=Variable(name='f')))))), argument=Abstraction(bound='u', body=Variable(name='x'))), argument=Abstraction(bound='u', body=Variable(name='u'))))))), argument=Variable(name='m')))): Term evaluating to the difference of its two arguments.

lambda_calculus.terms.arithmetic.MULTIPLY: Final = Abstraction(bound='m', body=Abstraction(bound='n', body=Abstraction(bound='f', body=Application(abstraction=Variable(name='m'), argument=Application(abstraction=Variable(name='n'), argument=Variable(name='f')))))): Term evaluating to the product of its two arguments.

lambda_calculus.terms.arithmetic.POWER: Final = Abstraction(bound='b', body=Abstraction(bound='e', body=Application(abstraction=Variable(name='e'), argument=Variable(name='b')))): Term evaluating to its first argument to the power of its second argument.

lambda_calculus.terms.arithmetic.number(n: int) → Abstraction[str][source]

Encode a number as a lambda term.