module PLFA.Lambda where

open import Data.Bool using (T; not)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List using (List; _∷_; [])
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product -- using (∃-syntax; _×_)
open import Data.String using (String; _≟_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable using (⌊_⌋; False; toWitnessFalse)
open import Relation.Nullary.Negation using (¬?)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)












-- * -- Syntax of the Lambda Calculus
-- terms of the lambda calculus with natural numbers and recursion

{-

stated in BNF

L, M, N ::=

-- pure lambda calculus fragment

   ` x       -- variables
   ƛ x ⇒ M   -- lambda expression
   M · N     -- application

-- natural number fragment

   `zero     -- constant 0
   `suc M    -- successor 
   case L [zero⇒ M |suc x ⇒ N ] -- case analysis on natural number L

-- recursion

   μ x ⇒ M   -- recursive expression where x is recursively defined

-}

Id : Set
Id = String

data Term : Set where
  `_      : Id → Term           -- ` "x"
  ƛ_⇒_    : Id → Term → Term    --  ƛ "x" ⇒ M
  _·_     : Term → Term → Term  -- M · N
  `zero   : Term
  `suc_   : Term → Term         -- `suc M
  case_[zero⇒_|suc_⇒_] : Term → Term → Id → Term → Term -- case L [zero⇒ M |suc x ⇒ N ]
  μ_⇒_    : Id → Term → Term                            -- μ "x" ⇒ M





infix  5  ƛ_⇒_
infix  5  μ_⇒_
infixl 7  _·_
infix  8  `suc_
infix  9  `_

-- examples: two, plus

two : Term
two = `suc (`suc `zero)

plus : Term
plus = μ "+" ⇒ (ƛ "m" ⇒ (ƛ "n" ⇒
       case (` "m")
         [zero⇒ (` "n")
         |suc "m'" ⇒ (`suc (` "+" · ` "m'" · ` "n")) ]))

{-
  later:  plus · two · two  == 4
-}

-- example: Church numerals
-- in lambda calculus, it's not necessary to include natural numbers
-- because they can be defined/encoded (but inefficiently)

-- idea: represent the natural number n by a higher-order function
-- that applies its argument function n-times

-- twoᶜ ; plusᶜ ; sucᶜ

twoᶜ : Term
twoᶜ = ƛ "f" ⇒ (ƛ "x" ⇒ (` "f" · (` "f" · ` "x")))

zeroᶜ : Term
zeroᶜ = ƛ "f" ⇒ ƛ "x" ⇒ ` "x"

-- take two arguments (Church numerals) and return the result (as Church numeral)
plusᶜ : Term
plusᶜ = ƛ "m" ⇒ ƛ "n" ⇒
       ƛ "f" ⇒ ƛ "x" ⇒ (` "m" · ` "f") · (` "n" · ` "f" · ` "x")

-- applies "f" m+n times to "x"

-- convert a number in Church encoding into a natural number (constructed from zero and suc_)
-- to that end, we construct a function that we can pass as "f" to a Church numeral
sucᶜ : Term
sucᶜ = ƛ "x" ⇒ `suc ` "x"

-- bound variables, free variables, α equivalence

{-

f1 = ƛ "x" ⇒ ` "x"
f2 = ƛ "y" ⇒ ` "y"

ƛ "x" ... *binds* the variable "x"
` "x" ... *uses* a variable "x" refers to a particular binding above the use of the variable

f2 is a renaming of f1:
 the bound variable "x" is renamed to "y" and all the references to "x" are also renamed to "y"
this is called *α renaming*, and f1 and f2 are called *α equivalent*

free variables:
` "x"                           -- "x" occurs free in the term
` "y"                           --  "y" occurs free
` "x" · ` "y"                   -- "x" and "y" occur free
ƛ "x" ⇒ ` "x" · ` "y"           -- "y" occurs free, but "x" is bound
ƛ "y" ⇒ ƛ "x" ⇒ ` "x" · ` "y"   -- no free variables, but "x" and "y" are bound
α renaming "y" to "z":
ƛ "z" ⇒ ƛ "x" ⇒ ` "x" · ` "z"   -- no free variables, but "x" and "z" are bound

` "y" · (ƛ "y" ⇒ ` "y")         -- "y" occurs free and "y" is bound
ƛ "y" ⇒ ` "y" · (ƛ "y" ⇒ ` "y") -- "y" is bound (two times)
α renaming the outermost "y" to "z":
ƛ "z" ⇒ ` "z" · (ƛ "y" ⇒ ` "y") -- "z" and "y" are bound variables

ƛ "x" ⇒ ` "x" · ` "y"           -- "y" occurs free, but "x" is bound

* cannot α rename "y" because it is free
* cannot α rename "x" to "y"
   because in  ƛ "y" ⇒ ` "y" · ` "y"  the second ` "y" has been *captured* 
* but can α rename "x" to anything but "y", e.g., to "z"

ƛ "z" ⇒ ` "z" · ` "y"           -- "y" occurs free, but "z" is bound

-}

----------------------------------------------------------------------
-- end lecture one
----------------------------------------------------------------------

-- * -- Evaluation of Lambda Terms
-- Value : expected results of evaluation
-- here values are a subset of terms
-- defined by a predicate, ie, an indexed datatype

-- here: only closed terms are candidates for values
---     (we are only going to define evaluation for closed terms)

variable
  x y : Id
  L M N L′ M′ N′ : Term

data Value : Term → Set where

  V-ƛ : 
    Value (ƛ x ⇒ M)

  V-zero :
    Value `zero

  V-suc :
    Value M →
    ----------
    Value (`suc M)

-- substitution
infix 9 _[_:=_]

_[_:=_] : Term → Id → Term → Term

-- M [ x := L ]
-- substitute all free occurrences of x in M by L
-- assume that L is closed
-- (exercise: define a predicate closed : Term → Set)

(` y)     [ x := L ] with x ≟ y
... | yes x≡y = L
... | no  x≢y = ` y
(ƛ y ⇒ M) [ x := L ] with x ≟ y
... | yes x≡y = ƛ y ⇒ M
... | no  x≢y = ƛ y ⇒ M [ x := L ] -- exploiting that L is closed!
(M · N)   [ x := L ] = (M [ x := L ]) · (N [ x := L ])
`zero     [ x := L ] = `zero
(`suc M)  [ x := L ] = `suc (M [ x := L ])
case M [zero⇒ M₁ |suc y ⇒ M₂ ] [ x := L ] with x ≟ y
... | yes x≡y = case (M [ x := L ]) [zero⇒ (M₁ [ x := L ]) |suc y ⇒ M₂ ]
... | no  x≢y = case (M [ x := L ]) [zero⇒ (M₁ [ x := L ]) |suc y ⇒ M₂ [ x := L ] ]
(μ y ⇒ M) [ x := L ] with x ≟ y
... | yes x≡y = μ y ⇒ M
... | no  x≢y = μ y ⇒ M [ x := L ]

-- define evaluation in so-called "small-step operational semantics"
-- ==
-- define evlauation step-by-step
-- each step transforms just one place in a term
-- i.e. we get a sequece of intermediate results
-- and iterate single steps until we reach a value (if ever)

-- single-step reduction
infix 4 _—→_

data _—→_ : Term → Term → Set where

  β-ƛ :                         -- beta value reduction
                                -- left side: (beta) redex
    Value N →                   -- right side: reductum (generally)
    ------------------------------
    (ƛ x ⇒ M) · N —→ M [ x := N ]

  β-zero :

    case `zero [zero⇒ M |suc x ⇒ N ] —→ M

  β-suc :

    Value L →
    --------------------------------------------------
    case (`suc L) [zero⇒ M |suc x ⇒ N ] —→ N [ x := L ]

  β-μ :

    μ x ⇒ M —→ M [ x := μ x ⇒ M ]

  -- context rules

  ξ-·₁ :

    M —→ M′ →
    --------------------
    M · N —→ M′ · N

  ξ-·₂ :
    
    Value M → 
    N —→ N′ →
    --------------------
    M · N —→ M · N′

  ξ-suc :

    M —→ M′ →
    --------------------
    `suc M —→ `suc M′

  ξ-case :

    L —→ L′ →
    ---------------------------------------------------------------
    case L [zero⇒ M |suc x ⇒ N ] —→ case L′ [zero⇒ M |suc x ⇒ N ]

-- examples
plus-unrolled : Term
plus-unrolled = ƛ "m" ⇒ (ƛ "n" ⇒ 
            case (` "m") [zero⇒ (` "n")
                         |suc "m'" ⇒ (`suc (plus · ` "m'" · ` "n")) ])

_ : plus —→ plus-unrolled
_ = β-μ

_ : plus · two · two —→ (plus-unrolled · two) · two
_ = ξ-·₁ (ξ-·₁ β-μ)

----------------------------------------------------------------------
-- end lecture 2
----------------------------------------------------------------------


-- reflexive transitive closure
-- infix 2 _—↠_

data _—↠_ : Term → Term → Set where

  —↠-refl :
    M —↠ M

  —↠-step :
    M —→ N → 
    ----------
    M —↠ N

  —↠-trans :
    M —↠ N →
    N —↠ L →
    ----------
    M —↠ L

  {- alternative for step and trans
  —↠-step-trans :
    M —→ N →
    N —↠ L →
    ----------
    M —↠ L
  -}


-- properties: deterministic, diamond, confluence

values-dont-reduce : Value M → ¬ (M —→ N)
values-dont-reduce V-ƛ ()
values-dont-reduce V-zero ()
values-dont-reduce (V-suc val-m) (ξ-suc M->N) = values-dont-reduce val-m M->N

deterministic : M —→ N → M —→ L → N ≡ L
deterministic (β-ƛ x) (β-ƛ x₁) = refl
deterministic (β-ƛ value-N) (ξ-·₂ x₁ M->L) = ⊥-elim (values-dont-reduce value-N M->L)
deterministic β-zero β-zero = refl
deterministic (β-suc x) (β-suc x₁) = refl
deterministic (β-suc value-L) (ξ-case M->L) = ⊥-elim (values-dont-reduce (V-suc value-L) M->L)
deterministic β-μ β-μ = refl
deterministic (ξ-·₁ M->N) (ξ-·₁ M->L) rewrite deterministic M->N M->L = refl
deterministic (ξ-·₁ M->N) (ξ-·₂ value-M M->L) = ⊥-elim (values-dont-reduce value-M M->N)
deterministic (ξ-·₂ x M->N) (β-ƛ value-N) = ⊥-elim (values-dont-reduce value-N M->N)
deterministic (ξ-·₂ value-M M->N) (ξ-·₁ M->L) = ⊥-elim (values-dont-reduce value-M M->L)
deterministic (ξ-·₂ x M->N) (ξ-·₂ x₁ M->L) rewrite deterministic M->N M->L = refl
deterministic (ξ-suc M->N) (ξ-suc M->L) rewrite deterministic M->N M->L = refl
deterministic (ξ-case M->N) (β-suc value-L) = ⊥-elim (values-dont-reduce (V-suc value-L) M->N)
deterministic (ξ-case M->N) (ξ-case M->L) rewrite deterministic M->N M->L = refl

-- the diamond property is trivial (sic) for deterministic reduction systems
-- but it is non-trivial for nondeterministic systems
-- (we restricted the lambda calculus to be deterministic; the full calculus is nondeterministic)
diamond : M —→ N → M —→ L → ∃[ P ] ((N —↠ P) × (L —↠ P))
diamond m->n m->l rewrite deterministic m->n m->l = _ , —↠-refl , —↠-refl

{-# TERMINATING #-}
confluence : M —↠ N → M —↠ L → ∃[ P ] ((N —↠ P) × (L —↠ P))
confluence {M} —↠-refl —↠-refl = M , —↠-refl , —↠-refl
confluence {M}{N}{L} —↠-refl (—↠-step M->L) = L , (—↠-step M->L , —↠-refl)
confluence {M}{N}{L} —↠-refl M->L@(—↠-trans m->>l m->>l₁) = L , M->L , —↠-refl
confluence {M}{N}{L} M->N@(—↠-step x) —↠-refl = N , (—↠-refl , M->N)
confluence {M}{N}{L} (—↠-step M->N) (—↠-step M->L) = diamond M->N M->L
confluence {M}{N}{L} M->>N@(—↠-step M->N) (—↠-trans m->>l m->>l₁) 
  with confluence M->>N m->>l
... | P' , n->>p' , n1->>p' with confluence n1->>p' m->>l₁
... | P'' , p'->>p'' , l->>p'' = P'' , ((—↠-trans n->>p' p'->>p'') , l->>p'')
confluence {M}{N}{L} M->>N@(—↠-trans m->>n m->>n₁) —↠-refl = N , —↠-refl , M->>N
confluence (—↠-trans m->>n m->>n₁) M->>L@(—↠-step M->L)
  with confluence m->>n M->>L
... | P' , n1->>p' , l->>p' with confluence m->>n₁ n1->>p'
... | P'' , n->>p'' , p'->>p'' = P'' , (n->>p'' , (—↠-trans l->>p' p'->>p''))
confluence (—↠-trans m->>n m->>n₁) (—↠-trans m->>l m->>l₁)
  with confluence m->>n m->>l
... | P1 , n1->>p1 , n2->>p1
  with confluence m->>n₁ n1->>p1
... | PN , n->>pn , p1->>pn
  with confluence n2->>p1 m->>l₁
... | PL , p1->>pl , l->>pl
  with confluence p1->>pn p1->>pl
... | P , pn->>p , pl->>p = P , ((—↠-trans n->>pn pn->>p) , (—↠-trans l->>pl pl->>p))

-- * -- (Simple) Types of the Lambda Calculus

{-
idea of a type system:
define a syntax of "types" where each "type" corresponds to a particular form of value
in the best case, the form of value enables a certain class of β-reductions.

examples:
* the function type A ⇒ B is to describe terms that evaluate to a lambda expression
* the number type   `ℕ    is to describe terms that evaluate to `zero or `suc v (values)

initially, the "type" language is just syntax (with some intuition...)
then, connect types to terms using typing rules
that specify a relation between terms and types (still just a relation between syntactic objects)

finally, show that the intution plays out by proving that the typing relation is consistent with evaluation
-}

infixr 7 _⇒_

data Type : Set where
  _⇒_ : Type → Type → Type
  `ℕ  : Type

-- examples for terms

_ : Term
_ = `zero                       -- : `ℕ
_ = ƛ "x" ⇒ `zero               -- : `ℕ ⇒ `ℕ  or (`ℕ ⇒ `ℕ) ⇒ `ℕ
_ = ƛ "x" ⇒ ` "x"               -- : `ℕ ⇒ `ℕ or  (`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ)
_ = ` "x"                       -- type depends on the context of use

-- important observation:
-- type depends on the context (of use)
-- => typing relation also need to include a context that assigns variables to types

-- * -- contexts

infixl 5 _,_⦂_

data Context : Set where
  ∅ : Context
  _,_⦂_ : Context → Id → Type → Context

_ : Context
_ = ∅
_ = ∅ , "x" ⦂ `ℕ
_ = ∅ , "x" ⦂ `ℕ , "y" ⦂ `ℕ ⇒ `ℕ
_ = (∅ , "x" ⦂ `ℕ) , "y" ⦂ `ℕ ⇒ `ℕ


-- * -- the typing judgment
-- this is about defining the relation between Context, Term, and Type
-- written as Γ ⊢ M ⦂ A

variable
  Γ : Context
  A B : Type

-- auxiliary judgment
-- a relation to find a type assumption in the context
-- Γ ∋ x ⦂ A

infix 4 _∋_⦂_

data _∋_⦂_ : Context → Id → Type → Set where

  -- variable appears at top of context
  Z :
    Γ , x ⦂ A ∋ x ⦂ A

  -- variable appears somewhere deeper down
  S :
    x ≢ y →
    Γ ∋ x ⦂ A →
    --------------------
    Γ , y ⦂ B ∋ x ⦂ A

infix 4 _⊢_⦂_

data _⊢_⦂_ : Context → Term → Type → Set where

  var :
    Γ ∋ x ⦂ A →
    -----------
    Γ ⊢ ` x ⦂ A

  -- rules for functions

  ⇒-I :
    Γ , x ⦂ A ⊢ M ⦂ B →
    --------------------
    Γ ⊢ ƛ x ⇒ M ⦂ A ⇒ B

  ⇒-E :
    Γ ⊢ M ⦂ A ⇒ B →
    Γ ⊢ N ⦂ A →
    ----------------
    Γ ⊢ M · N ⦂ B

  -- rules for terms denoting numbers

  ℕ-I-zero :
    Γ ⊢ `zero ⦂ `ℕ

  ℕ-I-suc :
    Γ ⊢ M ⦂ `ℕ →
    --------------------
    Γ ⊢ `suc M ⦂ `ℕ

  ℕ-E-case :
    Γ ⊢ L ⦂ `ℕ →
    Γ ⊢ M ⦂ A →
    Γ , x ⦂ `ℕ ⊢ N ⦂ A →
    ----------------------------------------
    Γ ⊢ case L [zero⇒ M |suc x ⇒ N ] ⦂ A

  μ-E :
    Γ , x ⦂ A ⊢ M ⦂ A →
    --------------------
    Γ ⊢ μ x ⇒ M ⦂ A

----------------------------------------------------------------------
-- end lecture 3
----------------------------------------------------------------------

-- some typed expressions

⊢two : ∀ {Γ} → Γ ⊢ two ⦂ `ℕ
⊢two = ℕ-I-suc (ℕ-I-suc ℕ-I-zero)

⊢plus : ∅ ⊢ plus ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ
⊢plus = μ-E (⇒-I (⇒-I (ℕ-E-case (var (S (λ()) Z))
                                (var Z)
                                (ℕ-I-suc (⇒-E (⇒-E (var (S (λ()) (S (λ()) (S (λ()) Z)))) (var Z)) (var (S (λ()) Z)))))))

-- an untyped expression
⊬zero-fun : ¬ (∅ ⊢ `zero · `zero ⦂ A)
⊬zero-fun (⇒-E () ℕ-I-zero)

-- a lemma about lookup in the context
∋-injective : Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
∋-injective Z Z = refl
∋-injective Z (S x≢x x⦂B) = ⊥-elim (x≢x refl)
∋-injective (S x≢x x⦂A) Z = ⊥-elim (x≢x refl)
∋-injective (S x≢y x⦂A) (S x≢y' x⦂B) = ∋-injective x⦂A x⦂B