Defining a predicate on the structure of a string I have the following homework question. (For a bit of context - the study unit is Formal Languages and Automata).


  Define the predicate $\mathrm{pre}(s,t)$ over $s, t\in\Sigma^*$ by induction on the structure of $s$ such that it satisfies the following conditions: 
  $$\mathrm{pre}(s,t) = \begin{cases}
\mathsf{true} &amp; \text{if there exists $s'\in\Sigma^*$ such that $s \mathbin{+\!\!+} s' = t$} \\
\mathsf{false} &amp; \text{otherwise}.
\end{cases}$$


Now I have considered two definitions so far. However they both assume things about the structure of $t$, and the way the question is worded implies that we can only assume things on the structure of $s$ (in a recursive way).

The definition is:
$$ \mathrm{pre}(\epsilon,t) := \mathsf{true}\\
   \mathrm{pre}(\alpha.s,\beta.t) := (\alpha = \beta) \wedge \mathrm{pre}(s,t),
$$
and the second, which avoids having $\beta.t$ in the argument:
$$ \mathrm{pre}(\epsilon,t) := \mathsf{true}\\
   \mathrm{pre}(\alpha.s,t) := (\alpha =\mathrm{head}(t)) \wedge \mathrm{pre}(s,\mathrm{tail}(t)),
$$
where I would then define $\mathrm{head}$ and $\mathrm{tail}$ in a recursive way on $\alpha.s\in\Sigma^*$ (so essentially, this does the same thing). 

Is there a way this can be done without assuming anything about the structure of $t$?
No, in the recursive case you need to take the first symbol out of $t$, so you need at that point to unfold the structure of $t$.

Note that, as in functional programming, the functions $head$ and $tail$ should be used with great care since they are not total: $head(\epsilon)$ and $tail(\epsilon)$ are undefined. Hence, remember to require $t\neq\epsilon$ every time you use $head(t)$ or $tail(t)$, and to handle the $\epsilon$ case elsewhere.

I would tend to use your first solution, which needs a similar fix.

$$
\begin{array}{l}
{\sf pre}(\epsilon,t):= \sf true \\
{\sf pre}(\alpha.s,\epsilon):=\sf false \\
{\sf pre}(\alpha.s,\beta.t):=(\alpha=\beta)\land {\sf pre}(s,t)
\end{array}
$$

In this way you are not assuming that the second argument is non empty. You are still assuming that it is a word, but that's needed.