SoP1: Assignment

Posted on March 31, 2016
Tags: SoP

This post discusses the syntax and semantics of a simple imperative language with simultaneous assignment.

module SoP1 where

open import Data.Bool using(if_then_else_ ; true ; false) renaming (Bool to 𝔹 )
open import MyPrelude hiding  (_β¨Ύ_ ; swap) renaming (_Γ—_ to _AND_)

The last import just brings into context the usual notions of propositional equality, sums, products, function operations, and a small theory of natural number arithmetic.

DataTypes

We want to describe sets of states of program variables and to write assertions about them. For simplicity, in our very elementary language (for now!), we only consider 𝒩atural numbers and 𝒫ropositions.

data Type : Set where
  𝒩  : Type
  𝒫  : Type

Which are then interpreted as elements of type Set₁:

-- subscript t, for "t"ypes
⟦_βŸ§β‚œ : Type β†’ Set₁
⟦ 𝒩 βŸ§β‚œ = Lift β„•
⟦ 𝒫 βŸ§β‚œ = Set

Notice that we interpret propositions constructively, since we’re in Agda after-all. Had we interpreted them as Booleans, reasoning would be a bit tricky since Booleans are not proof-carrying data. Alternatively: a proposition describes the set of states in which it is true and in Agda these notions coincide via Curry-Howard.

The Lift data type behaves, roughly, as follows: βˆ€ (i j : Level) β†’ i ≀ j β†’ Set i β†’ Set j. That is, it lets us embed a small type into a larger type. The β€˜equivalence’ A β‰… Lift A is witnessed by the constructor lift and inversely by the eliminator lower.

Finally, without any surprise, we can decide when the types coincide or not:

_β‰Ÿβ‚œ_ : Decidable {A = Type} _≑_
𝒩 β‰Ÿβ‚œ 𝒩 = yes ≑-refl
𝒩 β‰Ÿβ‚œ 𝒫 = no (Ξ» ())
𝒫 β‰Ÿβ‚œ 𝒩 = no (Ξ» ())
𝒫 β‰Ÿβ‚œ 𝒫 = yes ≑-refl

It feels like we ought to be able to mechanically derive equality as is done in Haskell; and indeed there is discussion on how to achieve this.

Variables

To make assertions of program variables, we need to have variables in the first place.

We use an explicitly dedicated datatype for formal variables.

data Variable : Type β†’ Set where
  x y z : βˆ€ {t} β†’ Variable t

_β‰Ÿα΅₯_ : βˆ€ {t s} β†’ Variable t β†’ Variable s β†’ 𝔹
x β‰Ÿα΅₯ x = true
x β‰Ÿα΅₯ _ = false
y β‰Ÿα΅₯ y = true
y β‰Ÿα΅₯ _ = false
z β‰Ÿα΅₯ z = true
z β‰Ÿα΅₯ _ = false

A more generic approach would be to parameterise the module by a type for variables that is endowed with decidable equality β€”a setoid.

Note that we cannot consider using de Bruijn indices, as in Agda by Example: Ξ»-calculus, since our variables are not bound to any quantifier. –perhaps I will switch to begin-end blocks introducing/quantifying over variables.

Expressions

With types and variables in-hand, we can discuss how to form terms and how to assign meaning to them.

Syntax

A term is defined to be a constant symbol c, a variable v, or a function/relation symbol f applied to terms:

term ∷= constant c ∣ variable v ∣ application f(t₁, …, tβ‚™)

For now, we take our function and relation symbols to be addition, ordering, equality, and conjunction.

data Expr : Type β†’ Set₁ where
  -- varaibles
  Var : βˆ€ {t} (v : Variable t) β†’ Expr t

  -- constant constructors
  𝒩 : β„• β†’ Expr 𝒩
  𝒫 : Set β†’ Expr 𝒫

  -- function/relation symbol application
  _+_ : (m n : Expr 𝒩) β†’ Expr 𝒩
  _β‰ˆ_ _≀_ : (e f : Expr 𝒩) β†’ Expr 𝒫
  _∧_ : (p q : Expr 𝒫) β†’ Expr 𝒫

infix 11 _+_
infix 10 _β‰ˆ_ _≀_
infix 8 _∧_

Notice that we make a natural constant by using 𝒩 and the type of the resulting expression is of type 𝒩, with this overloading, we can loosely say 𝒩 is the β€˜constructor’ for the β€˜type’ 𝒩. Likewise for 𝒫.

Another candidate for constant constructor is,

π’ž : βˆ€ {t} β†’ ⟦ t βŸ§β‚œ β†’ Expr t

syntax π’ž {t} c = c ∢ t -- ghost colon

However, I prefer the pair 𝒩, 𝒫 as they clearly denote the type of variable I’m working with; moreover, I cannot make them synonyms for _ ∢ 𝒩 , _ ∢ 𝒫 since 𝒩 , 𝒫 are already defined and Agda only permits constructor overloading.

Also, I thought about using 𝒱 instead of Var but the latter seems clearer and the former clashes with the aforementioned convention of the curly-letters denoting the type of the associated constant.

Semantics

An expression like Var x + 𝒩 5 can appear in a program; when encountered, it is β€˜evaluated’ in the current machine β€˜state’ to produce another natural number. What is this state? It is an association of identifiers to values.

State : Set₁
State = βˆ€ {t : Type} β†’ Variable t β†’ ⟦ t βŸ§β‚œ

It is common to denote the interpretation of an expression e in state Οƒ by ⟦ e ⟧ Οƒ where the β€˜semantics-brackets’ are defined by

⟦ c ⟧ Οƒ =  c  ; ⟦ v ⟧ Οƒ = Οƒ v ; ⟦ f(t₁, …, tβ‚™) ⟧ Οƒ = ⟦ f ⟧( ⟦ t₁ ⟧ Οƒ , …, ⟦ tβ‚™ ⟧ Οƒ)

Formally,

-- subscript e, for "e"xpressions
⟦_βŸ§β‚‘ : βˆ€ {t} β†’ Expr t β†’ State β†’ ⟦ t βŸ§β‚œ
⟦_βŸ§β‚‘ (Var v)  Οƒ = Οƒ v
⟦_βŸ§β‚‘ (𝒩 q)   Οƒ = lift q
⟦_βŸ§β‚‘ (𝒫 p)   Οƒ = p
⟦_βŸ§β‚‘ (e + e₁) Οƒ = lift $ lower (⟦ e βŸ§β‚‘ Οƒ) +β„•     lower (⟦ e₁ βŸ§β‚‘ Οƒ)
⟦_βŸ§β‚‘ (e β‰ˆ e₁) Οƒ = lift (lower (⟦ e βŸ§β‚‘ Οƒ)) ≑ lift (lower (⟦ e₁ βŸ§β‚‘ Οƒ)) -- propositional equality
⟦_βŸ§β‚‘ (e ≀ e₁) Οƒ =       lower (⟦ e βŸ§β‚‘ Οƒ)  ≀ℕ     lower (⟦ e₁ βŸ§β‚‘ Οƒ) 
⟦_βŸ§β‚‘ (e ∧ e₁) Οƒ =              ⟦ e βŸ§β‚‘ Οƒ   AND            ⟦ e₁ βŸ§β‚‘ Οƒ    -- Cartesian product

The addition case works as follows: ⟦ e + e₁ ⟧ Οƒ is obtained by recursively obtaining the semantics of the arguments, then using lower on the results to obtain the underlying naturals (of the lifted number type), then adding them, then packing up the whole thing into the lifted number type again. Similarly for the other cases.

Sometimes we want to update the state for a variable, say when it is reassigned, and we accomplish this by β€˜function patching’:

f [z ↦ y] = Ξ» x β†’ If x β‰Ÿ z Then y Else f x

Formally,

_[_↦_] : State β†’ βˆ€ {t} β†’ Variable t β†’ ⟦ t βŸ§β‚œ β†’ State
_[_↦_] Οƒ {t} v e {s} v∢s with t β‰Ÿβ‚œ s
_[_↦_] Οƒ v e v∢s ∣ yes ≑-refl = if v β‰Ÿα΅₯ v∢s then e else Οƒ v∢s
_[_↦_] Οƒ v e v∢s ∣ no Β¬p = Οƒ v∢s

Reasoning about Boolean expressions

Say proposition Q is weaker than P if P β‡’ Q; alternatively, P is stronger than Q. β€˜A stronger proposition makes more restrictions on the combinations of values its identifiers can be associated with, a weaker proposition makes fewer.’ That is, Q is β€˜less restrictive’ than P.

infix 2 _β‡’_
_β‡’_ : Expr 𝒫 β†’ Expr 𝒫 β†’ Set₁
P β‡’ Q = βˆ€ (Οƒ : State) β†’ ⟦ P βŸ§β‚‘ Οƒ β†’ ⟦ Q βŸ§β‚‘ Οƒ

The weakest proposition is true, or any tautology, because it represents the set of all states β€”ie it is always inhabited.

True : Expr 𝒫
True = 𝒫 ⊀

everything-implies-truth : βˆ€ {R} β†’ R β‡’ True
everything-implies-truth = Ξ» _ _ β†’ tt

The strongest proposition is false, because it represents the set of no states β€”ie it is never inhabited.

False : Expr 𝒫
False = 𝒫 βŠ₯

false-is-strongest : βˆ€ {Q} β†’ False β‡’ Q
false-is-strongest Οƒ ()

Before we move on, let us remark that _β‡’_ admits familiar properties, such as

β‡’-refl : βˆ€ {P} β†’ P β‡’ P
β‡’-refl Οƒ pf = pf

-- C-c C-a
β‡’-trans : βˆ€ {P Q R} β†’ P β‡’ Q β†’ Q β‡’ R β†’ P β‡’ R
β‡’-trans = Ξ» {P} {Q} {R} z₁ zβ‚‚ st z₃ β†’ zβ‚‚ st (z₁ st z₃)

∧-sym : βˆ€ {P Q} β†’ P ∧ Q β‡’ Q ∧ P
∧-sym st (p , q) = q , p

Using β‡’-refl without mentioning the implicit parameter yields yellow since Agda for some reason cannot infer them! However, if we comment out the definition of ⟦_βŸ§β‚‘ and postulate it instead, then no yellow :/ Send help!

Textual Substitution

Any expression E can be considered as a function E(v₁, …, vβ‚™) of it’s free-variables, say v₁, …, vβ‚™, then we can form a new expression E(e₁, …, eβ‚™) for any expressions eα΅’. However, this is cumbersome since the order of variables must be specified and also troublesome when I only want to substitute a few of the free variables. This is remedied by naming the variables to be replaced (irrespective of whether they are even in the given expression) and indicating its replacement as well β€”a sort of β€˜named arguments’ approach.

This β€˜textual substitution’ of variables v by expressions e is defined, informally, by three rules:

c [ e / v ]           = e
u [ e / v ]           = IF variable u is one of the vα΅’ THEN eα΅’ ELSE u
f(t₁, …, tβ‚™) [ e / v ] = f (t₁ [ e / v ], …, tβ‚™ [ e / v ])

The new term to be introduced occurs above the fraction symbol, expression [ new_term / old_variable], and we read E [t / x] as β€˜E with t replacing x’. As such, some would also write E [x β•² t]; other notations include E[x ≔ t] and EΛ£β‚œ.

Warning! Simultaneous is not iteration! In general, E [ u , v / x , y] β‰  (E [ u / x])[ v / y]. For example,

(x + y)[ x + y , z / x , y] = (x + y) + z β‰  (x + z) + z = (x + y)[x + y / x][z / y]

Anyhow, we implement the case n = 1 and leave the case n = 2 as an exercise for the reader. At the moment, I do not foresee the need for the general case; nor do I see a way to make it (quickly) syntactically appealing in Agda!

_[_/_] : βˆ€ {s t} (E : Expr t) (e : Expr s) (v : Variable s) β†’ Expr t
_[_/_] {s} {t} (Var v) u e with s β‰Ÿβ‚œ t
Var v [ e / u ] ∣ yes ≑-refl = if v β‰Ÿα΅₯ u then e else Var v
Var v [ e / u ] ∣ no ¬p = Var v
𝒩 n [ e / v ] = 𝒩 n
𝒫 p [ e / v ] = 𝒫 p
(E + F) [ e / v ] = E  [ e / v ]  +  F [ e / v ]
(E β‰ˆ F) [ e / v ] = E  [ e / v ]  β‰ˆ  F [ e / v ]
(E ≀ F) [ e / v ] = (E [ e / v ]) ≀ (F [ e / v ])
(E ∧ F) [ e / v ] = (E [ e / v ]) ∧ (F [ e / v ])

Observe,

The following is an exercise for the reader, where we want them to implement the function so that E [e, d / v,v] = E [d / v].

_[_,_/β‚‚_,_] : βˆ€ {s₁ sβ‚‚ t} (E : Expr t) (e₁ : Expr s₁) (eβ‚‚ : Expr sβ‚‚) (v₁ : Variable s₁) (vβ‚‚ : Variable sβ‚‚)  β†’ Expr t
E [ e₁ , eβ‚‚ /β‚‚ v₁ , vβ‚‚ ] = {! exercise !}

To close we give some lemmas dealing with textual substitution. Their proofs would be by induction on expressions and using the definitions of substitution; all-in-all quite a bore and so not proven here. From Chapter 4 of SoP:

-- constant helper
π’ž : βˆ€ {t} β†’ ⟦ t βŸ§β‚œ β†’ Expr t
π’ž {𝒩} c = 𝒩 (lower c)
π’ž {𝒫} c = 𝒫 c

postulate eval-over-sub : βˆ€ {t s} {v : Variable t} {Οƒ : State} {e : Expr t} {E : Expr s}
                        β†’ ⟦ E [ e / v ]  βŸ§β‚‘ Οƒ ≑ ⟦ E [ π’ž (⟦ e βŸ§β‚‘ Οƒ) / v ] βŸ§β‚‘ Οƒ
postulate sub-to-state : βˆ€ {t} {v : Variable t} {e : Expr t} {s} {E : Expr s} {Οƒ : State}
               β†’ ⟦ E [ e / v ] βŸ§β‚‘ Οƒ ≑ ⟦ E βŸ§β‚‘ (Οƒ [ v ↦ ⟦ e βŸ§β‚‘ Οƒ ])

That is, evaluating a substituted expression is the same as evaluating the original expression in an updated state. Notice that this law allows us to make substitutions part of the syntax and the law is then how to evaluate such syntax! Is that a better approach?!

postulate iterated-substitution : βˆ€ {t} {v : Variable t} {e d : Expr t} {s} {E : Expr s}
                                β†’ (E [ e / v ]) [ d / v ] ≑ E [ e [ d / v ] / v ]

For the curious, here is a very uninsightful proof of one of the above lemmas:

patching-id-pf : βˆ€ {t} {Οƒ : State} (v : Variable t) β†’ βˆ€ (u : Variable t) β†’ (Οƒ [ v ↦ Οƒ v ]) u ≑ Οƒ u
patching-id-pf {t} {Οƒ} v u with t β‰Ÿβ‚œ t
patching-id-pf v u ∣ no Β¬p = ≑-refl
patching-id-pf x x ∣ yes ≑-refl = ≑-refl
patching-id-pf x y ∣ yes ≑-refl = ≑-refl
patching-id-pf x z ∣ yes ≑-refl = ≑-refl
patching-id-pf y x ∣ yes ≑-refl = ≑-refl
patching-id-pf y y ∣ yes ≑-refl = ≑-refl
patching-id-pf y z ∣ yes ≑-refl = ≑-refl
patching-id-pf z x ∣ yes ≑-refl = ≑-refl
patching-id-pf z y ∣ yes ≑-refl = ≑-refl
patching-id-pf z z ∣ yes ≑-refl = ≑-refl

Admittedly, it could have been simplified had we implemented equality as a Decidable rather than just a Boolean.

To be fair, here’s a another proof of another result: substitution is monotonic. Informally,

  ⟦ P [ v / e ] βŸ§β‚‘ Οƒ
≑
  ⟦ P βŸ§β‚‘ (Οƒ [ v ↦ ⟦ e βŸ§β‚‘ Οƒ ])   -- since sub-to-state
β†’ 
  ⟦ Q βŸ§β‚‘ (Οƒ [ v ↦ ⟦ e βŸ§β‚‘ Οƒ ])   -- since P β‡’ Q
≑                              
  ⟦ Q [ v / e ] βŸ§β‚‘ Οƒ            -- since sub-to-state

Rather than create/import the needed syntacic sugar, let’s just β€˜wing-it’:

subst-over-β‡’ : βˆ€ {P Q t} {v : Variable t} {e : Expr t} β†’ P β‡’ Q β†’ P [ e / v ] β‡’ Q [ e / v ]
subst-over-⇒ {P} {Q} {t} {v} {e} P⇒Q σ
  rewrite sub-to-state {t} {v} {e} {𝒫} {P} {Οƒ} ` sub-to-state {t} {v} {e} {𝒫} {Q} {Οƒ} = Pβ‡’Q _

Programming Language

The syntax of our miniature language is as follows,

data Program : Set₁ where
  skip  : Program
  abort : Program
  _β¨Ύ_   : Program β†’ Program β†’ Program
  _≔_      : βˆ€ {t} β†’ Variable t β†’ Expr t β†’ Program
  _,_≔₂_,_ : βˆ€ {s t} β†’ Variable t β†’ Variable s β†’ Expr t β†’ Expr s β†’ Program

The subscript 2 in simultaneous assignment is needed, otherwise there’ll be parsing conflicts with the notation for elementary assignment.

As in usual programming languages, the precedence for the program constructors cannot be greater than that of expressions; otherwise, we’ll need many parentheses.

infix 7 _≔_
infixr 5 _β¨Ύ_

Now we quickly turn to the program semantics β€”we do not give β€˜operational semantics’ but instead use β€˜Hoare Triples’. The traditional notation for Hoare Triples is {Q} S {R}, with assertions enclosed in braces. However, since braces are one of the few reserved symbols in Agda, we instead employ the semantics-brackets yet again. This is not too much of a leap since the conditions are seen to define the program and so assign it meaning β€”the ideology mentioned in SoP is that one begins with the pre- and post-conditions then derives the program.

infixr 5 _⨾⟨_⟩_

data ⟦_⟧_⟦_⟧ : Expr 𝒫 β†’ Program β†’ Expr 𝒫 β†’ Set₁ where
  _⨾⟨_⟩_      : βˆ€ {Q S₁ P₁ Pβ‚‚ Sβ‚‚ R} β†’ ⟦ Q ⟧ S₁ ⟦ P₁ ⟧ β†’ P₁ β‡’ Pβ‚‚ β†’ ⟦ Pβ‚‚ ⟧ Sβ‚‚ ⟦ R ⟧ β†’ ⟦ Q ⟧ S₁ β¨Ύ Sβ‚‚ ⟦ R ⟧
  skip-rule  : βˆ€ {Q R} β†’ Q β‡’ R β†’ ⟦ Q ⟧ skip ⟦ R ⟧
  absurd     : βˆ€ {Q R} β†’ Q β‡’ False β†’ ⟦ Q ⟧ abort ⟦ R ⟧
  assignment : {t : Type} (v : Variable t) (e : Expr t) (Q R : Expr 𝒫)
             β†’ Q β‡’ R [ e  / v ] β†’ ⟦ Q ⟧ v ≔ e ⟦ R ⟧ 
  simuAssign : {t₁ tβ‚‚ : Type} (v₁ : Variable t₁) (vβ‚‚ : Variable tβ‚‚) (e₁ : Expr t₁) (eβ‚‚ : Expr tβ‚‚)
               (Q R : Expr 𝒫) β†’ Q β‡’ R [ e₁ , eβ‚‚ /β‚‚ v₁ , vβ‚‚ ] β†’ ⟦ Q ⟧ v₁ , vβ‚‚ ≔₂ e₁ , eβ‚‚ ⟦ R ⟧

Those who know me know that I simply adore types and so might be wondering why I considered raw untyped programs, Program, then correspondingly adorned each constructor with a type by considering programs typed by their specification. I do this so that

Anyhow, some remarks are in order:

As mentioned above, in a future post, I intend to replace the explicit constructors by what interpreted function symbols, but it seems that I need them to be augmented with a β€˜domain’ operation. For example, the symbol Γ· can be interpreted as integral division with domain condition being the second argument is non-zero. For now, all of our expressions are well-defined. In the future, we intend to use β€˜interpreted function symbols with domain’.

In practice, the domain condition is omitted altogether since assignments should be always written in contexts in which the expressions can be properly evaluated. If we are deriving our program and know not the context, then the full definition is quiet useful.

We now introduce some combinators to make our annotated programs look more like those presented in the literature.

-- for easy copy/paste: ⟦ ? ⟧ ? ≔ ? since ? ⟦ ? ⟧
syntax assignment v e Q R Qβ‡’Rβ‚‘Λ£ = ⟦ Q ⟧ v ≔ e since Qβ‡’Rβ‚‘Λ£ ⟦ R ⟧
syntax simuAssign v₁ vβ‚‚ e₁ eβ‚‚ Q R Qβ‡’Rβ‚‘Λ£ = ⟦ Q ⟧ v₁ , vβ‚‚ ≔₂ e₁ , eβ‚‚ since Qβ‡’Rβ‚‘Λ£ ⟦ R ⟧
syntax skip-rule {Q} {R} Qβ‡’R = ⟦ Q ⟧⟨ Qβ‡’R ⟩⟦ R ⟧ -- ⟦ Q ⟧ skip-since Qβ‡’R ⟦ R ⟧

For example, β€”Example 1, page 118 of SoPβ€”

progβ‚€ : ⟦ 𝒩 5 β‰ˆ 𝒩 5 ⟧ x ≔ 𝒩 5 ⟦ Var x β‰ˆ 𝒩 5  ⟧
progβ‚€ = assignment _ _ _ _ (Ξ» _ _ β†’ ≑-refl)

Now with out handy-dandy syntax:

prog₁ : ⟦ 𝒩 5 β‰ˆ 𝒩 5 ⟧ x ≔ 𝒩 5 ⟦ Var x β‰ˆ 𝒩 5  ⟧ 
prog₁ = ⟦ 𝒩 5 β‰ˆ 𝒩 5 ⟧ x ≔ 𝒩 5 since (Ξ» st β†’ β‡’-refl {𝒩 5 β‰ˆ 𝒩 5} st) ⟦ Var x β‰ˆ 𝒩 5 ⟧

Before we move on, we know from propostional logic that all theorems can be replaced with true. In particular, reflexitvity of equality does not give us much (in our toy language) and so we can replace it with true which was defined earlier as the unit type.

progβ‚‚ : ⟦ True ⟧ x ≔ 𝒩 5 ⟦ Var x β‰ˆ 𝒩 5  ⟧
progβ‚‚ = ⟦ True         ⟧
           x ≔ 𝒩 5      since (Ξ» _ _ β†’ ≑-refl) 
        ⟦ Var x β‰ˆ 𝒩 5 ⟧

Examples

We now port over some simple programs from Gries’ text and show that readability is still maintained! We begin with the most complicated one, that is expressible in the language as described so far.

swap : βˆ€ {X Y : β„•} β†’ ⟦ Var x β‰ˆ 𝒩 X ∧ Var y β‰ˆ 𝒩 Y ⟧
                             z ≔ Var {𝒩} x
                           β¨Ύ x ≔ Var {𝒩} y
                           β¨Ύ y ≔ Var {𝒩} z
                      ⟦ Var x β‰ˆ 𝒩 Y ∧ Var y β‰ˆ 𝒩 X ⟧
swap {X} {Y} =
                   ⟦ Var x β‰ˆ 𝒩 X  ∧ Var y β‰ˆ 𝒩 Y ⟧
                     z ≔ Var x                     since ∧-sym {Var x β‰ˆ 𝒩 X} {Var y β‰ˆ 𝒩 Y}
                   ⟦ Var y β‰ˆ 𝒩 Y ∧ Var z β‰ˆ 𝒩 X ⟧
                   ⨾⟨ (Ξ» st z₁ β†’ z₁) ⟩
                   ⟦ Var y β‰ˆ 𝒩 Y ∧ Var z β‰ˆ 𝒩 X ⟧
                     x ≔ Var y                     since (Ξ» st z₁ β†’ z₁)
                   ⟦ Var x β‰ˆ 𝒩 Y ∧ Var z β‰ˆ 𝒩 X ⟧
                   ⨾⟨ (Ξ» st z₁ β†’ z₁) ⟩
                   ⟦ Var x β‰ˆ 𝒩 Y ∧ Var z β‰ˆ 𝒩 X ⟧
                     y ≔ Var z                     since (Ξ» st z₁ β†’ z₁)
                   ⟦ Var x β‰ˆ 𝒩 Y ∧ Var y β‰ˆ 𝒩 X ⟧

Some things to note:

Swapping becomes a one-liner using simultaneous assignment.

swap2 : βˆ€ {X Y : β„•} β†’ ⟦ Var x β‰ˆ 𝒩 X ∧ Var y β‰ˆ 𝒩 Y ⟧ x , y ≔₂ Var {𝒩} y , Var {𝒩} x ⟦ Var x β‰ˆ 𝒩 Y ∧ Var y β‰ˆ 𝒩 X ⟧
swap2 {X} {Y} = ⟦ Var x β‰ˆ 𝒩 X ∧ Var y β‰ˆ 𝒩 Y ⟧
                  x , y ≔₂ Var y , Var x         since ∧-sym {Var x β‰ˆ 𝒩 X} {Var y β‰ˆ 𝒩 Y}
                ⟦ Var x β‰ˆ 𝒩 Y ∧ Var y β‰ˆ 𝒩 X ⟧

One popular language that offers such a command is Python.

Another example of sequence β€”many C-c C-r!

prog₃ : ⟦ True ⟧ skip β¨Ύ x ≔ 𝒩 5 ⟦ Var x β‰ˆ 𝒩 5  ⟧
prog₃ =  ⟦ True ⟧⟨    β‡’-refl {True}
         ⟩⟦ True ⟧
        ⨾⟨ (Ξ» st x₁ β†’ x₁) ⟩
        ⟦ True ⟧
        x ≔ 𝒩 5 since (Ξ» _ _ β†’ ≑-refl)
        ⟦ Var x β‰ˆ 𝒩 5 ⟧

Multiple assignments to the same variable mean only the last assignment is realized.

progβ‚„ : ⟦ True ⟧ x ≔ 𝒩 5 β¨Ύ x ≔ 𝒩 3 ⟦ Var x β‰ˆ 𝒩 3  ⟧ 
progβ‚„ = ⟦ True ⟧
          x ≔ 𝒩 5       since (Ξ» _ _ β†’ ≑-refl)
        ⟦ 𝒩 3 β‰ˆ 𝒩 3 ⟧
        ⨾⟨ β‡’-refl {𝒩 3 β‰ˆ 𝒩 3} ⟩
        ⟦ 𝒩 3 β‰ˆ 𝒩 3 ⟧
          x ≔ 𝒩 3       since β‡’-refl {𝒩 3 β‰ˆ 𝒩 3}
        ⟦ Var x β‰ˆ 𝒩 3 ⟧

Awesome! Looks like a paper-and-pencil annotation (with proofs)!

If the post condition does not involve the variable assigned, then we can ignore it: x not free in P yields ⟦ P ⟧ x ≔ e ⟦ P ⟧.

Here is a particular case, obtained by C-c C-a then using syntactic sugar –page 119–,

constantEx : βˆ€ {e : Expr 𝒩} {c : β„•} β†’ ⟦ Var y β‰ˆ 𝒩 c ⟧ x ≔ e ⟦ Var y β‰ˆ 𝒩 c ⟧
constantEx {e} {c} = ⟦ Var y β‰ˆ 𝒩 c ⟧
                       x ≔ e       since (Ξ» st pf β†’ pf)
                     ⟦ Var y β‰ˆ 𝒩 c ⟧

Sometimes we’ll need lemmas in our annotations. For example, If I want x to be at least 10 after increasing it by 3, then I necessairly need x to be at least 7 before the increment. [Page 118, but no negative numbers.]

leq : ⟦ 𝒩 7 ≀ Var x ⟧ x ≔ Var x + 𝒩 3 ⟦ 𝒩 10 ≀ Var x  ⟧
leq = ⟦ 𝒩 7 ≀ Var x ⟧
         x ≔ Var x + 𝒩 3       since lemma1
      ⟦ 𝒩 10 ≀ Var x ⟧
      where
        lemma1 : 𝒩 7 ≀ Var x β‡’ 𝒩 10 ≀ Var x + 𝒩 3
        lemma1 Οƒ 7≀σx = 7≀σx +-mono ≀ℕ-refl {3}

where we have used the fact that addition preserves order, _+-mono_ : βˆ€ {x y u v : β„•} β†’ x ≀ℕ y β†’ u ≀ℕ v β†’ x +β„• u ≀ y +β„• v.

Program Equality

Earlier, when introducing the programming language semantics, we mentioned certain equalities; such as, skip is identity of composition: skip β¨Ύ S = S β¨Ύ skip = S. We never defined program equality! Let’s fix that.

Two programs are considered equal precisely when they satisfy the same specifications,

infix 4 _β‰ˆβ‚š_
_β‰ˆβ‚š_ : Program β†’ Program β†’ Set₁
S β‰ˆβ‚š T = βˆ€ {Q R} β†’ ⟦ Q ⟧ S ⟦ R ⟧ ⇔ ⟦ Q ⟧ T ⟦ R ⟧

Where x ⇔ y just means a pair of functions x β†’ y and y β†’ x.

Let us prove the aforementioned unity law. We begin with an expected result, then the needed pieces.

strengthen : βˆ€ Q {P R S} β†’ Q β‡’ P β†’ ⟦ P ⟧ S ⟦ R ⟧ β†’ ⟦ Q ⟧ S ⟦ R ⟧
strengthen = {! exercise in C-c C-c and C-c C-a   ^_^ !}

What about? weaken : βˆ€ {Q P} R {S} β†’ P β‡’ R β†’ ⟦ Q ⟧ S ⟦ P ⟧ β†’ ⟦ Q ⟧ S ⟦ R ⟧ ?

Let’s add some syntacic sugar β€”good ol’ sweet stuff ^_^

syntax strengthen Q Qβ‡’P ⟦P⟧S⟦R⟧ = ⟦ Q βŸ§β‡’βŸ¨ Qβ‡’P ⟩ ⟦P⟧S⟦R⟧
tada : βˆ€ {S Q R} β†’  ⟦ Q ⟧ skip β¨Ύ S ⟦ R ⟧ β†’ ⟦ Q ⟧ S ⟦ R ⟧
tada {S} {Q} {R} (skip-rule Qβ‡’P₁ ⨾⟨ P₁⇒Pβ‚‚ ⟩ ⟦Pβ‚‚βŸ§S⟦R⟧) =
  ⟦ Q βŸ§β‡’βŸ¨ (Ξ» Οƒ z₁ β†’ P₁⇒Pβ‚‚ Οƒ (Qβ‡’P₁ Οƒ z₁))⟩ ⟦Pβ‚‚βŸ§S⟦R⟧


tada˘ : βˆ€ {S} {Q R}  β†’ ⟦ Q ⟧ S ⟦ R ⟧ β†’  ⟦ Q ⟧ skip β¨Ύ S ⟦ R ⟧
tada˘ {S} {Q} {R} ⟦Q⟧S⟦R⟧ =
  ⟦ Q ⟧⟨ β‡’-refl {Q}
  ⟩⟦ Q ⟧
  ⨾⟨ β‡’-refl {Q} ⟩
  ⟦Q⟧S⟦R⟧

skip-left-unit : βˆ€ {S} β†’ skip β¨Ύ S β‰ˆβ‚š S
skip-left-unit = tada , tada˘

These abstract-proofs are not as clear as the examples, but that’s to be expected since the syntax was made with concrete code annotation in mind.

Closing

It seems that we’ve managed to get a lot done –up to chapter 9 of SoP excluding arrays, quantification, and a few other function and relation symbols. We intend to remedy the situation in future posts! Hope you’ve enjoyed the article!