Module unsafe

Substitutions which dont check if the substitutions are valid

final class lambda_calculus.visitors.substitution.unsafe.UnsafeSubstitution(variable: V, value: Term[V])[source]

Bases: DeferrableSubstitution[V]

Substitution which does not check if a free variable gets bound.

Parameters
  • variable – variable to substitute

  • value – value which should be substituted

classmethod from_substitution(variable: V, value: Term[V]) UnsafeSubstitution[V][source]

Create an instance from the substitution it should perform

Parameters
  • variable – variable to substitute

  • value – value which should be substituted

Returns

new instance

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

Visit a Variable term.

Parameters

variable – variable term to visit

Returns

variable term or value which should be substituted

defer_abstraction(abstraction: Abstraction[V]) tuple[lambda_calculus.terms.Abstraction[V], Optional[lambda_calculus.visitors.substitution.unsafe.UnsafeSubstitution[V]]][source]

Visit an Abstraction term.

Parameters

abstraction – abstraction term to visit

Returns

tuple containing the abstraction term and this visitor to be used for visiting its body if variable is not bound

defer_application(application: Application[V]) tuple[lambda_calculus.terms.Application[V], lambda_calculus.visitors.substitution.unsafe.UnsafeSubstitution[V], lambda_calculus.visitors.substitution.unsafe.UnsafeSubstitution[V]][source]

Visit an Application term.

Parameters

application – application term to visit

Returns

tuple containing the application term and this visitor to be used for visiting its abstraction and argument