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?

  • 2
    $\begingroup$ 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? $\endgroup$ – gardenhead Oct 11 '16 at 21:36
  • $\begingroup$ 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"). $\endgroup$ – choeger Oct 12 '16 at 6:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.