# 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

Yes, well-formed formulas in predicate logic for a given signature be recognized in LOGSPACE, at least for the two notations (grammars) given in the question!

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.

The given RPN grammar is also a visibly pushdown language, because the maximum arity of the given signature doesn't exceed two. You push on the stack the variables, pop from the stack for the binary function, the quantifier and the equality relation, and do nothing for the rest. What we actually push on the stack is the type (empty, term, or proposition) of the top element of the "real RPN" stack, before the new element is pushed. Convince yourself that we can always know this type (variable is not a type here).

Also RNP formulas for signatures with higher arity can be recognized in LOGSPACE, because they can be converted in constant time and space to an equivalent signature that whose arity doesn't exceed two, by using a pair constructor.

• For the second element, we actually also have to add a marker that the stack will contain exactly one element after it is popped, i.e. that it is possible to accept then. – Thomas Klimpel May 20 '15 at 8:27