Modeling tower of hanoi in linear logic

You can use linear logic to model Hanoi puzzle:

towers

Reciting the rules of hanoi:

  1. We can only move one disc at a time.
  2. Only the topmost discs can move.
  3. Larger disc must never be above smaller disc.

In this post I'm using the same syntax that's used in Wikipedia. Understanding linear logic is not necessary to follow this post though. I've added pictures to illustrate what is going on.

Model

To represent the structure of the puzzle in propositions, we can list pegs with topmost disc in them, and which disc is above what disc.

top(disc, index)
above(disc, disc)

These alone do not define the structure of the puzzle. Additionally we need to describe how the discs are stacked over each other in the peg.

peg(i:index) ≡ (∃a:disc. top(a,i) ⊗ discs(a))
discs(a:disc) ≡
  (∃b:disc. (above(a,b) ⊗ !(a<b) ⊗ discs(b)))
  ⊕ !(∀x:disc. x<a)

We have this recursively defined type that takes a proof that we can stack the specific discs. Each stack ends into a "floor" -disc, requiring the proof that any disc can be stacked above it.

To prove things about stack of discs defined this way, you need an induction rule.

ind_discs ≡ ∀C:(Discs->U).
  !(∀b:Discs. (C(b) -o C(∃a:disc. above(a,b) ⊗ !(a<b) ⊗ b)))
  -o C(!(∀x:disc. x<a))
  -o ∀d:Discs. C(d)

ind_discs

Actually this rule may be not suitable for constructing a rule described later. It's a similar rule though and I keep this in because it's belonging to the definition I gave earlier about discs.

In short it says that to prove something for any stack of discs, first prove that you can prove it if it has been proven for a stack with one less disc on it, then prove it for stack with no discs.

The structures mentioned on the lines 1,2 alone allow to describe the valid motions in the hanoi puzzle.

motion ≡ ∀a,b,c:disc.∀i,j:index.
  !(a<b) ⊗ top(a,i) ⊗ top(b,j) ⊗ above(a,c)
  ⊸ top(c,i) ⊗ top(a,j) ⊗ above(a,b)

If we lift a piece from a peg, we already know that it was smaller than the disc that was exposed. To solve the puzzle, we also need to know between pegs, which disc is larger than the other.

lt ≡ ∀a,b:disc. a ⊸ b ⊸ (!(a<b) ⊕ !(b<a)) ⊗ a ⊗ b

We need to be able to compare the two topmost discs and for that we need this kind of a lifted version of the comparisor.

top_lt ≡ ∀a,b:disc.∀i,j:index.
  top(a,i) ⊸ top(b,j)
  ⊸ (!(a<b) ⊕ !(b<a)) ⊗ top(a,i) ⊗ top(b,j)

The puzzle has been completely modeled now.

Working with the model

We may want to prove that given any three pegs, it can be transformed into some other peg configuration.

peg 0 ⊗ peg 1 ⊗ peg 2 ⊸ peg 0 ⊗ peg 1 ⊗ peg 2

To prove that the puzzle can be solved, we should prove that..

peg 0 ⊗ peg 1 ⊗ peg 2 ⊸ peg 0 ⊗ top(Ø, 1) ⊗ top(Ø, 2)

As a shorthand I denote the "disc larger than all other discs" with Ø. Main content would not change dramatically so I'm not doing that.

If you open up the whole proposition, you get:

(∀a:disc. ~top(a,0) ⅋ ~discs(a))
⅋ (∀b:disc. ~top(b,1) ⅋ ~discs(b))
⅋ (∀c:disc. ~top(c,2) ⅋ ~discs(c))
⅋ (∃d:disc. top(d,0) ⊗ discs(d))
  ⊗ top(Ø, 1)
  ⊗ top(Ø, 2)

Examining this for a while shows we don't have a simple way to solve it.

Movement of moving multiple pieces

So we know how to move one piece. What do we need in order to move two pieces?

∀a,b,c,d:disc.∀i,j:index.
  ~top(a,i) ⅋ ~top(c,j) ⅋ ~above(a,b) ⅋ ~above(b,d)
  ⅋ top(d,i) ⊗ top(a,j) ⊗ above(a,b) ⊗ above(b,c)

move_two

Lets do one motion. The result is.

∀a,b,c,d,e:disc.∀i,j,k:index.
  ~top(a,i) ⅋ ~top(c,j) ⅋ ~above(a,b) ⅋ ~above(b,d)
  ⅋ top(d,i) ⊗ top(b,j) ⊗ above(b,c) ⊗ !(a<b)
⊗ (top(a,k) ⊗ above(a,e) ⅋ ~top(e,k))

move_two

The peg k cannot be the first peg because we couldn't do the motion. We also got a requirement that the a must be smaller than b. Lets clean those out and add into the root of the proof.

!(a<b) ... ⊸  top(e,k) ...

∀a,b,c,d,e:disc.∀i,j,k:index.
  ~top(a,i) ⅋ ~top(c,j) ⅋ ~above(a,b) ⅋ ~above(b,d)
  ⅋ top(d,i) ⊗ top(b,j) ⊗ above(b,c) ⊗ (top(a,k) ⊗ above(a,e))

We must have moved the a to the third peg in order to achieve this.

!(a<e) ⊗ top(e,k) ... ⊸ ...

∀a,b,c,d,e:disc.∀i,j,k:index.
  ~top(c,j) ⅋ ~above(b,d)
  ⅋ top(d,i) ⊗ top(b,j) ⊗ above(b,c) ⊗ ~top(b,i)

And the b must have been moved to the second peg after that..

!(b<c) ... ⊸ ...

∀a,b,c,d,e:disc.∀i,j,k:index.
  ~top(c,j) ⅋ ~above(b,d)
  ⅋ top(b,i) ⊗ top(c,j) ⊗ above(b,d) ⊗ ~top(b,i)

Next the elimination...

∀a,b,c,d,e:disc.∀i,j,k:index.
  ~above(b,d)
  ⅋ top(b,i) ⊗ above(b,d) ⊗ ~top(b,i)

∀a,b,c,d,e:disc.∀i,j,k:index.
  top(b,i) ⊗ ~top(b,i)

∀a,b:disc.∀c,d,e:(disc ⊕ floor).∀i,j,k:index. 1

So now we have a proof that we can move two items if we have a third peg free. We also have some reasonable requirements for it to succeed.

∀a,b,c,d,e:disc.∀i,j,k:index.
  !(a<b) ⊗ !(a<e) ⊗ !(b<c) ⊗ 
  top(a,i) ⊗ top(c,j) ⊗ top(e,k) ⊗ above(a,b) ⊗ above(b,d)
  ⊸ top(d,i) ⊗ top(a,j) ⊗ top(e,k) ⊗ above(a,b) ⊗ above(b,c)

move_two

Notably, the topmost element on the little stack must be smaller than the topmost element in the third peg.

Using induction?

There are still things I would need to study in order to provide a certified program to the puzzle with linear logic. But I can informally present the outline of using the induction rule to prove that the hanoi puzzle can be solved.

To keep it simple, lets keep the other pegs empty and state the task is to move the stack from that peg into either of the other pegs.

We have to prove that we can move the whole stack of discs from one place to an another in the puzzle.

If the peg is empty, we have the end-state that we expected for.

Using the induction rule, next we assume that we already know how to move a stack with one item less in it.

We already know how to move a disc if we have only one disc in the stack. We can move other discs elsewhere from above it. We've already proven that we can move an empty stack elsewhere without a trouble. There's the peg around that we don't care about, so we can move the stuff above there, then move it back above the disc once we move it.

full_proof

This forms a proof that we can solve the tower puzzle.

There is one puzzling problem that the proof I present here is iterating into the opposite direction than what the induction rule is doing. The disrepancy could be solved by inverting how the stack is defined, or by providing an alternative view of a stack with its own induction rule. Something that we can do trivially as the definitions are just a way to reason over multiple propositions that follow some structure.

Conclusion and thoughs

The way quantifiers can be used as names for discs and then used to construct "facts" that we can modify only through few rules. I think it came quite naturally while working on this problem. They do the important job of constraining how we can move the puzzle pieces.

I learned how to write those inductive definitions from the homotopy type theory book. I don't understand the larger half of this book's contents though.

I wonder if coinduction can be captured in a similar manner, into a small definition?

Similar posts