Package substitution

Visitors for variable substitution

class lambda_calculus.visitors.substitution.Substitution[source]

Bases: Visitor[terms.Term[V], V]

ABC for Visitors which replace a free Variable with another term.

Type Variables:

V: represents the type of variables used in terms

abstract visit_abstraction(abstraction: Abstraction[V]) → Abstraction[V][source]

Visit an Abstraction term

The body is not automatically visited.

abstract visit_application(application: Application[V]) → Application[V][source]

Visit an Application term

The abstraction and argument are not automatically visited.

abstract classmethod from_substitution(variable: V, value: Term[V]) → T[source]

Create an instance from the substitution it should perform

Parameters

Returns

new instance

class lambda_calculus.visitors.substitution.DeferrableSubstitution[source]

Bases: DeferrableVisitor[terms.Term[V], V], Substitution[V]

ABC for Substitutions which can be performed lazyly.

Visit an Abstraction term.

Parameters: abstraction – abstraction term to visit
Returns: tuple containing a new term instance with substitutions performed and a visitor to be used for visiting its body

Visit an Application term.

Parameters: application – application term to visit
Returns: tuple containing a new term instance with substitutions performed and visitors to be used for visiting its abstraction and argument

final visit_abstraction(abstraction: Abstraction[V]) → Abstraction[V][source]

Visit an Abstraction term

The body is visited after performing substitution.

final visit_application(application: Application[V]) → Application[V][source]

Visit an Application term

The abstraction and argument are visited after performing substitution.