2
$\begingroup$

I was reading the paper Mechanized Metatheory for the Masses: the PoplMark Challenge by Aydemir et al (PDF) and I found the following three questions on page 13 of the PDF a bit confusing.

Challenge 3: Testing and Animating with respect to semantics.

  1. Given $\mathrm{F}_{\texttt{<:}}$ terms $t$ and $t'$, decide whether $t\rightarrow t'$.

  2. Given $\mathrm{F}_{\texttt{<:}}$ terms $t$ and $t'$, decide whether $t \rightarrow^* t' \not\rightarrow$, where $\rightarrow^*$ is the reflexive-transitive closure of $\rightarrow$.

  3. Given an $\mathrm{F}_{\texttt{<:}}$ term $t$, find a term $t'$ such that $t\rightarrow t'$.

I think question (3) is saying reduce a term $t$ to $t'$ until which is no longer can be reduced (or become a value). What about question (1), are they just saying check the result if it is equal to some term $t'$? and question (2).

Could someone explain me their differences?

$\endgroup$
4
$\begingroup$

The reduction relation is beta reduction (for term and type variables) as defined in the description of Challenge 2B. It's a single reduction step, not repeated reduction until a value is reached.

(3) says to find a term $t'$ such that $t \to t'$ because if one exists, then there are infinitely many such terms in $F_{<:}$: all the terms in the same alpha equivalence class. Usually we say that beta reduction is deterministic, i.e. $t'$ is unique, but that's because we reason on alpha equivalence classes. PoplMark is concerned with the representation of variable binding, so here terms are a concrete representation where variable binding is treated explicitly. For example, in a nominal representation, $(\lambda \texttt{x}. \texttt{x}) (\lambda \texttt{x}. \texttt{x}) \to (\lambda \texttt{x}. \texttt{x})$, and $(\lambda \texttt{x}. \texttt{x}) (\lambda \texttt{x}. \texttt{x}) \to (\lambda \texttt{z}. \texttt{z})$; (3) allows finding any of these since they are all equally valid.

Similarly (1) asks to check whether $t'$ is a possible result of reducing $t$, not the result: the implementation of the reduction (item (3)) might find a different representative of the alpha equivalence class from the one submitted by the user.

Only (2) is about reducing to a value. It says so explicitly: $t$ reduces to $t'$ in any number of steps, and $t'$ cannot be reduced.

$\endgroup$
  • $\begingroup$ Thanks for your answer. Now I realized that I was confusing myself by thinking too much. :) $\endgroup$ – alim Jun 7 '16 at 5:01

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.