Function beta_reduce 

pub fn beta_reduce(expr: &ProofExpr) -> ProofExpr

Beta-reduce an expression to Weak Head Normal Form (WHNF).

Normalizes lambda applications and match expressions, enabling unification to work on structurally equivalent terms.

Reduction Rules

Redex	Reduction
(λx. body)(arg)	body[x := arg] (beta)
(fix f. body) (Ctor ...)	body[f := fix f. body] (Ctor ...) (fix unfolding)
match (Ctor args) { ... }	Selected arm with args substituted (iota)

Weak Head Normal Form

WHNF stops at the outermost constructor or lambda. It does not reduce under binders, making it efficient for unification purposes.

Termination

Fix unfolding only occurs when the argument is a constructor (Ctor), ensuring termination for well-typed terms.

Example

beta_reduce((λx. P(x))(Socrates))
→ P(Socrates)

beta_reduce(match Zero { Zero => True, Succ(k) => False })
→ True

See Also

• unify_exprs - Calls beta_reduce before comparing expressions
• certifier::certify - Uses normalized terms for kernel conversion