unicode_fol_kit.beta_eta_normalize¶
- unicode_fol_kit.beta_eta_normalize(node)[source]¶
Reduce node to beta-eta normal form by alternating beta_reduce and eta_reduce.
The alternation loop is a genuine necessity: eta-reduction can expose fresh beta-redexes (e.g. eta-contracting a func position turns an Application into a beta-redex), so the combined loop must iterate to a fixpoint rather than running each pass exactly once.
Raises ReductionLimitError if beta_reduce internally exceeds BETA_REDUCTION_LIMIT steps, or if the alternation loop itself exceeds BETA_ETA_ROUND_LIMIT rounds (which only fires on pathological terms that are not strongly normalizing under beta-eta). Returns a new Node; the input is never mutated.