Package terms

Module abc
Module logic
- TRUE
- FALSE
- AND
- OR
- NOT
- IF_THEN_ELSE
Module arithmetic
- ISZERO
- SUCCESSOR
- PREDECESSOR
- ADD
- SUBTRACT
- MULTIPLY
- POWER
- number()
Module pairs
- PAIR
- FIRST
- SECOND
- NIL
- NULL
Module combinators
- Y
- S
- K
- I
- B
- C
- W
- DELTA
- OMEGA

Lambda Terms

class lambda_calculus.terms.Term[source]

Bases: Iterable[Term[V]]

ABC for Lambda terms.

Type Variables:

V: represents the type of variables used in terms

__iter__() → Iterator[Term[V]][source]

Returns: Iterator over all subterms

abstract __str__() → str[source]

Create a string representation.

Returns: lambda term string

abstract free_variables() → Set[V][source]

Calculate the free variables of this Term.

Returns: variables not bound by an abstraction

abstract bound_variables() → Set[V][source]

Calculate the bound variables of this Term.

Returns: variables bound by an abstraction

abstract is_beta_normal_form() → bool[source]

Check if this Term is in beta-normal form.

Returns: if no beta reductions can be performed

abstract accept(visitor: Visitor[T, V]) → T[source]

Accept a visitor by calling his corresponding method.

Parameters: visitor – Visitor to accept
Returns: value returned by the visitors corresponding method

abstract(*variables: V) → Abstraction[V][source]

Create an Abstraction binding multiple variables.

Parameters: variables – Variables to bind, from first to last
Returns: requested Abstraction term

apply_to(*arguments: Term[V]) → Application[V][source]

Create an Application applying self to multiple arguments.

Parameters: arguments – arguments to apply to, from first to last
Returns: requested Application term

substitute(variable: V, value: Term[V]) → Term[V][source]

Substitute a free variable with a Term.

Parameters

variable – Variable to substitute
value – Value to be substituted

Raises

errors.CollisionError – If substitution would bind free variables

Returns

new term

is_combinator() → bool[source]

Check if this Term has no free variables.

Returns: If there are no free variables

final class lambda_calculus.terms.Variable(name: V)[source]

Bases: Term[V]

Term consisting of a Variable

Parameters: name – Name of the Variable

classmethod with_valid_name(name: V) → Variable[V][source]

Create an instance with a valid name.

Parameters: name – Name of the Variable
Raises: ValueError – If the name would conflict with string representations
Returns: requested Variable term

__str__() → str[source]

Create a string representation.

Returns: variable name

free_variables() → Set[V][source]

Calculate the free variables of this Term.

Returns: variables not bound by an abstraction

bound_variables() → Set[V][source]

Calculate the bound variables of this Term.

Returns: variables bound by an abstraction

is_beta_normal_form() → bool[source]

Check if this Term is in beta-normal form.

Returns: if no beta reductions can be performed

accept(visitor: Visitor[T, V]) → T[source]

Accept a visitor by calling visitors.Visitor.visit_variable.

Parameters: visitor – Visitor to accept
Returns: value returned by visitors.Visitor.visit_variable

final class lambda_calculus.terms.Abstraction(bound: V, body: Term[V])[source]

Bases: Term[V]

Term consisting of a lambda abstraction.

Parameters

bound – variable to be bound by this abstraction
body – term to be abstracted

classmethod curried(variables: Sequence[V], body: Term[V]) → Abstraction[V][source]

Create an Abstraction binding multiple variables.

Parameters

variables – variables to be bound, from first to last
body – term to be abstracted

Raises

ValueError – If no variables are passed

Returns

requested Abstraction term

__str__() → str[source]

Create a string representation.

Returns: (λ{bound}.{body})

free_variables() → Set[V][source]

Calculate the free variables of this Term.

Returns: variables not bound by an abstraction

bound_variables() → Set[V][source]

Calculate the free variables of this Term.

Returns: variables not bound by an abstraction

is_beta_normal_form() → bool[source]

Check if this Term is in beta-normal form.

Returns: if no beta reductions can be performed

alpha_conversion(new: V) → Abstraction[V][source]

Rename the bound variable

Parameters: new – new variable to bind
Raises: errors.CollisionError – If the new variable is a free variable
Returns: new term

eta_reduction() → Term[V][source]

Remove a useless abstraction.

Raises: ValueError – If abstraction is not useless
Returns: new term

accept(visitor: Visitor[T, V]) → T[source]

Accept a visitor by calling visitors.Visitor.visit_abstraction.

Parameters: visitor – Visitor to accept
Returns: value returned by visitors.Visitor.visit_abstraction

replace(*, bound: Optional[V] = None, body: Optional[Term[V]] = None) → Abstraction[V][source]

Return a copy with specific attributes replaced.

Parameters

bound – new value for bound variable, defaults to current
body – new value for body, defaults to current

Returns

new term

final class lambda_calculus.terms.Application(abstraction: Term[V], argument: Term[V])[source]

Bases: Term[V]

Term consisting of an application.

Parameters

abstraction – abstraction to be applied
argument – argument which to apply the abstraction to

classmethod with_arguments(abstraction: Term[V], arguments: Sequence[Term[V]]) → Application[V][source]

Create an Application applying the abstraction to multiple arguments.

Parameters

abstraction – abstraction to be applied
arguments – arguments which to apply the abstraction to, from first to last

Raises

ValueError – If no arguments are passed

Returns

requested Application term

__str__() → str[source]

Create a string representation.

Returns: ({abstraction} {argument})

free_variables() → Set[V][source]

Calculate the free variables of this Term.

Returns: variables not bound by an abstraction

bound_variables() → Set[V][source]

Calculate the free variables of this Term.

Returns: variables not bound by an abstraction

is_redex() → bool[source]

Check if this term can be reduced.

Returns: If a beta reduction can be performed

is_beta_normal_form() → bool[source]

Check if this Term is in beta-normal form.

Returns: if no beta reductions can be performed

beta_reduction() → Term[V][source]

Remove the abstraction.

Raises: ValueError – If this term can not be reduced
Returns: new term

accept(visitor: Visitor[T, V]) → T[source]

Accept a visitor by calling visitors.Visitor.visit_application.

Parameters: visitor – Visitor to accept
Returns: value returned by visitors.Visitor.visit_application

replace(*, abstraction: Optional[Term[V]] = None, argument: Optional[Term[V]] = None) → Application[V][source]

Return a copy with specific attributes replaced.

Parameters

abstraction – abstraction to be applied, defaults to current
argument – argument which to apply the abstraction to, defaults to current

Returns

new term