SoP2: Interpreted Function Symbols

Posted on April 2, 2016
Tags: SoP

This post discusses how to add arbitrary function symbols to the grammar introduced in the previous SoP article; thereby making the presentation of SoP1 more uniform!

The code for this article is available here.

module SoP2 where

open import Data.Vec renaming (map to vmap)
open import Data.Bool hiding (_∧_ ; _∨_) renaming (Bool to 𝔹)
open import MyPrelude hiding  (_⨾_ ; swap ; [_]) renaming (¬_ to NOT ; _>_ to _ℕ>_) 
open import SoP1 public using (Type ; 𝒩 ; 𝒫 ; ⟦_⟧ₜ ; _≟ₜ_ ;
                        Variable ; x ; y ; z ; _≟ᵥ_; State)

We build on the types and variables of the previous session, but alter the expressions. (The program language grammar is also unchanged, but refers to the new expressions instead!)

Function Symbol Datatype

We’d like to add arbitrary function symbols to our grammar. A first attempt would be,

record FunctionSymbol : Set where
  field
    arity : ℕ
    src tgt : Type

To capture the number of arguments, their source type, and the resulting target type.

To define the semantics brackets on expressions is now made unclear since we do not know how to interpret an arbitrary function symbol. The easiest thing to do is to place the interpretation alongside the other data.

record InterpretedFunctionSymbol : Set₁ where
  field
    arity : ℕ
    src tgt : Type
    reify   : Vec ⟦ src ⟧ₜ arity → ⟦ tgt ⟧ₜ

open InterpretedFunctionSymbol {{...}}

Now we extend the expressions datatype by a new function symbol application constructor:

data Expr : Type → Set₁ where
   ⋮
  app : (fsym : InterpretedFunctionSymbol) → Vec (Expr src) arity → Expr tgt

Then the semantics definition would be extended by the clause,

⟦ app fsym args ⟧ₑ σ  = reify (map (λ e → ⟦ e ⟧ₑ σ) args)

However this is a no-go since the semantics brackets are being recursively called on a not-so-trivially structurally smaller item and so not immediately clear that result will terminate. Hence Agda refuses the definition. One extreme, and unsafe, approach is just to disable termination checking. A more common approach is to case over the expressions/lists involved and do the map explicitly. A middle path would be to use well-founded recursion for writing non-structurally recursive programs in Agda. The first option is too scary and the last a bit technical for what we want, so we’ll take the simplest, thought not general, route.

So if we now try to case over args, we get a unification error. The system is not sure what to do. An immediate solution is to bring arity, the length of args, to the top as a parameter and then case over that. So we redefine,

record InterpretedFunctionSymbol (arity : ℕ) : Set₁ where
  field
    src tgt : Type
    reify   : Vec ⟦ src ⟧ₜ arity → ⟦ tgt ⟧ₜ

Okay great, we’ll case over args. Now how do we make a recursive call?! Our reify is not defined inductively and so we cannot break it down into pieces as we would for vectors. Let’s redefine yet again,

-- Func a s t ≡ s → s → ⋯ → s → t , with a-many s arguments
Func : ∀ {ℓ} (a : ℕ) (s t : Set ℓ) → Set ℓ
Func zero s t = t
Func (suc a) s t = s → Func a s t

record InterpretedFunctionSymbol (arity : ℕ) : Set₁ where
  field
    src tgt : Type
    reify   : Func arity ⟦ src ⟧ₜ ⟦ tgt ⟧ₜ

open InterpretedFunctionSymbol {{...}}

Now: an expression is a variable, a constant symbol, or a function symbol applied to other terms.

data Expr : Type → Set₁ where
  Var : ∀ {t} (v : Variable t) → Expr t
  𝒩  : ℕ → Expr 𝒩  
  𝒫  : Set → Expr 𝒫
  app : {arity : ℕ} (fsym : InterpretedFunctionSymbol arity) → Vec (Expr src) arity → Expr tgt

Notice that the formal code is quiet faithful to the informal definition preceding it!

Observe that we could not have written

  app : (arity : ℕ) (fsym : InterpretedFunctionSymbol arity) → Func arity (Expr src) (Expr tgt)

since datatype constructors must return the datatype being constructed and it’s not immediately clear that this is the case with Func, so the system rejects it.

Now: the interpretation of a variable is to look it up in the state, that of constants is to leave them alone, and that of a function application is to reify the function and apply it to the interpretation of its arguments.

infix 5 ⟦_⟧ₑ
⟦_⟧ₑ : ∀ {t} → Expr t → State → ⟦ t ⟧ₜ
⟦_⟧ₑ (Var v) σ = σ v
⟦_⟧ₑ (𝒩 q) σ = lift q
⟦_⟧ₑ (𝒫 p) σ = p
-- loosely: ⟦ f t₁ ⋯ tₙ ⟧ σ = (reify ⟦ t₁ ⟧ σ) ⟦ ftail t₂ ⋯ tₙ ⟧ σ
⟦_⟧ₑ (app {zero} fsym []) σ = reify
⟦_⟧ₑ (app {suc n} fsym (e ∷ args)) σ =
  let
    fsym-tail = record { src = src ; tgt = tgt ; reify = reify (⟦ e ⟧ₑ σ) }
  in
    ⟦ app {n} fsym-tail args ⟧ₑ σ

Notice that the formal code is quiet faithful to the informal definition preceding it!

One more time! The substitution over a variable occurs if the variables match, substitution over constants does nothing, and substitution over function symbol application is to just substitute over the argument terms.

_[_/_] : ∀ {s t} (E : Expr t) (e : Expr s) (v : Variable s) → Expr t
_[_/_] {s} {t} (Var v) v₁ e' with s ≟ₜ t
Var v [ e / v₁ ] ∣ yes ≡-refl = if v ≟ᵥ v₁ then e' else Var v
Var v [ e / v₁ ] ∣ no ¬p = Var v
𝒩 c  [ e / v  ] = 𝒩 c
𝒫 c  [ e / v  ] = 𝒫 c
app fsym args [ v / e ] = app fsym (helper args)
  where helper : ∀ {n} → Vec (Expr src) n → Vec (Expr src) n
        helper {zero } [] = []
        helper {suc n} (E ∷ ls) = E [ e / v ] ∷ helper ls

Notice that the formal code is quiet faithful to the informal definition preceding it!

Exercise! Write the definition of

_[_,_/₂_,_] : ∀ {s₁ s₂ t} → Expr t → Variable s₁ → Variable s₂ → Expr s₁ → Expr s₂ → Expr t

Regaining Our Previous Symbols

The old Expr syntax had built-in addition, conjunction, equality, etc.; and we intend to regain them with the power of interpreted function symbols.

We only show a few and leave the rest as exercises.

infix 10 _≈_
_≈_ : (m n : Expr 𝒩) → Expr 𝒫
m ≈ n = app symb (m ∷ n ∷ [])
  where
    sem : ⟦ 𝒩 ⟧ₜ → ⟦ 𝒩 ⟧ₜ → ⟦ 𝒫 ⟧ₜ
    sem (lift m) (lift n) = m ≡ n

    symb : InterpretedFunctionSymbol 2
    symb = record { src = 𝒩 ; tgt = 𝒫 ; reify = sem }

-- a new symbol ;)
infixr 11 _-_
_-_ : (m n : Expr 𝒩) → Expr 𝒩
m - n = app symb (m ∷ n ∷ [])
  where
    sem : ⟦ 𝒩 ⟧ₜ → ⟦ 𝒩 ⟧ₜ → ⟦ 𝒩 ⟧ₜ
    sem (lift m) (lift n) = lift (m ∸ n)

    symb : InterpretedFunctionSymbol 2
    symb = record { src = 𝒩 ; tgt = 𝒩 ; reify = sem }

Even more so, we can form simple notions of quantification. For example, simple summation:

-- sum over 'body' with index 'dummy' ranging over all natural numbers that are at most 'bound'
infix 10 Σ_≤_•_
Σ_≤_•_ : Variable 𝒩 → ℕ → Expr 𝒩 → Expr 𝒩
Σ_≤_•_ dummy bound body =
         app symb (vmap (λ i → body [ 𝒩 i / dummy ]) (downFrom bound))
  where

    -- downFrom n ≡ [n , n-1, n-2, …, 1, 0]
    downFrom : (n : ℕ) → Vec ℕ (suc n)
    downFrom zero = zero ∷ []
    downFrom (suc n) = suc n ∷ downFrom n

    -- ⟨ i , n ⟩ takes n-many arguments and adds them up then adds i on top of that
    ⟨_,_⟩ : Lift ℕ → (n : ℕ) → Func n ⟦ 𝒩 ⟧ₜ ⟦ 𝒩 ⟧ₜ
    ⟨ i , zero  ⟩   = i
    ⟨ lift i , suc n ⟩ (lift j) = ⟨ lift (i +ℕ j) , n ⟩

    example : ⟨ lift 0 , 4 ⟩ (lift 100) (lift 22) (lift 31) (lift 7) ≡ lift (100 +ℕ 22 +ℕ 31 +ℕ 7)
    example = ≡-refl

    symb : InterpretedFunctionSymbol (suc bound)
    symb = record { src = 𝒩 ; tgt = 𝒩 ; reify = ⟨ lift 0 , suc bound ⟩ }

Observe that the syntax ‘Σ dummy ≤ bound • body’ is interpreted as the sum of the body with dummy ranging over the integers 0..bound.

Let’s try this out! First, let’s use the notion of a default or initial state:

-- default state: numbers are 0 and booleans are false.
σ₀ : State
σ₀ {𝒩} v = lift 0
σ₀ {𝒫} v = ⊥

Then, say, the sum of the successor of naturals below 3 is 10:

-- ie 10 ≡ 10
sum-test :   ⟦ Σ x ≤ 3 • Var x + 𝒩 1 ⟧ₑ σ₀
           ≡ ⟦ (𝒩 0 + 𝒩 1) + (𝒩 1 + 𝒩 1) + (𝒩 2 + 𝒩 1) + (𝒩 3 + 𝒩 1)  ⟧ₑ σ₀
sum-test = ≡-refl

Notice that Σ x ≤ 3 • Var x + 𝒩 2 is really Σ x ≤ 3 • (Var x + 𝒩 2) and not (Σ x ≤ 3 • Var x) + 𝒩 2; which is consistent with the convention that quantifiers have scope as large/rightwards as possible. We’ve achieved this by the fixity declarations: summation is 10, which is higher priority than the 11 of addition.

Let’s consider a more complicated example; say a summation that involves variables.

σ₁ : State
σ₁ {𝒩} x = lift 1
σ₁ {𝒩} y = lift 2
σ₁ {𝒩} z = lift 3
σ₁ {𝒫} v = ⊥

sum-test2 :  ⟦ Σ x ≤ 3 • (Var x + Var y) - Var z ⟧ₑ σ₁
           ≡ ⟦ (𝒩 2 - 𝒩 3) + (𝒩 3 - 𝒩 3) + (𝒩 4 - 𝒩 3) + (𝒩 5 - 𝒩 3)  ⟧ₑ σ₁
sum-test2 = ≡-refl

Notice that x in the sum is not treated as a global variable and so state σ₁ is not called-upon for it.

Before we move on, let us remark that placing a bound of the form x ∶ m … n is tricky and I’ve failed to realize it since the interpretation portion of the symbol means I need a vector of length suc (n ∸ m) which is difficult to write. I’ve tried mimicking the Haskell definition and anyhow it’s not of immediate import. Still, it was hard and I just decided to use the case m ≡ 0 only.

This can be remedied by adding quantifiers explicitly to the expression syntax, thereby taking in a state for the interpretation. In particular,

⟦ SUM dummy bound range body ⟧ σ =
  reify (vmap (λ i → if ⟦ range [ dummy / 𝒩 i ] ⟧ σ then body [ dummy / 𝒩 i ] else 𝒩 0) (downFrom bound))

Just something to think about.

Unreify

While regaining some of our function symbols, one might’ve noticed a general pattern and it is that which we abstract here. That is, we will write a function that takes a real item and turns it into an an interpreted function symbol application.

-- two argument case
unreify₂ : ∀ {s t} → (⟦ s ⟧ₜ → ⟦ s ⟧ₜ → ⟦ t ⟧ₜ) → (a b : Expr s) → Expr t
unreify₂ {s} {t} r a b = app symb (a ∷ b ∷ [])
  where
    symb : InterpretedFunctionSymbol 2
    symb = record { src = s ; tgt = t ; reify = r }

-- one argument case
unreify₁ : ∀ {s t} → (⟦ s ⟧ₜ → ⟦ t ⟧ₜ) → (Expr s → Expr t)
unreify₁ {s} {t} r a = app symb (a ∷ [])
  where
    symb : InterpretedFunctionSymbol 1
    symb = record { src = s ; tgt = t ; reify = r }

-- could be less general by making B not depend on A
lift₂ : ∀ {a b ℓ} {A : Set a} {B : A → A → Set b}
      → ((p q : A) → B p q) → ((lp lq : Lift {a} {ℓ} A) → B (lower lp) (lower lq))
lift₂ r (lift p) (lift q) = r p q

lift₁ : ∀ {a b ℓ} {A : Set a} {B : A → Set b}
      → ((p : A) → B p) → ((lp : Lift {a} {ℓ} A) → B (lower lp))
lift₁ r (lift p) = r p

-- sometimes we have an operation of the form ℕ → ℕ → ℕ and we want this to yield a
-- function symbol typed Expr 𝒩 → Expr 𝒩 → Expr 𝒩 and so we introduce yet another combinator
unreify-ℕ₂ : (ℕ → ℕ → ℕ) → Expr 𝒩 → Expr 𝒩 → Expr 𝒩
unreify-ℕ₂ r = unreify₂ (lift₂ (λ p q → lift(r p q)))

Perhaps the name unreify is not the best..something to consider!

For example,

infixr 9 ¬_
¬_ : (p : Expr 𝒫) → Expr 𝒫
¬_ = unreify₁ NOT

infixr 8 _∨_
_∨_ : (p q : Expr 𝒫) → Expr 𝒫
_∨_ = unreify₂ _⊎_

infix 10 _>_
_>_ : (m n : Expr 𝒩) → Expr 𝒫
_>_ = unreify₂ (lift₂ (λ m n → n <ℕ m))

infix 10 _<_
_<_ : (m n : Expr 𝒩) → Expr 𝒫
m < n = n > m

infix 10 _≠_
_≠_ : (m n : Expr 𝒩) → Expr 𝒫
_≠_ = unreify₂ (lift₂ (λ a b → a ≡ b → ⊥))

Excellent! Now the user need only use these combinators and worry not about the underlying presentation of interpreted function symbols.

Let’s wrap-up by looking at an intersting theorem.

-- constant expression constructor
𝒞 : ∀ {t} → ⟦ t ⟧ₜ → Expr t
𝒞 {𝒩} e = 𝒩 (lower e)
𝒞 {𝒫} e = 𝒫 e

⟦𝒞⟧ : ∀ {t} {c : ⟦ t ⟧ₜ} {σ : State} → ⟦ 𝒞 c ⟧ₑ σ ≡ c
⟦𝒞⟧ {𝒩} = ≡-refl
⟦𝒞⟧ {𝒫} = ≡-refl

inverses : ∀ {s t} (f : ⟦ s ⟧ₜ → ⟦ t ⟧ₜ) (σ : State)
         →  let reify : ∀ {s' t'} (g : Expr s' → Expr t') → (⟦ s' ⟧ₜ → ⟦ t' ⟧ₜ) 
                reify g = λ a → ⟦ g (𝒞 a) ⟧ₑ σ in
          reify (unreify₁ f) ≗ f   -- pointwise equality
inverses f σ = λ a → ≡-cong f ⟦𝒞⟧

Notice that this reify differs from InterpretedFunctionSymbol.reify ! What of unreify₁ (reify f) ≗ f ? exercise.

Examples

Let’s produce a big example that uses all program constructs, except abort, and also makes use of the new symbols.

-- ∧ monotonicity: a nifty way to introduce implications involving ∧
∧-⇒ : ∀ {P Q P' Q'} → P ⇒ P' → Q ⇒ Q' → P ∧ Q ⇒ P' ∧ Q' 
∧-⇒ p q σ (a , b) = p σ a , q σ b

-- the refl case is so ubiquitous, let's name it.
_⨾⟨⟩_ : ∀ {Q S₁ P S₂ R} → ⟦ Q ⟧ S₁ ⟦ P ⟧ → ⟦ P ⟧ S₂ ⟦ R ⟧ → ⟦ Q ⟧ S₁ ⨾ S₂ ⟦ R ⟧
S ⨾⟨⟩ T = S ⨾⟨ (λ σ z₁ → z₁) ⟩ T -- C-c C-a

test : ⟦ True ⟧
           x ≔ 𝒩 3
         ⨾ skip
         ⨾ y ≔ 𝒩 4
         ⨾ x ≔ (Σ z ≤ 4 • Var z + Var z) -- sum of all even's that're at-most 8 = 0+2+4+6+8 = 20 
         ⨾ x , y ≔₂ Var x + Var y , Var x - Var y
       ⟦ Var x ≈ 𝒩 24 ∧ Var y ≈ 𝒩 16 ⟧
test =
        ⟦ True ⟧
            x ≔ 𝒩 3                                     since (λ σ _ → ≡-refl)
        ⟦ Var x ≈ 𝒩 3                                 ⟧
          ⨾⟨ (λ σ z₁ → z₁)  ⟩ -- ⇒-refl ⟩
        ⟦ Var x ≈ 𝒩 3                                 ⟧⟨ (λ σ z₁ → z₁) -- ⇒-refl 
        ⟩⟦ Var x ≈ 𝒩 3                                ⟧
          ⨾⟨ (λ σ _ → ≡-refl , ≡-refl) ⟩
        ⟦ 𝒩 20 + 𝒩 4 ≈ 𝒩 24 ∧ 𝒩 20 - 𝒩 4 ≈ 𝒩 16   ⟧
          y ≔ 𝒩 4                                       since (λ σ _ → ≡-refl , ≡-refl)
        ⟦ 𝒩 20 + Var y ≈ 𝒩 24 ∧ 𝒩 20 - Var y ≈ 𝒩 16 ⟧
          ⨾⟨ (λ σ z₁ → z₁) ⟩ -- ⇒-refl ⟩
        ⟦ (Σ z ≤ 4 • Var z + Var z) + Var y ≈ 𝒩 24 ∧ (Σ z ≤ 4 • Var z + Var z) - Var y ≈ 𝒩 16 ⟧
          x ≔ (Σ z ≤ 4 • Var z + Var z)                  since (λ σ z₁ → z₁) -- ⇒-refl
        ⟦ Var x + Var y ≈ 𝒩 24 ∧ Var x - Var y ≈ 𝒩 16 ⟧
          ⨾⟨⟩
        ⟦ Var x + Var y ≈ 𝒩 24 ∧ Var x - Var y ≈ 𝒩 16 ⟧
          x , y ≔₂ Var x + Var y , Var x - Var y since (λ σ z₁ → z₁) -- ⇒-refl
        ⟦ Var x ≈ 𝒩 24 ∧ Var y ≈ 𝒩 16 ⟧

Notice that the type is a claim we are making about the correctness of a program and the body is a proof of that claim.

Of course one should check that our earlier programs still work with the function symbols in-place. Exercise ;)

Closing

It seems that we’ve managed to get a lot done –up to chapter 9 of SoP excluding arrays–. Hope you’ve enjoyed the article!