# 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} & \text{if there exists s'\in\Sigma^* such that s \mathbin{+\!\!+} s' = t} \\ \mathsf{false} & \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$?

## 1 Answer

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.