Axiomatizing stacks and queues using first-order logic

Question

In the textbook I'm using to prepare the logic exam says that first order logic may be used to implement axiomatize data structures. There is an example of that:

"Stack": uses a language that contains the predicates functions top, pop and push, and the constant nil (empty stack). It axioms are:

• $\forall s \forall x . top(push(s, x))=x$
• $\forall s \forall x . pop(push(s, x))=s$
• $\forall s . push(pop(s), top(s))=s$

Premise: that I didn't understand this example completely (there's no explanation about how can these axioms describe a stack).

Suppose I have to describe another data structure, for example a "Queue", what strategy do you follow to write the axioms of this data structure? Can you make an example of the axioms you would use?

EDIT: Using the @user21820 's answer as an example, I'm trying to answer my own question.

Strategy:

1. Describe the language used: $(Queue, add, remove, element, nil)$ where
   • $Queue$ is an unary predicate, $Queue(x)$ means $x \in Queue$;
   • $add$ is a binary function. $add(q, e), q \in Queue$ returns the queue with a new element at the end of the queue;
   • $remove$ is a binary function. $remove(q, e), q \in Queue$ returns the queue without the first element of the queue;
   • $element$ is a unary function that returns the first element of the queue.
   • $nil$ is a constant, means empty queue.
2. Describe the axioms you need (they might be wrong):
   • remove an element from a queue with one element return the empty queue;
   • remove an element from a queue return the queue without the first element;
   • add an element from the queue returns the queue with the element added;
   • element function returns the first element inserted;
3. Write the axioms:
   • $remove(add(nil, x)) = nil$
   • $\forall q \in Queue. \left(remove(add(q, x)) = ???\right)$
   • $???$
   • $???$

Answer 1

Here is an answer that applies if you do not allow the length function for stacks/queues.

Stacks

If you take away the axioms about the length of stacks, there are worlds that satisfy the axioms but have very weird behaviour. (I was writing a more detailed version of this section but lost the whole lot accidentally. I'm not going to rewrite it, sorry.)

In one world, $push([0,0],0) = nil$, and $pop(nil) = [0,0]$ and $top(nil) = 0$, and everything else is as usual. In another, every stack consists of finitely many items on top of $nil$, while $nil$ is actually an infinite stack of turtles all the way down, and of course $push(nil,) = pop(nil) = nil$. In a third, there are both finite stacks including $nil$ and infinite stacks that are eventually turtles all the way down, and the infinite turtle stack is not $nil$. If one varies the nature of the infinite stacks one can get interesting behaviour; it could be that every infinite stack is eventually an alternating stack $T$ of and at the bottom, such that $push(push(T,),) = T$ but still we have $push(s,x) \ne s$ for every stack $s$ and object $x$.

The best you can do if you do not have the length function is to add the following axioms:

$\forall s \in Stacks\ \forall x\ ( push(s,x) \ne nil )$.

$\forall s \in Stacks\ \forall x\ ( push(s,x) \ne s )$.

$\forall s \in Stacks\ \forall x,y\ ( push(push(s,x),y) \ne s )$.

... [generalize to all possible number of pushes] ...

At least this axiomatization allows you to prove or disprove every true sentence you can state over the original language. (If I'm not mistaken.)

It also prevents the weird worlds mentioned above, though there are other non-standard worlds that satisfy even this. One of them is as follows. Every stack is either a standard finite stack or a bi-directional infinite array with an index $p$ that is filled up to cell $p$ and is empty from cell $p+1$ onwards. Operations on the standard stacks are as usual. Operations on the non-standard stacks is done as if the filled cells form a stack with cell $p$ at the top, so pushing an item will fill cell $p+1$, while popping will erase cell $p$, and $p$ is incremented or decremented as appropriate. You can check that all the axioms are satisfied.

Queues

As with stacks, what you can axiomatize for queues is limited if you do not have a length function, but let's see what can be done.

First let's look at your attempt:

• remove(add(nil,x))=nil

  Invalid because you didn't specify $x$. The correct version is:

  $\forall x\ ( remove(add(nil,x)) = nil )$.

• ∀q∈Queue.(remove(add(q,x))=???)

  You probably realize that you can't determine what's left behind.

  Well for a non-empty queue the order of adding an item or removing the first does not matter.

• ???

  In first-order logic you cannot specify the output type of a function.

  Read and follow my example for stacks properly.

  You're also missing axioms specifying the first element of a queue.

[Try before looking below.]

$\forall q \in Queues\ \forall x\ ( add(q,x) \in Queues )$.

$\forall q \in Queues\ ( q \ne nil \to pop(q) \in Queues )$.

$nil \in Queues$.

$\forall x\ ( first(add(nil,x)) = x )$.

$\forall q \in Queues\ \forall x\ ( q \ne nil \to first(add(q,x)) = first(q) )$.

$\forall x\ ( remove(add(nil,x)) = nil )$.   [The one you thought of.]

$\forall q \in Queues\ \forall x\ ( q \ne nil \to remove(add(q,x)) = add(remove(q),x) )$.

$\forall q \in Queues\ \forall x\ ( add(q,x) \ne nil )$.

$\forall q \in Queues\ \forall x\ ( add(q,x) \ne q )$.

$\forall q \in Queues\ \forall x,y\ ( add(add(q,x),y) \ne q )$.

... [generalize to all possible number of adds] ...

$\forall q \in Queues\ ( q \ne nil \to remove(q) \ne q )$.

$\forall q \in Queues\ ( q \ne nil \land remove(q) \ne nil \to remove(remove(q)) \ne q )$.

... [generalize to all possible number of removes] ...

I think these axioms will allow you to prove any true sentence about queues in the given language. But they will not prevent a world with non-standard queues. Similar to the non-standard world at the end of the section about stacks, one can have a world where a non-standard queue is a queue with an infinite front and infinite back, each stored in an infinite array where the position of both the first and last items are tracked.

Answer 2

Firstly, $push,pop,top$ are not predicates but functions, otherwise your axioms are syntactically meaningless in first-order logic.

The axioms describe some guarantees of the stack interface:

1. The top of a stack is the last item pushed onto it.

2. Popping a stack after pushing an item onto it gives you the original stack.

3. Popping a stack and then pushing the original top item gives you the original stack.

It is actually not the case that these axioms are enough, nor are they actually correct. There are glaring issues:

• The quantifiers are not restricted, so the axiom governs $push(s,x)$ even when $s$ is not a stack. This is not technically a problem (garbage in, garbage out) but is a severe violation of type-safety.

• Worse still, what happens if the stack is empty? For the axioms to hold, you would need 'negative-height' stacks to exist. For instance $nil$ must have a top element and there must be a stack such that when you push $top(nil)$ onto it you get $nil$!

• Also, it's not possible to state or prove certain properties about stacks without adding more axioms. For example you can't state anything about the length of stacks.

A proper axiomatization of stacks would look something like: $\def\nn{\mathbb{N}}$

[Add function symbol $len$ to the language.]

[Add predicates $Stacks,\nn$ to the language.]

$\forall s \in Stacks\ \forall x\ ( push(s,x) \in Stacks )$.

$\forall s \in Stacks\ \forall x\ ( s \ne nil \to pop(s) \in Stacks )$.

$nil \in Stacks$.

$\forall s \in Stacks\ \forall x\ ( top(push(s,x)) = x )$.

$\forall s \in Stacks\ \forall x\ ( pop(push(s,x)) = s )$.

$\forall s \in Stacks\ ( s \ne nil \to push(pop(s),top(s)) = s )$.

$\forall s \in Stacks\ ( len(s) \in \nn )$.

$\forall s \in Stacks\ \forall x\ ( len(push(s,x)) = len(s)+1 )$.

$\forall s \in Stacks\ ( s \ne nil \to len(s) = len(pop(s))+1 )$.

$\forall s \in Stacks\ ( s = nil \to len(s) = 0 )$.

[Add all the standard axioms about the natural numbers $\nn$.]

Note that "$x \in P$" here can be understood to mean "$P(x)$", and likewise a restricted quantification "$\forall x \in P\ ( \cdots )$" can be taken as "$\forall x\ ( P(x) \to \cdots )$".