Module checked

Substitutions checking if the substitutions are valid

final class lambda_calculus.visitors.substitution.checked.CheckedSubstitution(variable: V, value: Term[V], free_variables: Set[V])

Bases: Substitution[V]

Substitution which checks if a free variable gets bound.

Parameters

• variable – variable to substitute

• value – value which should be substituted

• free_variables – free variables which should not be bound

Raises

errors.CollisionError – If a free variable gets bound

classmethod from_substitution(variable: V, value: Term[V]) → CheckedSubstitution[V]

Create an instance from the substitution it should perform

Parameters

• variable – variable to substitute

• value – value which should be substituted

Returns

new instance with free_variables set to the free variables of value

bind_variable(name: V) → None

Mark a variable as bound.

Bound variables are not automatically unbound and can be bound multiple times.

Parameters

name – name of the variable

unbind_variable(name: V) → None

Mark a variable as not bound.

A variable needs to be unbound multiple times if it was bound multiple times.

Parameters

name – name of the variable

Raises

KeyError – If the variable is not bound

visit_variable(variable: Variable[V]) → Term[V]

Visit a Variable term.

Parameters

variable – variable term to visit

Raises

errors.CollisionError – If the substitution whould bind free variables

Returns

variable term or value which should be substituted

visit_abstraction(abstraction: Abstraction[V]) → Abstraction[V]

Visit an Abstraction term.

Parameters

abstraction – abstraction term to visit

Raises

errors.CollisionError – If a substitution in the body whould bind free variables

Returns

abstraction term or new term with substitutions performed

visit_application(application: Application[V]) → Application[V]

Visit an Application term.

Parameters

appliation – application term to visit

Raises

errors.CollisionError – If a substitution in the abstraction or argument whould bind free variables

Returns

new term with substitutions performed