Lambda2.agda

-- Normalization by evaluation for λ→2
-- Thorsten Altenkirch and Tarmo Uustalu (FLOPS
--
-- Agda translation by Oleg Grenrus
-- no proofs yet.

module Lambda2 where

open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
import Data.Nat.Properties as ℕ
open import Data.Bool using (Bool; true; false; if_then_else_; not; _∧_)
open import Data.List using (List; []; _∷_)
open import Data.Product using (_×_; _,_)
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning

data Ty : Set where
  bool : Ty
  _⇒_  : Ty → Ty → Ty

infixr 0 _⇒_

Ctx : Set
Ctx = List Ty

variable
  A B : Ty
  Γ Δ : Ctx

data Var (A : Ty) : Ctx → Set where
  vz : Var A (A ∷ Γ)
  vs : Var A Γ → Var A (B ∷ Γ)

data Term (Γ : Ctx) : Ty → Set where
  `true  : Term Γ bool
  `false : Term Γ bool
  `if    : Term Γ bool → Term Γ A → Term Γ A → Term Γ A
  `var   : Var A Γ → Term Γ A
  `app   : Term Γ (A ⇒ B) → Term Γ A → Term Γ B
  `lam   : Term (A ∷ Γ) B → Term Γ (A ⇒ B)

data Wk : Ctx → Ctx → Set where
  nil : Wk [] []
  keep : Wk Γ Δ → Wk (A ∷ Γ) (A ∷ Δ)
  skip : Wk Γ Δ → Wk Γ       (A ∷ Δ)

wkVar : Wk Γ Δ → Var A Γ → Var A Δ
wkVar (keep wk) vz      = vz
wkVar (keep wk) (vs x) = vs (wkVar wk x)
wkVar (skip wk) x      = vs (wkVar wk x)

wkTerm : Wk Γ Δ → Term Γ A → Term Δ A
wkTerm wk `true = `true
wkTerm wk `false = `false
wkTerm wk (`if t t₁ t₂) = `if (wkTerm wk t) (wkTerm wk t₁) (wkTerm wk t₂)
wkTerm wk (`var x) = `var (wkVar wk x)
wkTerm wk (`app t t₁) = `app (wkTerm wk t) (wkTerm wk t₁)
wkTerm wk (`lam t) = `lam (wkTerm (keep wk) t)

data NP (F : Ty → Set) : Ctx → Set where
  []  : NP F []
  _∷_ : F A → NP F Γ → NP F (A ∷ Γ)

lookup : ∀ {F : Ty → Set} → NP F Γ → Var A Γ → F A
lookup (x ∷ xs) vz     = x
lookup (x ∷ xs) (vs i) = lookup xs i


⟦_⟧ : Ty → Set
⟦ bool  ⟧ = Bool
⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧

eval : NP ⟦_⟧ Γ → Term Γ A → ⟦ A ⟧
eval γ `true = true
eval γ `false = false
eval γ (`if t s r) = if (eval γ t) then eval γ s else eval γ r
eval γ (`var x) = lookup γ x
eval γ (`app t t₁) = eval γ t (eval γ t₁)
eval γ (`lam t) = λ z → eval (z ∷ γ) t

data Tree (A : Set) : ℕ → Set where
  leaf   : A → Tree A 0
  choice : ∀ {n} → Tree A n → Tree A n → Tree A (suc n)

data Vec (A : Set) : ℕ → Set where
  [] : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

variable
  n m : ℕ
  X Y Z : Set

find : Vec Bool n → Tree Y n → Y
find []           (leaf x)       = x
find (true  ∷ xs) (choice t₁ t₂) = find xs t₁
find (false ∷ xs) (choice t₁ t₂) = find xs t₂

mapTree : ∀ {n} {A B : Set} → (A → B) → Tree A n → Tree B n
mapTree f (leaf x) = leaf (f x)
mapTree f (choice t₁ t₂) = choice (mapTree f t₁) (mapTree f t₂)

forTree : Tree X n → (X → Y) → Tree Y n
forTree t f = mapTree f t

bindTree : ∀ {n m} {A B : Set} → Tree A n → (A → Tree B m) → Tree B (n + m)
bindTree (leaf x) f = f x
bindTree (choice t₁ t₂) f = choice (bindTree t₁ f) (bindTree t₂ f)

mapVec : (X → Y) → Vec X n → Vec Y n
mapVec f [] = []
mapVec f (x ∷ xs) = f x ∷ mapVec f xs

_++_ : Vec X n → Vec X m → Vec X (n + m)
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

bindVec : Vec X n → (X → Vec Y m) → Vec Y (n * m)
bindVec [] f = []
bindVec (x ∷ xs) f = f x ++ bindVec xs f

forVec : Vec X n → (X → Y) → Vec Y n
forVec xs f = mapVec f xs

double : ℕ → ℕ
double n = n + n

exp2 : ℕ → ℕ
exp2 zero    = 1
exp2 (suc n) = double (exp2 n)

flatten : Tree X n → Vec X (exp2 n)
flatten (leaf x) = x ∷ []
flatten (choice t₁ t₂) = flatten t₁ ++ flatten t₂

choices : (A : Ty) → ℕ
choices bool = 1
choices (A ⇒ B) = exp2 (choices A) * (choices B)

mkEnum : ∀ {n m} → Vec (⟦ A ⟧ → Bool) n → Tree ⟦ B ⟧ m → Tree (⟦ A ⟧ → ⟦ B ⟧) (exp2 n * m)
mkEnum {m = m}  [] es =
  subst (Tree _) (sym (ℕ.+-identityʳ m))
  (mapTree (λ b a → b) es)
mkEnum {n = suc n} {m = m} (q ∷ qs) es = subst (Tree _) size rec
  where
  size : exp2 n * m + (exp2 n * m) ≡ double (exp2 n) * m
  size = begin
    exp2 n * m + exp2 n * m  ≡⟨ sym (ℕ.*-distribʳ-+ m (exp2 n) (exp2 n)) ⟩
    double (exp2 n) * m ∎

  rec = bindTree (mkEnum qs es) λ f₁ →
        forTree  (mkEnum qs es) λ f₂ →
        (λ x → if q x then f₁ x else f₂ x)

enum      : (A : Ty) → Tree ⟦ A ⟧ (choices A)
questions : (A : Ty) → Vec (⟦ A ⟧ → Bool) (choices A)

enum bool = choice (leaf true) (leaf false)
enum (A ⇒ B) = mkEnum (questions A) (enum B)

questions bool = (λ x → x) ∷ []
questions (A ⇒ B) =
  bindVec (flatten (enum A)) λ d →
  forVec (questions B) λ q →
  (λ f → q (f d))

data Nf (Γ : Ctx) : Ty → Set
data Ne (Γ : Ctx) : Ty → Set

data Nf Γ where
  trueₙ  : Nf Γ bool
  falseₙ : Nf Γ bool
  lamₙ   : Nf (A ∷ Γ) B → Nf Γ (A ⇒ B)
  neuₙ   : Ne Γ A → Nf Γ A

data Ne Γ where
  varₙ : Var A Γ → Ne Γ A
  appₙ : Ne Γ (A ⇒ B) → Nf Γ A → Ne Γ B
  ifₙ  : Ne Γ bool → Nf Γ A → Nf Γ A → Ne Γ A

mkEnum' : ∀ {n m} → Vec (Ne (A ∷ Γ) A → Ne (A ∷ Γ) bool) n → Tree (Nf (A ∷ Γ) B) m → Tree (Nf (A ∷ Γ) B) (exp2 n * m)
mkEnum' [] es = subst (Tree _) (sym (ℕ.+-identityʳ _)) es
mkEnum' {A = A} {Γ} {B} {n = suc n} {m} (q ∷ qs) es = subst (Tree _) size rec
  where
  size : exp2 n * m + (exp2 n * m) ≡ double (exp2 n) * m
  size = begin
    exp2 n * m + exp2 n * m  ≡⟨ sym (ℕ.*-distribʳ-+ m (exp2 n) (exp2 n)) ⟩
    double (exp2 n) * m ∎
    
  rec : Tree (Nf (A ∷ Γ) B) (exp2 n * m + exp2 n * m)
  rec = bindTree (mkEnum' qs es) λ f₁ →
        forTree  (mkEnum' qs es) λ f₂ →
        neuₙ (ifₙ (q (varₙ vz)) f₁ f₂)

enum' : (A : Ty) → Tree (Nf Γ A) (choices A)
questions' : (A : Ty) → Vec (Ne Γ A → Ne Γ bool) (choices A)

enum' bool = choice (leaf trueₙ) (leaf falseₙ)
enum' (A ⇒ B) = mapTree lamₙ (mkEnum' (questions' A) (enum' B))

questions' bool = (λ z → z) ∷ []
questions' (A ⇒ B) =
  bindVec (flatten (enum' A)) λ d →
  forVec (questions' B) λ q →
  λ f → q (appₙ f d)  

quot : (A : Ty) → ⟦ A ⟧ → Nf [] A
quot A x = find (mapVec (λ q → q x) (questions A)) (enum' A) 

demo : quot (bool ⇒ bool ⇒ bool) _∧_ ≡
  lamₙ (neuₙ (ifₙ (varₙ vz)
    (lamₙ (neuₙ (ifₙ (varₙ vz) trueₙ  falseₙ)))
    (lamₙ (neuₙ (ifₙ (varₙ vz) falseₙ falseₙ)))))
demo = refl