What are these questions in the PoplMark challenge asking?
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_{&lt;:}$: 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.