0
$\begingroup$

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$?

$\endgroup$
0
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$

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.