Module renaming

Substitutions performing automatic alpha conversion

class lambda_calculus.visitors.substitution.renaming.RenamingSubstitution[source]

Bases: DeferrableSubstitution[V]

ABC for Substitutions which rename bound variables if a free variable gets bound.

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

Prevent collisions by renaming bound variables.

Parameters: abstraction – abstraction term which could bind free variables
Returns: abstraction term which does not bind free variables

final trace() → TracingDecorator[V][source]

Create a new visitor which yields when an alpha conversion occurs.

Returns: new visitor wrapping this instance

final 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

final defer_abstraction(abstraction: Abstraction[V]) → tuple[lambda_calculus.terms.Abstraction[V], Optional[lambda_calculus.visitors.substitution.renaming.RenamingSubstitution[V]]][source]

Visit an Abstraction term.

Parameters: abstraction – abstraction term to visit
Returns: tuple containing an abstraction term not binding free variables and this visitor to be used for visiting its body if variable is not bound

final defer_application(application: Application[V]) → tuple[lambda_calculus.terms.Application[V], lambda_calculus.visitors.substitution.renaming.RenamingSubstitution[V], lambda_calculus.visitors.substitution.renaming.RenamingSubstitution[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

final class lambda_calculus.visitors.substitution.renaming.TracingDecorator(substitution: RenamingSubstitution[V])[source]

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

Visitor which transforms a RenamingSubstitution into an Generator which yields after performing an alpha conversion and returns the term with substitutions.

Parameters: substitution – instance to wrap

visit_variable(variable: Variable[V]) → Generator[Variable[V], None, Term[V]][source]

Visit a Variable term.

Parameters: variable – variable term to visit
Returns: empty Generator returning the result of RenamingSubstitution.visit_variable()

visit_abstraction(abstraction: Abstraction[V]) → Generator[Abstraction[V], None, Abstraction[V]][source]

Visit an Abstraction term

Parameters: abstraction – abstraction term to visit
Returns: Generator yielding alpha conversions and returning the term with substitutions

visit_application(application: Application[V]) → Generator[Application[V], None, Application[V]][source]

Visit an Application term

Parameters: appliation – application term to visit
Returns: Generator yielding alpha conversions and returning the term with substitutions

final class lambda_calculus.visitors.substitution.renaming.CountingSubstitution(variable: str, value: Term[str], free_variables: Set[str])[source]

Bases: RenamingSubstitution[str]

Substitution which renames bound variables if a free variable gets bound by appending a number.

Parameters

variable – variable to substitute
value – value which should be substituted
free_variables – free variables which should not be bound

classmethod from_substitution(variable: str, value: Term[str]) → CountingSubstitution[source]

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

prevent_collision(abstraction: Abstraction[str]) → Abstraction[str][source]

Prevent collisions by appending a number.

Parameters: abstraction – abstraction term which could bind free variables
Returns: abstraction term which does not bind free variables