unicode_fol_kit.eliminate_lambdas

unicode_fol_kit.eliminate_lambdas(node)[source]

Return a lambda-free node ready for the FOL export / normal-form pipeline.

The node is first beta-eta normalized, then residual applied-predicate and applied-symbol spines are folded back into Atom / Function calls. If any Lambda, Application, or LambdaVar still remains (a partially applied or stuck term — e.g. a free higher-order variable applied to arguments), a ValueError naming the leftover construct is raised.

Raises:
  • ReductionLimitError – if normalization does not terminate within limits.

  • ValueError – if the normalized node is not lambda-free.

Returns:

A lambda-free Node; the input is never mutated.

Parameters:

node (Node)

Return type:

Node