nat-semantics.agda

open import Data.Nat
open import Data.Bool hiding (_<_)
open import Data.List
open import Data.Fin hiding (_<_; _+_)
open import Data.Unit
open import Relation.Nullary
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- What is a semantics? A semantics defines the meaning of terms.
-- So how do we define the meaning of terms?
-- Well, what is a term?

-- A language of arithmetic expressions over Nats
data Type : Set where
  -- object-language Nat
  oNat : Type

-- Represent vars as de Bruijn indexes
Env = List Type
Var = ℕ

-- We only work with well-bound Vars
well-bound : Env -> Var -> Set
well-bound Γ n = (n < (length Γ))
env-lookup : (Γ : Env) -> {n : Var} -> (well-bound Γ n) -> Type
env-lookup Γ p = lookup Γ (fromℕ< p)

-- Raw syntax of terms
data Term : Set where
  -- variables
  var : Var -> Term
  -- natural number literals
  lit : ℕ -> Term
  -- addition
  add : Term -> Term -> Term
  -- multiplication
  mul : Term -> Term -> Term

-- Well typed terms.
-- Here, the only thing we're really checking is well-bounded ness.

data _⊢_::_ : Env -> Term -> Type -> Set where
  Rule-Var : ∀ {Γ n A} ->
    (x : (well-bound Γ n)) ->
    (A ≡ (env-lookup Γ x)) ->
    ------------------------
    Γ ⊢ (var n) :: A

  Rule-Nat : ∀ {Γ} ->
    (n : ℕ) ->
    -------------------
    Γ ⊢ (lit n) :: oNat

  Rule-Add : ∀ {Γ e1 e2} ->
    Γ ⊢ e1 :: oNat ->
    Γ ⊢ e2 :: oNat ->
    -------------------
    Γ ⊢ (add e1 e2) :: oNat

  Rule-Mul : ∀ {Γ e1 e2} ->
    Γ ⊢ e1 :: oNat ->
    Γ ⊢ e2 :: oNat ->
    -------------------
    Γ ⊢ (mul e1 e2) :: oNat

module test-types where
  example1 : [] ⊢ (lit 0) :: oNat
  -- Our rules are kind of like smart constructors, constructing well-typed terms.
  -- This definition can be solved by C-c C-a
  example1 = Rule-Nat 0

  example2 : [] ⊢ (add (lit 1) (lit 0)) :: oNat
  -- This definition can be solved by C-c C-a
  example2 = Rule-Add (Rule-Nat 1) (Rule-Nat 0)

-- Let's define a semantics, i.e. a meaning of terms, via a model.
-- We model expressions as Agda Nats.
-- A model is an interpretation of the language the preserves relationships.
module model1 where
  -- The interpretation of a Type is.. it's Agda type
  -- If we can complete this semantics, everything must be terminating, by
  -- construction, since Agda is.
  T⟦_⟧ : Type -> Set
  T⟦ oNat ⟧ = ℕ

  -- Interpretation of environments are substitutions
  G⟦_⟧ : Env -> Set
  G⟦ [] ⟧ = ⊤
  G⟦ A ∷ Γ ⟧ = (T⟦ A ⟧) × G⟦ Γ ⟧

  -- Applying a substitution to a well-bound Var produces a semantic value.
  -- this was mostly automatically generated.
  apply : ∀ {Γ : Env} -> G⟦ Γ ⟧ -> {n : Var} -> (x : well-bound Γ n) -> T⟦(env-lookup Γ x) ⟧
  -- EXERCISE 1: Try deleting the definition it and redoing it from the stub below:
  -- apply = ?
  apply {A ∷ Γ} ρ {zero} p = proj₁ ρ
  apply {A ∷ Γ} ρ {suc n} (s≤s p) = apply (proj₂ ρ) p

  -- Interpretation of typing derivation, i.e., well-typed terms.
  -- Any well-typed term has a well-typed semantic term, which terminates
  ⟦_⟧ : ∀ {Γ e A} -> Γ ⊢ e :: A -> G⟦ Γ ⟧ -> T⟦ A ⟧
  -- ⟦ D ⟧ ρ = ?
  ⟦ Rule-Var x p ⟧ ρ rewrite p = apply ρ x
  ⟦ Rule-Nat n ⟧ ρ = n
  ⟦ Rule-Add D D₁ ⟧ ρ = (⟦ D ⟧ ρ) + (⟦ D₁ ⟧ ρ)
  ⟦ Rule-Mul D D₁ ⟧ ρ = (⟦ D ⟧ ρ) * (⟦ D₁ ⟧ ρ)

-- The above is a model of the language so far.
-- All elements of the language (types, environments, (well-typed) terms) have
-- interpretations, and the original relationships between those things are
-- preserved.
-- The definition ⟦_⟧ is a also proof that the construction is a model.

-- QUESTION 1: Could we formalize/mechanize what it means to be a model of the
-- above language?

-- We can use this model to reason about equivalence:
module test-model1 where
  open model1
  example1 : ⟦ test-types.example1 ⟧ tt ≡ ⟦ test-types.example1 ⟧ tt
  example1 = refl

  example2 : ⟦ Rule-Add (Rule-Nat 0) (Rule-Nat 1) ⟧ tt ≡ ⟦ Rule-Nat 1 ⟧ tt
  example2 = refl

  -- And inequivalence
  example3 : ¬ (⟦ Rule-Add (Rule-Nat 0) (Rule-Nat 1) ⟧ tt ≡ ⟦ Rule-Nat 2 ⟧ tt)
  example3 ()

-- What does this model tell us about the language?

-- Well, it implies the the type system is consistent (if Agda is), since all
-- well-typed derivations are translated to Agda derivations.
-- It implies that for every expression, there exists a value (termination)...
-- in the model.

-- This isn't *quite* the termination proof we might expect.
-- It states that *in this model* all terms terminate.
-- We haven't shown that the model preserves any useful operational things such
-- as equivalence, or reduction, since we haven't even specified reduction.
-- So let's do that, and extend the model with a proof that equivalence is
-- preserved, which is required to still be considered a model.

-- Some equations I want to be true:
data _==_ : Term -> Term -> Set where
  =Refl : ∀ {e} ->
    ------
    e == e

  =Add0 : ∀ {e} ->
    --------------
    (add (lit 0) e) == e

  =AddS : ∀ {e n} ->
    --------------
    (add (lit (suc n)) e) == (add (lit n) (add (lit 1) e))

  =Mul0 : ∀ {e} ->
    --------------
    (mul (lit 0) e) == (lit 0)

  =Mul1 : ∀ {e} ->
    --------------
    (mul (lit 1) e) == e

-- Might avoid this by defining equivalence on typed terms (typing derivations).
open model1
open import Data.Nat.Properties

-- Seems to be necessary since well-bound is not a Prop
-- Uniqueness of well-bound proofs
UWBP : ∀ {Γ n} -> (p1 p2 : (well-bound Γ n)) -> p1 ≡ p2
UWBP {x ∷ Γ} {n = zero} (s≤s z≤n) (s≤s z≤n) = refl
UWBP {x ∷ Γ} {n = suc n} (s≤s p1) (s≤s p2) with (UWBP {Γ} {n} p1 p2)
... | p = cong s≤s p

coherence : ∀ {e1 Γ A} -> (D1 : (Γ ⊢ e1 :: A)) -> (D2 : (Γ ⊢ e1 :: A)) -> D1 ≡ D2
coherence {var x} {Γ} {.(env-lookup Γ bound)} (Rule-Var {.Γ} {.x} bound refl) (Rule-Var x₁ p) rewrite (UWBP {Γ} {x} bound x₁) with p
... | refl = refl
coherence {lit x} (Rule-Nat .x) (Rule-Nat .x) = refl
coherence {add e e₁} (Rule-Add D1 D3) (Rule-Add D2 D4) rewrite (coherence D1 D2) | (coherence D3 D4) = refl
coherence {mul e e₁} (Rule-Mul D1 D3) (Rule-Mul D2 D4) rewrite (coherence D1 D2) | (coherence D3 D4) = refl

soundness : ∀ {e1 e2 A Γ} -> (D1 : (Γ ⊢ e1 :: A)) -> (D2 : (Γ ⊢ e2 :: A))
       -> e1 == e2
       -> (ρ : G⟦ Γ ⟧)
       -> (⟦ D1 ⟧ ρ ≡ ⟦ D2 ⟧ ρ)
soundness D1 D2 =Refl ρ rewrite (coherence D1 D2) = refl
soundness (Rule-Add (Rule-Nat .0) D3) D2 =Add0 ρ = soundness D3 D2 =Refl ρ
soundness (Rule-Add (Rule-Nat .(suc n)) D4) (Rule-Add (Rule-Nat n) (Rule-Add (Rule-Nat .1) D5)) =AddS ρ rewrite (coherence D4 D5) = (sym (+-suc n (⟦ D5 ⟧ ρ)))
soundness (Rule-Mul (Rule-Nat .0) D3) (Rule-Nat .0) =Mul0 ρ = refl
soundness (Rule-Mul (Rule-Nat .1) D3) D2 =Mul1 ρ rewrite (coherence D2 D3) rewrite +-comm (⟦ D3 ⟧ ρ) 0 = refl

-- Completeness doesn't hold.
incompleteness : ¬ (∀ {e1 e2 A Γ} -> (D1 : (Γ ⊢ e1 :: A)) -> (D2 : (Γ ⊢ e2 :: A))
               -> (ρ : G⟦ Γ ⟧)
               -> (⟦ D1 ⟧ ρ ≡ ⟦ D2 ⟧ ρ)
               -> (e1 == e2))
incompleteness H with (H {var 0} {lit 0} {Γ = (oNat ∷ [])} (Rule-Var (s≤s z≤n) refl) (Rule-Nat 0) (0 , tt) refl)
... | ()