Brendan Hart 2019-2020

We define PCF types and terms, substitution as in PLFA, and the big step semantics.

https://plfa.github.io/

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import UF.PropTrunc

module PCF.Lambda.AbstractSyntax (pt : propositional-truncations-exist) where

open PropositionalTruncation pt

open import MLTT.Spartan

data Vec (X : ๐“คโ‚€ ฬ‡ ) : โ„• โ†’ ๐“คโ‚€ ฬ‡ where
 โŸจโŸฉ  : Vec X zero
 _โ€™_ : {n : โ„•} โ†’ Vec X n โ†’ X โ†’ Vec X (succ n)

data Fin : (n : โ„•) โ†’ ๐“คโ‚€ ฬ‡ where
 zero : โˆ€ {n} โ†’ Fin (succ n)
 succ : โˆ€ {n} โ†’ Fin n โ†’ Fin (succ n)

data type : ๐“คโ‚€ ฬ‡ where
 ฮน : type
 _โ‡’_ : type โ†’ type โ†’ type

infixr 1 _โ‡’_

Context : โ„• โ†’ ๐“คโ‚€ ฬ‡
Context = Vec type

data _โˆ‹_ : {n : โ„•} โ†’ Context n โ†’ type โ†’ ๐“คโ‚€ ฬ‡ where
 Z : โˆ€ {n : โ„•} {ฮ“ : Context n} {ฯƒ : type} โ†’ (ฮ“ โ€™ ฯƒ) โˆ‹ ฯƒ
 S : โˆ€ {n : โ„•} {ฮ“ : Context n} {ฯƒ ฯ„ : type}
   โ†’ ฮ“ โˆ‹ ฯƒ
   โ†’ (ฮ“ โ€™ ฯ„) โˆ‹ ฯƒ


data PCF : {n : โ„•} (ฮ“ : Context n) (ฯƒ : type) โ†’ ๐“คโ‚€ ฬ‡ where

 Zero   : {n : โ„•} {ฮ“ : Context n}
        โ†’ PCF ฮ“ ฮน

 Succ   : {n : โ„•} {ฮ“ : Context n}
        โ†’ PCF ฮ“ ฮน
        โ†’ PCF ฮ“ ฮน

 Pred   : {n : โ„•} {ฮ“ : Context n}
        โ†’ PCF ฮ“ ฮน
        โ†’ PCF ฮ“ ฮน

 IfZero : {n : โ„•} {ฮ“ : Context n}
        โ†’ PCF ฮ“ ฮน
        โ†’ PCF ฮ“ ฮน
        โ†’ PCF ฮ“ ฮน
        โ†’ PCF ฮ“ ฮน

 ฦ›      : {n : โ„•} {ฮ“ : Context n} {ฯƒ ฯ„ : type}
        โ†’ PCF (ฮ“ โ€™ ฯƒ) ฯ„
        โ†’ PCF ฮ“ (ฯƒ โ‡’ ฯ„)

 _ยท_    : {n : โ„•} {ฮ“ : Context n} {ฯƒ ฯ„ : type}
        โ†’ PCF ฮ“ (ฯƒ โ‡’ ฯ„)
        โ†’ PCF ฮ“ ฯƒ
        โ†’ PCF ฮ“ ฯ„

 v      : {n : โ„•} {ฮ“ : Context n} {ฯƒ : type}
        โ†’ ฮ“ โˆ‹ ฯƒ
        โ†’ PCF ฮ“ ฯƒ

 Fix    : {n : โ„•} {ฮ“ : Context n} {ฯƒ : type}
        โ†’ PCF ฮ“ (ฯƒ โ‡’ ฯƒ)
        โ†’ PCF ฮ“ ฯƒ

infixl 1 _ยท_

lookup : {n : โ„•} โ†’ Context n โ†’ Fin n โ†’ type
lookup (ฮ“ โ€™ x) zero     = x
lookup (ฮ“ โ€™ x) (succ n) = lookup ฮ“ n

count : {n : โ„•} {ฮ“ : Context n} โ†’ (f : Fin n) โ†’ ฮ“ โˆ‹ lookup ฮ“ f
count {.(succ _)} {ฮ“ โ€™ x} zero     = Z
count {.(succ _)} {ฮ“ โ€™ x} (succ f) = S (count f)

ext : โˆ€ {m n} {ฮ“ : Context m} {ฮ” : Context n}
    โ†’ (โˆ€ {A} โ†’ ฮ“ โˆ‹ A โ†’ ฮ” โˆ‹ A)
    โ†’ (โˆ€ {ฯƒ A} โ†’ (ฮ“ โ€™ ฯƒ) โˆ‹ A โ†’ (ฮ” โ€™ ฯƒ) โˆ‹ A)
ext f Z     = Z
ext f (S t) = S (f t)

rename : โˆ€ {m n} {ฮ“ : Context m} {ฮ” : Context n}
       โ†’ (โˆ€ {A} โ†’ ฮ“ โˆ‹ A โ†’ ฮ” โˆ‹ A)
       โ†’ (โˆ€ {A} โ†’ PCF ฮ“ A โ†’ PCF ฮ” A)
rename f Zero = Zero
rename f (Succ t)         = Succ (rename f t)
rename f (Pred t)         = Pred (rename f t)
rename f (IfZero t tโ‚ tโ‚‚) = IfZero (rename f t) (rename f tโ‚) (rename f tโ‚‚)
rename f (ฦ› t)            = ฦ› (rename (ext f) t)
rename f (t ยท tโ‚)         = rename f t ยท rename f tโ‚
rename f (v x)            = v (f x)
rename f (Fix t)          = Fix (rename f t)

exts : โˆ€ {m n} {ฮ“ : Context m} {ฮ” : Context n}
       โ†’ (โˆ€ {A} โ†’ ฮ“ โˆ‹ A โ†’ PCF ฮ” A)
       โ†’ (โˆ€ {ฯƒ A} โ†’ (ฮ“ โ€™ ฯƒ) โˆ‹ A โ†’ PCF (ฮ” โ€™ ฯƒ) A)
exts f Z     = v Z
exts f (S t) = rename (_โˆ‹_.S) (f t)

subst : โˆ€ {m n} {ฮ“ : Context m} {ฮ” : Context n}
      โ†’ (โˆ€ {A} โ†’ ฮ“ โˆ‹ A โ†’ PCF ฮ” A)
      โ†’ (โˆ€ {A} โ†’ PCF ฮ“ A โ†’ PCF ฮ” A)
subst f Zero = Zero
subst f (Succ t)         = Succ (subst f t)
subst f (Pred t)         = Pred (subst f t)
subst f (IfZero t tโ‚ tโ‚‚) = IfZero (subst f t) (subst f tโ‚) (subst f tโ‚‚)
subst f (ฦ› t)            = ฦ› (subst (exts f) t)
subst f (t ยท tโ‚)         = subst f t ยท subst f tโ‚
subst f (v x)            = f x
subst f (Fix t)          = Fix (subst f t)

extend-with : {n : โ„•} {m : โ„•} {ฮ“ : Context n} {ฮ” : Context m}
              {A : type} (N : PCF ฮ” A)
            โ†’ (โˆ€ {A} โ†’ ฮ“ โˆ‹ A โ†’ PCF ฮ” A)
            โ†’ (โˆ€ {B} โ†’ (ฮ“ โ€™ A) โˆ‹ B โ†’ PCF ฮ” B)
extend-with N f Z = N
extend-with N f (S x) = f x

replace-first : {n : โ„•} (A : type) (ฮ“ : Context n) (N : PCF ฮ“ A)
              โ†’ (โˆ€ {B} โ†’ (ฮ“ โ€™ A) โˆ‹ B โ†’ PCF ฮ“ B)
replace-first A ฮ“ N Z     = N
replace-first A ฮ“ N (S t) = v t

_[_] : {n : โ„•} {ฮ“ : Context n} {ฯƒ A : type}
         โ†’ PCF (ฮ“ โ€™ A) ฯƒ โ†’ PCF ฮ“ A โ†’ PCF ฮ“ ฯƒ
_[_] {n} {ฮ“} {ฯƒ} {A} M N = subst (replace-first A ฮ“ N) M

numeral : โˆ€ {n} {ฮ“ : Context n} โ†’ โ„• โ†’ PCF ฮ“ ฮน
numeral zero     = Zero
numeral (succ n) = Succ (numeral n)

peano-axiom-for-PCF : โˆ€ {n ฮ“ k} โ†’ numeral {n} {ฮ“} zero โ‰  numeral (succ k)
peano-axiom-for-PCF ()

\end{code}