5
$\begingroup$

Two common ways of formulating operational semantics for programming languages based on lambda-calculus are big-step and small-step semantics.

  1. In a big step semantics, you give a relation $e \Downarrow v$ which directly relates an expression to the value it computes.
  2. In a small-step semantics, you give a transition relation $e \mapsto e'$ which does one step of evaluation, and you get to a value by iterating the transition relation. $e \mapsto^{*} v$.

These two relations are equivalent, in the sense that $e \Downarrow v$ if and only if $e \mapsto^{*} v$.

However, some things are easier to define one way or another. For example, we can say that a set of terms $R \subseteq \mathrm{Exp}$ is closed under expansion if it satisfies the property that: $$\forall e \in R, e' \in \mathrm{Exp}.\;e' \mapsto e \;\mathrm{implies}\; e' \in R$$

Likewise, a set $R$ is closed under reduction if if satisfies:

$$\forall e \in R, e' \in \mathrm{Exp}.\;e \mapsto e' \;\mathrm{implies}\; e' \in R$$

It's not immediately obvious to me how to formulate expansion or contraction in terms of a big-step semantics. Does anyone know how?

$\endgroup$
  • $\begingroup$ The definitions of being closed under expansion and closed under reduction depend only on the transitive closure - they are upper and lower sets (en.wikipedia.org/wiki/Upper_set) for the preorder generated by $\mapsto$ (i.e. the reflexive transitive closure). But your description of $\Downarrow$ doesn't quite sound like the transitive closure: if $a\mapsto b\mapsto c$, does $a\Downarrow b $ hold? $\endgroup$ – Colin McQuillan Jul 31 '12 at 10:49
5
$\begingroup$

The notion of "next" and "last" - prior to the idea of "expansion" and "reduction" - are essentially lost when we read a big-step operational semantics as an inductive definition, which is too bad because the way we usually prove things about big-step operational semantics is by reading it as an inductive definition!

You can prove a "full expansion" property (big step preservation) that $e \Downarrow v$ and $e \in R$ imply $v \in R$, and then observe that the proof of this property actually proves a small-step expansion property. This is because computational structure of the proof actually recovers the small-step evaluation process that Prolog/Twelf would use to execute the big-step semantics as a logic program! But for appropriately tricky semantics (especially non-deterministic ones), I've noticed it's frequently the case that you can prove a big-step property when it doesn't hold for the small-step evaluation process that Prolog/Twelf proof proof search would imply.

In my view, the best option - if we want to use big-step specifications but recover the information that was lost when we treated the big-step semantics as inductive definition - to characterize the small-step evaluation process that Prolog/Twelf would use. (This ends up basically or exactly being an abstract machine semantics.) This may not be satisfying depending on what it is you're trying to do, of course. There are a couple of versions of this: see Hannan and Miller or Ager, for instance. (There's also a bit about this in my thesis, some work I did with Ian Zerny, but I'll link to that when there's a thing to link to.) You could also carefully characterize a set of partial derivations of $e_1 \Downarrow v_1, \ldots, e_n \Downarrow v_n \vdash e \Downarrow v$ that corresponded to partial executions, but when I've contemplated this the details have seemed fraught enough that the abstract machine interpretation seems like a safer bet.

$\endgroup$
  • $\begingroup$ Thanks! I am switching a system from big-step to small-step so I can close a set up under expansion, and was curious if there was something obvious I had overlooked that would let me talk expansion using big-step semantics. $\endgroup$ – Neel Krishnaswami Aug 1 '12 at 6:48
  • $\begingroup$ I wonder if this is related to the fact that termination is not a natural property to express using big-step semantics: stability of normalization by head-expansion is a crucial step in the normalization proof! $\endgroup$ – cody Aug 1 '12 at 15:27
  • 1
    $\begingroup$ @cody: You actually put your finger on exactly what I was doing! I had been proving termination for a language, and started with a big-step semantics on the grounds that at the end of the day everything terminate. So I did a logical relations proof using value and expressions (kind of in monadic style). This worked, but when I tried to unify the value and expression relations (since it's weird to introduce the distinction when everything terminates), I found I needed stability under head-expansion. $\endgroup$ – Neel Krishnaswami Aug 2 '12 at 5:55

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.