#+title: CS 3MI3 Tutorial
#+subtitle: Semantics Review
#+date: October 30

Possible midterm question:
*Given this language in BNF, provide a simple rewrite semantics.*

* Super Simple Arithmetical Language

  Expr ∷= Zero
        ∣ Succ Expr
        ∣ Expr + Expr
        ∣ True
        ∣ False
        ∣ If Expr Then Expr Else Expr

* Important Observations
  ⇨ No types!
    “True + Zero” is a valid expression
     We need types to avoid such silliness

     /Just because you can do it, doesn't mean you should do it./

  ⇨ No variables!
    This makes things super easy

  ⇨ No parenthesis and other ‘punctuation’
    *Why is this relevant?*
    Eliminate ambiguity!


* Write the BNF in Agda :Question:

#+BEGIN_SRC agda
{- Almost exactly as the informal BNF -}
data Expr : Set where
  {- Numbers -}
  Zero : Expr
  Succ : Expr → Expr
  _+_  : Expr → Expr → Expr
  {- Booleans -}
  True False : Expr
  If_Then_Else_ : Expr → Expr → Expr → Expr

{- Some may call this a “program” or a “term” of the language. -}
example : Expr
example = If True Then Zero Else Succ Zero

silly : Expr
silly = True + Succ Zero
#+END_SRC

* Reduction Semantics

  _A_ /reduction semantics/ is a relation “_⟶_” that is intended
  to capture how a computation is carried out by a machine.
  It takes /states/ to /states./

  In our super simple arithmetical language, a “state” is just
  an expression --such as ~Zero~ or ~True + False~. Some expressions
  cannot be reduced such as ~True + Zero~ and may be thought of as
  “crashing”. Other non-reducing terms are called “values”, which
  are ~Zero, True, False~.

  Reduction relations are an alternative to Turing Machines, automata,
  and λ-calculus.

  Here's how we compute:
  + Zero+ :: Zero   + y ⟶ y
  + Succ+ :: Succ x + y ⟶ Succ (x + y)
  + SuccCong :: Succ e ⟶ Succ e′ /provided/ e ⟶ e′

                E.g., 3 + 2 ⟶ 5
                and so Succ(3 + 2) ⟶ Succ 5

                The first two clauses do not cover this example:
                E.g., Succ (If ⋯) ⟶ Succ (⋯)

  + Important :: You almost always want “cong”ruence rules.

  + IfTrue  :: If True Then e Else d  ⟶ e
  + IfFalse :: If False Then e Else d  ⟶ d

  + PlusCong :: e₀ + e₁ ⟶ e₀′ + e₁′
                /provided/
                eᵢ ⟶ eᵢ′ for /any/ 𝒾

                ⇨ Notice we have not chosen a particular reduction scheme, in particular we are not reducing left-to-right; i.e., e₀
                before e₁; we are being “non-deterministic”.

  + IfCong  ::  If e₀ Then e₁ Else e₂  ⟶ If e₀′ Then e₁′ Else e₂′
               /provided/
               eᵢ ⟶ eᵢ′ for /any/ 𝒾

               ⇨ Notice that we may *non-determinsticly* reduce any subpart of a conditional!
               ⇨ This can be super dangerous! The rule is shown only for demonstration.
               ⇨ E.g.,
                          If 0 ≠ 0 then 1 ÷ 0 else 2
                      ⟶ If 0 ≠ 0 then *CRASH* else 2  ;; which is not cool!
* Do it in Agda :Question:

#+BEGIN_SRC Agda
infix 0 _⟶_

open import Data.Sum renaming (_⊎_ to _∨_)

{- incomplete -}
data _⟶_ : Expr → Expr → Set where
  Zero+ : {e : Expr}   → Zero + e ⟶ e
  Succ+ : {e₁ e₂ : Expr} → Succ e₁ + e₂ ⟶ Succ (e₁ + e₂)
  SuccCong : {e e′ : Expr} →  e ⟶ e′
                           → Succ e ⟶ Succ e′
  PlusCong₁ : {e₁ e₁′ e₂ : Expr}
            →  e₁ ⟶ e₁′
            → e₁ + e₂ ⟶ e₁′ + e₂
  PlusCong₂ : {e₁ e₂ e₂′ : Expr}
            → e₂ ⟶ e₂′
            → e₁ + e₂ ⟶ e₁ + e₂′
  IfTrue  : {e₂ e₃ : Expr}
            →  If True Then e₂ Else e₃ ⟶ e₂
  IfFalse  : {e₂ e₃ : Expr}
            →  If False Then e₂ Else e₃ ⟶ e₃
  IfCong₁   : {e₁ e₁′ e₂ e₃ : Expr}
             →  e₁ ⟶ e₁′
             →  If e₁ Then e₂ Else e₃ ⟶ If e₁′ Then e₂ Else e₃
             {- This is “safe”, we reduce condition first -}

{-
Our language does NOT have variables;
but the eᵢ above denote METAVARIABLES; i.e.,
they stand for arbitary EXPRessions.
-}


{- When we compute ‘example’, we obtain result ‘Zero’ -}
_ : example ⟶ Zero
_ = IfTrue

{- There is NO possible reduction of “silly”!

Harder than it looks in Agda; maybe hmwrk assignment.
-}

#+END_SRC