module bb2 where

-- Turing machines in Agda
--
-- 1. Turing machines as programs: the Busy Beaver champions for 2, 3, 4 states
-- 2. Non-termination as a proposition, and a proof that a machine never stops
--
-- Everything is defined from scratch: no library is needed.

------------------------------------------------------------------------
-- Basic data types
------------------------------------------------------------------------

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data List (A : Set) : Set where
  []   : List A
  _::_ : A → List A → List A

infixr 5 _::_

-- Dependent pairs (Σ-types); product and sum as special cases

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ

infixr 4 _,_

_×_ : Set → Set → Set
A × B = Σ A (λ _ → B)

infixr 4 _×_

data _+_ (A B : Set) : Set where
  inl : A → A + B
  inr : B → A + B

-- A few numbers, to bound the runs below

five : Nat
five = suc (suc (suc (suc (suc zero))))

ten : Nat
ten = suc (suc (suc (suc (suc five))))

twice : Nat → Nat
twice zero    = zero
twice (suc n) = suc (suc (twice n))

twenty : Nat
twenty = twice ten

big : Nat                       -- 320
big = twice (twice (twice (twice twenty)))

------------------------------------------------------------------------
-- Turing machines
------------------------------------------------------------------------

-- Symbols: zero = blank, one = mark
data Symbol : Set where
  zero one : Symbol

-- States, with a distinguished halting state
data State : Set where
  qA qB qC qD qHalt : State

-- Head movements
data Dir : Set where
  L R : Dir

-- The tape: the cells to the left of the head (nearest first), the cell
-- under the head, the cells to the right.  Only finitely many cells are
-- stored; the rest are blank.
record Tape : Set where
  constructor tape
  field
    left  : List Symbol
    head  : Symbol
    right : List Symbol

open Tape

move : Dir → Tape → Tape
move L (tape []        h r) = tape [] zero (h :: r)
move L (tape (l :: ls) h r) = tape ls l (h :: r)
move R (tape l h [])        = tape (h :: l) zero []
move R (tape l h (r :: rs)) = tape (h :: l) r rs

-- A machine is its transition function: from the current state and the
-- symbol under the head, give the new state, the symbol to write, and
-- where to move.
Transition : Set
Transition = State → Symbol → State × Symbol × Dir

-- One step of execution
step : Transition → State → Tape → State × Tape
step δ s t = go (δ s (head t))
  where
    go : State × Symbol × Dir → State × Tape
    go (s' , sym , d) = (s' , move d (tape (left t) sym (right t)))

-- Run for at most n steps, stopping early in the halting state.
-- This always terminates: n decreases at each call.
run : Nat → Transition → State → Tape → State × Tape
run zero    δ s t = (s , t)
run (suc n) δ s t = go (step δ s t)
  where
    go : State × Tape → State × Tape
    go (qHalt , t') = (qHalt , t')
    go (s'    , t') = run n δ s' t'

-- Start in qA on a blank tape
initialTape : Tape
initialTape = tape [] zero []

srun : Nat → Transition → State × Tape
srun n δ = run n δ qA initialTape

------------------------------------------------------------------------
-- The Busy Beaver champions
------------------------------------------------------------------------

-- BB(2) = 6 steps
bb2 : Transition
bb2 qA zero = (qB    , one , R)
bb2 qA one  = (qB    , one , L)
bb2 qB zero = (qA    , one , L)
bb2 qB one  = (qHalt , one , R)
bb2 q  s    = (qHalt , s   , R)      -- unused states

-- BB(3) = 21 steps
bb3 : Transition
bb3 qA zero = (qB    , one , R)
bb3 qA one  = (qC    , one , L)
bb3 qB zero = (qA    , one , L)
bb3 qB one  = (qB    , one , R)
bb3 qC zero = (qB    , one , L)
bb3 qC one  = (qHalt , one , R)
bb3 q  s    = (qHalt , s   , R)

-- BB(4) = 107 steps, leaves 13 marks on the tape (Brady 1983)
bb4 : Transition
bb4 qA zero = (qB    , one  , R)
bb4 qA one  = (qB    , one  , L)
bb4 qB zero = (qA    , one  , L)
bb4 qB one  = (qC    , zero , L)
bb4 qC zero = (qHalt , one  , R)
bb4 qC one  = (qD    , one  , L)
bb4 qD zero = (qD    , one  , R)
bb4 qD one  = (qA    , zero , R)
bb4 q  s    = (qHalt , s    , R)

-- Evaluate these with C-c C-n
runBB2 : State × Tape
runBB2 = srun big bb2

runBB3 : State × Tape
runBB3 = srun big bb3

runBB4 : State × Tape
runBB4 = srun big bb4

-- Exercise: write a function counting the number of steps until the machine
-- halts, and check that bb4 halts after 107 steps.

------------------------------------------------------------------------
-- Machines that never stop
------------------------------------------------------------------------

-- The simplest one: stay in qA and move right forever
forever : Transition
forever qA zero = (qA , zero , R)
forever q  s    = (q  , s    , R)

-- A slightly less trivial one: alternate between qA and qB
alternate : Transition
alternate qA s = (qB , one  , R)
alternate qB s = (qA , zero , R)
alternate q  s = (qHalt , s , R)

-- Running them just gives back a state and a tape; no amount of running
-- can show that a machine never stops.  For that we need a proof.
runForever : State × Tape
runForever = srun big forever

------------------------------------------------------------------------
-- Propositions as types
------------------------------------------------------------------------

-- The false proposition: no proof
data ⊥ : Set where

-- The true proposition: one proof
data ⊤ : Set where
  tt : ⊤

-- Negation: a proof of ¬ A is a function from proofs of A to proofs of ⊥
¬ : Set → Set
¬ A = A → ⊥

-- "The state s is the halting state", as a proposition depending on s
Stop : State → Set
Stop qHalt = ⊤
Stop _     = ⊥

-- "The state s is qA"
QA : State → Set
QA qA = ⊤
QA _  = ⊥

-- A state cannot be both qA and halting.  Proof by cases on the state;
-- in each case the proof is trivial once the types have computed.
QA-notStop : (s : State) → QA s → ¬ (Stop s)
QA-notStop qA    p h = h
QA-notStop qB    p h = p
QA-notStop qC    p h = p
QA-notStop qD    p h = p
QA-notStop qHalt p h = p

-- "The machine δ never stops": for every n, after n steps we are not halted
neverStop : Transition → Set
neverStop δ = (n : Nat) → ¬ (Stop (fst (srun n δ)))

-- "The machine δ stops": for some n, after n steps we are halted
willStop : Transition → Set
willStop δ = Σ Nat (λ n → Stop (fst (srun n δ)))

-- The machine `forever` stays in qA, whatever the tape to the left.
-- Proof by induction on n.  Note that the statement has to be generalised
-- to an arbitrary tape on the left, since each step adds one cell there.
staysInQA : (n : Nat) (l : List Symbol) → QA (fst (run n forever qA (tape l zero [])))
staysInQA zero    l = tt
staysInQA (suc n) l = staysInQA n (zero :: l)

theorem : neverStop forever
theorem n = QA-notStop (fst (srun n forever)) (staysInQA n [])

-- Exercise: prove  neverStop alternate.
-- Hint: define QB, and prove by induction that after n steps the machine is
-- in qA or in qB.

------------------------------------------------------------------------
-- What we cannot expect to prove
------------------------------------------------------------------------

-- For a given machine, deciding which of the two holds is the halting
-- problem.  So we do not expect to prove the following for all δ.
Halting : Transition → Set
Halting δ = neverStop δ + willStop δ

------------------------------------------------------------------------
-- Equality, and proofs by computation
------------------------------------------------------------------------

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

-- These are checked by the type checker itself: it runs the machine.
bb2-halts : fst runBB2 ≡ qHalt
bb2-halts = refl

bb4-halts : fst runBB4 ≡ qHalt
bb4-halts = refl

forever-runs : fst runForever ≡ qA
forever-runs = refl

--------------------------------------------------------------------------------
-- Follow-up exercises on this file:
--
-- 1. Prove that neverStop is logically equivalent to the negation of willStop.
--    What about the opposite direction: Is willStop the negation of neverStop?
--
-- 2. Refactor the code so that State does not contain qHalt,
--    but instead the Transition function is partial,
--
--       State → Symbol → Maybe (State × Symbol × Dir)
--
--    with the standard definition of Maybe:
--
--       data Maybe (A : Set) : Set where
--         nothing : Maybe A
--         just    : A → Maybe A
--
--    This refactoring may force you to adapt many of the definitions.
--
--    Try to make a judgement:
--    Is the refactored code more clear or the original one?
--
--------------------------------------------------------------------------------