<p>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! </p>

<p>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 <i>proof</i> 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.</p>

<p>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 <a href="http://repository.upenn.edu/cgi/viewcontent.cgi?article=1523&amp;context=cis_reports" rel="nofollow">Hannan and Miller</a> or <a href="http://www.springerlink.com/content/ht7067y2hhpj905r/" rel="nofollow">Ager</a>, 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 <i>partial</i> 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.</p>

CC BY-SA 3.0
2012-08-01T06:48:47.670Z
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.
Neel Krishnaswami
CC BY-SA 3.0
2012-08-01T15:27:06.807Z
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!
cody
CC BY-SA 3.0
2012-08-02T05:55:12.787Z
@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.
Neel Krishnaswami
CC BY-SA 3.0
2012-07-31T12:10:08.110Z
2012-08-01T12:53:25.647Z
2012-08-01T12:53:25.647Z
Rob Simmons
<p>Two common ways of formulating operational semantics for programming languages based on lambda-calculus are <em>big-step</em> and <em>small-step</em> semantics. </p>

<ol>
<li>In a big step semantics, you give a relation $e \Downarrow v$ which directly relates an expression to the value it computes. </li>
<li>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$. </li>
</ol>

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

<p>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 <em>closed under expansion</em> if it satisfies the property that:
$$\forall e \in R, e' \in \mathrm{Exp}.\;e' \mapsto e \;\mathrm{implies}\; e' \in R$$</p>

<p>Likewise, a set $R$ is <em>closed under reduction</em> if if satisfies:</p>

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

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

CC BY-SA 3.0
2012-07-31T10:49:27.050Z
The definitions of being closed under expansion and closed under reduction depend only on the transitive closure - they are upper and lower sets (http://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?
Colin McQuillan
<pl.programming-languages><lambda-calculus><operational-semantics>
Characterizing closure under expansion/reduction for big-step semantics?
Neel Krishnaswami
# Characterizing closure under expansion/reduction for big-step semantics?

(Asked by: username_0 on 2012-07-31)

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?

**Tags:** pl.programming-languages, lambda-calculus, operational-semantics
> **Comments:**
> **username_1**: The definitions of being closed under expansion and closed under reduction depend only on the transitive closure - they are upper and lower sets (http://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?  

---

## 1 answers

### Answer by username_2 on 2012-07-31. Score: 5 | Accepted answer

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](http://repository.upenn.edu/cgi/viewcontent.cgi?article=1523&context=cis_reports) or [Ager](http://www.springerlink.com/content/ht7067y2hhpj905r/), 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.

> **Comments:**
> **username_0**: 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.  
> **username_3**: 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!  
> **username_0**: @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.  

---

