Yes, it's context-free. A formula is a tree, which can be traversed with a stack. As we traverse, we are evaluating four things:
- x = 0, y = 0;
- x = 0, y = 1;
- x = 1, y = 0;
- x = 1, y = 1.
In effect, we are evaluating four "substantiated formulas" in parallel. A substantiated formula is one with variables replaced by 0 or 1.
Let's get more precise and define the transition table. We assume that the formula is in pre-order, that is, operator before operands.
- The initial state:
- If the current symbol is "$\lnot$", push onto the stack the symbol "($\lnot$, operator, ?, ?, ?, ?)" and go to the initial state.
- If the current symbol is "$\to$", push onto the stack the symbol "($\to$, operator, ?, ?, ?, ?)" and go to the initial state.
- If the current symbol is "x", go to the (0, 0, 1, 1) state.
- If the current symbol is "y", go to the (0, 1, 0, 1) state.
- The (a, b, c, d) state:
- If the top symbol of the stack is "($\lnot$, operator, ?, ?, ?, ?)", pop the stack and go to the ($\lnot$a, $\lnot$b, $\lnot$c, $\lnot$d) state.
- If the top symbol of the stack is "($\to$, operator, ?, ?, ?, ?)", pop the stack, push "($\to$, first operand, a, b, c, d)", go to the initial state.
- If the top symbol of the stack is "($\to$, first operand, e, f, g, h)", pop the stack, go to the (e $\to$ a, f $\to$ b, g $\to$ c, h $\to$ d) state.
The (a, b, c, d) state is a template. There are actually 16 such states: the (0, 0, 0, 0) state, the (0, 0, 0, 1) state, the (0, 0, 1, 0) state, the (0, 0, 1, 1) state and so on.
Similarly, the third rule in the generic (a, b, c, d) state is a generic rule. There are 16 such rules, with (e, f, g, h) = (0, 0, 0, 0), (0, 0, 0, 1), and so forth.
The (1, 1, 1, 1) state has one extra rule:
- If the stack is empty, go to the accepting state.
OK, this program has a weak point as discussed in the second comment. Now let's define a perfect version.
Assume two things: 1) The formula is in pre-order, and 2) there is a pair of parenthesis around each sub-formula.
Now, the transition table:
- start:
- if read = (, go to operator.
- operator:
- if read = ~, push (~, ?, ?, ?, ?), go to start.
- if read = ->, push (->, ?, ?, ?, ?), go to start.
- if read = x, push (ret, 0, 0, 1, 1), go to eval.
- if read = y, push (ret, 0, 1, 0, 1), go to eval.
- eval:
- if read = ), let the top element be (ret, a, b, c, d), pop, go to (a, b, c, d).
- (a, b, c, d):
- if read = ) and top = (~, ?, ?, ?, ?), pop, go to (~a, ~b, ~c, ~d).
- if read = ) and top = (->, e, f, g, h), pop, go to (e -> a, f -> b, g -> c, h -> d).
- if read = ( and top = (->, ?, ?, ?, ?), pop, push (->, a, b, c, d), go to operator.
- (1, 1, 1, 1) has one extra rule:
- if the stack is empty, accept.