Created
October 18, 2022 21:04
-
-
Save phadej/bc21a4201ac5d10c082c1f0d21e75e73 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment