Module normalisation

Visitor for term normalisation

class lambda_calculus.visitors.normalisation.Conversion(value)

Bases: Enum

Conversion performed by normalisation

final class lambda_calculus.visitors.normalisation.BetaNormalisingVisitor

Bases: Visitor[Iterator[tuple[Conversion, Term[str]]], str]

Visitor which transforms a term into its beta normal form, yielding intermediate steps until it is reached

No steps are yielded if the term is already in its beta normal form.

Remember that some terms dont thave a beta normal form and can cause infinite recursion.

skip_intermediate(term: Term[str]) → Term[str]

Calculate the beta normal form directly.

Parameters

term – term which should be transformed into ist beta normal form

Returns

new term representing the beta normal form if it exists

visit_variable(variable: Variable[str]) → Iterator[tuple['Conversion', lambda_calculus.terms.Term[str]]]

Visit a Variable term.

Parameters

variable – variable term to visit

Returns

empty Iterator, variables are already in beta normal form

visit_abstraction(abstraction: Abstraction[str]) → Iterator[tuple['Conversion', lambda_calculus.terms.Term[str]]]

Visit an Abstraction term.

Parameters

abstraction – abstraction term to visit

Returns

Iterator yielding steps performed on its body

beta_reducation(abstraction: Abstraction[str], argument: Term[str]) → Generator[tuple['Conversion', lambda_calculus.terms.Term[str]], None, Term[str]]

Perform beta reduction of an application.

Parameters

• abstraction – abstraction of the application

• argument – argument of the application

Returns

Generator yielding steps and returning the reduced term

visit_application(application: Application[str]) → Iterator[tuple['Conversion', lambda_calculus.terms.Term[str]]]

Visit an Application term

The abstraction and argument are not automatically visited.

Parameters

application – application term to visit

Returns

steps for performing beta reduction if possible and performed on its result or abstraction and argument