Boolean language.agda

-- The "Boolean" language from Types and Programming Languages, 3.5

-- Terms of the boolean language
data Term : Set where
  true false : Term
  if_then_else_ : Term → Term → Term → Term

-- A small-step semantics. Each constructor is a single reduction rule.
data _⟶_ : Term → Term → Set where
  e-IfTrue : ∀ {t₂ t₃} → if true then t₂ else t₃ ⟶ t₂
  e-IfFalse : ∀ {t₂ t₃} → if false then t₂ else t₃ ⟶ t₃
  e-If : ∀ {t₁ t₁′ t₂ t₃} → t₁ ⟶ t₁′ → if t₁ then t₂ else t₃ ⟶ if t₁′ then t₂ else t₃

-- Witness that a term can be reduced (a proof that a term is reducible)
data Reduction (t : Term) : Set where
  reduce : ∀ t′ → t ⟶ t′ → Reduction t

-- False
data ⊥ : Set where

-- Negate a proof by showing you can construct the impossible. Good luck.
¬_ : Set → Set
¬ a = a → ⊥

-- Terms are normal if there is no proof that they can be reduced
is-normal? : Term → Set
is-normal? t = ¬ (Reduction t)

-- true is normal because we cannot construct reduction from it. Notice that all of the ways we can construct _⟶_ have if_then_else_ on the left hand side.
true-is-normal : is-normal? true
true-is-normal (reduce b ()) -- () signifies impossible, that is - no one would be able to show a reduction exists.

-- Likewise for false.
false-is-normal : is-normal? false
false-is-normal (reduce b ())

-- A proof that any 'if' statement can be reduced - that is, if statements are not a normal form.
if-is-reducible : ∀ {t t₂ t₃} → Reduction (if t then t₂ else t₃)
if-is-reducible {true} {t₂} = reduce t₂ e-IfTrue
if-is-reducible {false} {_} {t₃} = reduce t₃ e-IfFalse
if-is-reducible {if t′ then t₄ else t₅} {_} {t₃} with if-is-reducible {t′} {t₄} {t₅}
if-is-reducible {if t′ then t₄ else t₅} {t₂} {t₃} | reduce t′₁ x = reduce (if t′₁ then t₂ else t₃) (e-If x)

-- The multi-step evaluation relation.
data _⟶*_ : Term → Term → Set where
  [] : ∀ {a} → a ⟶* a
  _::_ : ∀ {a b c} → a ⟶ b → b ⟶* c → a ⟶* c

-- Multi-step evaluations can be composed head-to-tail
_∘_ : ∀ {a b c} → a ⟶* b → b ⟶* c → a ⟶* c
[] ∘ b = b
(x :: a₁) ∘ b₂ = x :: (a₁ ∘ b₂)

-- Proofs that a term can be reduced to a normal form.
data Terminates (t : Term) : Set where
  termination : ∀ t′ -- The final normal form after reductions
                → t ⟶* t′ -- The multi-step reductions to get to the normal form
                → is-normal? t′ -- A proof that we do reach a normal form
                → Terminates t

-- If we can take multiple steps to reduce a term 'a' to a term 'b', then
-- we can also take multiple steps to reduce 'if a ...' to 'if b ...', by
-- lifting each step through e-If.
e-If* : ∀ {a b t₁ t₂} → a ⟶* b → if a then t₁ else t₂ ⟶* if b then t₁ else t₂
e-If* [] = []
e-If* (x :: a₁) = e-If x :: e-If* a₁

-- Reduce any term to its normal form
terminates : (t : Term) → Terminates t
terminates true = termination true [] true-is-normal
terminates false = termination false [] false-is-normal

-- If statements are reduced by first reducing the predicate to a boolean
terminates (if t then _ else _)   with terminates t

terminates (if t then t₁ else _)  | termination true _ _                with terminates t₁
terminates (if _ then _ else _)   | termination true reduce-predicate _ | termination t′ reduce-body is-normal = termination t′ (e-If* reduce-predicate ∘ (e-IfTrue :: reduce-body)) is-normal

terminates (if t then t₁ else t₂) | termination false _ _                with terminates t₂
terminates (if t then t₁ else t₂) | termination false reduce-predicate _ | termination t′ reduce-body x₁ = termination t′ (e-If* reduce-predicate ∘ (e-IfFalse :: reduce-body)) x₁

-- It is impossible for the predicate to reduce to anything other than a boolean, because termination contains a proof that it terminates to a normal form.
terminates (if t then t₁ else t₂) | termination (if tt then tt₁ else tt₂) x not-normal with not-normal if-is-reducible
... | ()