What are these questions in the PoplMark challenge asking?

Question

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?

Answer 1

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.