# Can well-formed formulas in predicate logic for a given signature be recognized in LOGSPACE?

I read that visibly pushdown languages are supposed to model the typical simple formal languages like XML better than deterministic context free languages. The visibly pushdown languages can be recognized in LOGSPACE. I wonder whether the well-formed formulas in predicate logic for a given signature are a visibly pushdown language, or can at least be recognized in LOGSPACE.

Here is a typical well-formed formula in predicate logic, for the given signature $(f(\cdot,\cdot), g(\cdot))$:

$\forall x (f(x,y)=z \land g(z)=x)$

A corresponding context free grammar would be

$P \to T=T$
$P \to (P \land P)$
$P \to (P \lor P)$
$P \to \lnot P$
$P \to \forall V P$
$P \to \exists V P$
$T \to V$

$V \to x$
$V \to y$
$V \to z$

$T \to f(T,T)$
$T \to g(T)$

Some people prefer to use reverse polish notation:

$xyfz=zgx=\land x\forall$

A corresponding context free grammar would be

$P \to TT=$
$P \to PP\land$
$P \to PP\lor$
$P \to P\lnot$
$P \to PV\forall$
$P \to PV\exists$
$T \to V$

$V \to x$
$V \to y$
$V \to z$

$T \to TTf$
$T \to Tg$

Because I have now written down two explicit grammars, let the question just be whether these two grammars generate visibly pushdown languages, or can at least be recognized in LOGSPACE.

• What do you think? Have you tried expressing these languages as visibly pushdown languages? – Yuval Filmus May 15 '15 at 23:25
• @YuvalFilmus The formula in reverse polish notation seems to be a visibly pushdown language. You push for the variables, pop for the binary function and the equality relation, and do nothing for the rest. The normal notation is less obvious to me. But I think it should be possible to transform it into RPN (or another suitable visibly pushdown language) in logarithmic space. Hence I think that the well-formed formulas should be recognizable in LOGSPACE, but then I should also be able to give a simple algorithm doing just that, but here I have problems. – Thomas Klimpel May 15 '15 at 23:58

The normal notation is indeed a visibly pushdown language, with $\Sigma_c=\{(\}$, $\Sigma_r=\{)\}$. When we encounter the symbol $($, then we push the number of still expected occurrences of of terms or proposition (and whether we expect terms or propositions) on the stack. When we encounter the symbol $)$, then we first check that exactly the expected number of terms or proposition occurred, then overwrite the counter by the value on the stack, and decrease it by one. The counter is finite, because its maximum value is the maximum arity of the signature, and zero is its minimal value, because we reject when the counter would become negative.