# Reasonable definition of beta-equivalence in big-step semantics

Assume, an extension of the lambda calculus with terms $t$ and values $v$ is defined in big-step operational semantics with evaluation relation $t \Downarrow v$.

It is intuitive to assume that $\beta$-equivalence holds, e.g.

(λx. t) unit $\equiv_\beta$ t when x is not free in t

It is however unclear to me, how $\equiv_\beta$ can be precisely defined in such a setting: Obviously, there is no small-step relation $\rightarrow_\beta$ that can be used to express a single reduction step, since the evaluation relates terms and values.

On the other hand, beta-equivalent terms do not evaluate to syntactically equal terms (e.g. when comparing abstractions which already are values).

So how does one define this equivalence in such a case?

• Do you want to define beta equivalence in terms of the ⇓ judgement? I don't think this is how it is done. Just define beta equivalence directly. Also, is your system typed or untyped? – gardenhead Oct 11 '16 at 21:36
• That is precisely the problem: A classical reduction step is part of a small-step semantics. Hence, for the classical definition of beta-equivalence to mean something, it must be related to the big-step reduction. The system is type-agnostic (i.e. it is untyped but does not contain any rules that make it "untypable"). – choeger Oct 12 '16 at 6:50