<p>Fix a first-order language <span class="math-container">$L_0$</span>, and let
<span class="math-container">$$L=\{f(\varphi)\mid \varphi \text{ is a well-formed formula of $L_0$}\},$$</span>
where <span class="math-container">$f(\varphi)$</span> is <em><span class="math-container">$\varphi$</span> with all occurrences of free variables underlined</em>.</p>
<p>For example, <span class="math-container">$L$</span> contains
<span class="math-container">$\forall x\forall y(x=y)$</span> and
<span class="math-container">$\forall y(\underline{x}=y)$</span>,
but not <span class="math-container">$\forall x\forall y(\underline{x}=y)$</span>.</p>
<blockquote>
<p>What is known (or can you prove) about <span class="math-container">$L$</span> being (not) context-free, or context-sensitive?</p>
</blockquote>
<p>Assume that the infinitely many variable symbols are encoded in unary in the form <span class="math-container">$v(1), v(11), v(111),\dots$</span> and there are only finitely many non-logical symbols in <span class="math-container">$L_0$</span>.</p>

CC BY-SA 4.0
2022-11-29T07:42:48.977Z
The language is easily seen to be computable in uniform $\mathrm{TC^0\subseteq L\subseteq NSPACE}[O(n)]=\mathrm{CSL}$.
Emil Jeřábek
CC BY-SA 4.0
2022-11-29T07:45:08.203Z
Can’t you prove it’s not context-free just by applying the pumping lemma to $\forall v(1^n)\,(v(1^n)=v(1^n))$ for large enough $n$?
Emil Jeřábek
CC BY-SA 4.0
2022-11-29T07:56:20.403Z
Is there a bounded number of variables? Or are they encoded (e.g. in binary)? In the first case it seems easy to derive a CFL by having a NT for each subset of variables representing the free variables, in the second case it seems you cannot have a CFL covering everything because a NT cannot "remember" which  variables are free… (this can be elaborated in a more detailed proof).
Louis
CC BY-SA 4.0
2022-11-29T08:39:59.843Z
@Louis See the last paragraph.
Emil Jeřábek
CC BY-SA 4.0
2022-11-29T12:00:43.990Z
Ah sorry. Then I agree with you about pumping. To extend you argument, take the formula ∀x,x=x, with x that has a big enough encoding, then pump in the middle of the last occurrence of x and you get ∀x, x=y with y marked as bound but it is not.
Louis
CC BY-SA 4.0
2022-11-29T16:24:25.587Z
@EmilJeřábek how do you get TC0? Threshold circuits useful for this?
Bjørn Kjos-Hanssen
CC BY-SA 4.0
2022-11-29T18:04:27.007Z
Basically, the most complicated thing you need in order to parse a formula is to be able to count brackets. This allows you to check that it is correctly bracketed, and to determine the ancestors of a given symbol in the parse tree, which in turn allows you to decide whether a given variable occurence is free or bound.
Emil Jeřábek
<context-free>
Context-free languages and free/bound variables
Bjørn Kjos-Hanssen
# Context-free languages and free/bound variables

(Asked by: username_0 on 2022-11-28)

Fix a first-order language $L\_0$, and let
$$L=\{f(\varphi)\mid \varphi \text{ is a well-formed formula of $L\_0$}\},$$
where $f(\varphi)$ is *$\varphi$ with all occurrences of free variables underlined*.

For example, $L$ contains
$\forall x\forall y(x=y)$ and
$\forall y(\underline{x}=y)$,
but not $\forall x\forall y(\underline{x}=y)$.

> What is known (or can you prove) about $L$ being (not) context-free, or context-sensitive?

Assume that the infinitely many variable symbols are encoded in unary in the form $v(1), v(11), v(111),\dots$ and there are only finitely many non-logical symbols in $L\_0$.

**Tags:** context-free

> **Comments:**
> **username_1**: The language is easily seen to be computable in uniform $\mathrm{TC^0\subseteq L\subseteq NSPACE}[O(n)]=\mathrm{CSL}$.  
> **username_1**: Can’t you prove it’s not context-free just by applying the pumping lemma to $\forall v(1^n)\,(v(1^n)=v(1^n))$ for large enough $n$?  
> **username_2**: Is there a bounded number of variables? Or are they encoded (e.g. in binary)? In the first case it seems easy to derive a CFL by having a NT for each subset of variables representing the free variables, in the second case it seems you cannot have a CFL covering everything because a NT cannot "remember" which  variables are free… (this can be elaborated in a more detailed proof).  
> **username_1**: @username_2 See the last paragraph.  
> **username_2**: Ah sorry. Then I agree with you about pumping. To extend you argument, take the formula ∀x,x=x, with x that has a big enough encoding, then pump in the middle of the last occurrence of x and you get ∀x, x=y with y marked as bound but it is not.  
> **username_0**: @EmilJeřábek how do you get TC0? Threshold circuits useful for this?  
> **username_1**: Basically, the most complicated thing you need in order to parse a formula is to be able to count brackets. This allows you to check that it is correctly bracketed, and to determine the ancestors of a given symbol in the parse tree, which in turn allows you to decide whether a given variable occurence is free or bound.  

---

## 0 answers

