module plfa.part3.Denotational where

The lambda calculus is a language about functions, that is, mappings from input to output. In computing we often think of such mappings as being carried out by a sequence of operations that transform an input into an output. But functions can also be represented as data. For example, one can tabulate a function, that is, create a table where each row has two entries, an input and the corresponding output for the function. Function application is then the process of looking up the row for a given input and reading off the output.

We shall create a semantics for the untyped lambda calculus based on this idea of functions-as-tables. However, there are two difficulties that arise. First, functions often have an infinite domain, so it would seem that we would need infinitely long tables to represent functions. Second, in the lambda calculus, functions can be applied to functions. They can even be applied to themselves! So it would seem that the tables would contain cycles. One might start to worry that advanced techniques are necessary to address these issues, but fortunately this is not the case!

The first problem, of functions with infinite domains, is solved by observing that in the execution of a terminating program, each lambda abstraction will only be applied to a finite number of distinct arguments. (We come back later to discuss diverging programs.) This observation is another way of looking at Dana Scott’s insight that only continuous functions are needed to model the lambda calculus.

The second problem, that of self-application, is solved by relaxing the way in which we lookup an argument in a function’s table. Naively, one would look in the table for a row in which the input entry exactly matches the argument. In the case of self-application, this would require the table to contain a copy of itself. Impossible! (At least, it is impossible if we want to build tables using inductive data type definitions, which indeed we do.) Instead it is sufficient to find an input such that every row of the input appears as a row of the argument (that is, the input is a subset of the argument). In the case of self-application, the table only needs to contain a smaller copy of itself, which is fine.

With these two observations in hand, it is straightforward to write down a denotational semantics of the lambda calculus.

Imports

open import Agda.Primitive using (lzero; lsuc)
open import Data.Empty using (βŠ₯-elim)
open import Data.Nat using (β„•; zero; suc)
open import Data.Product using (_Γ—_; Ξ£; Ξ£-syntax; βˆƒ; βˆƒ-syntax; proj₁; projβ‚‚)
  renaming (_,_ to ⟨_,_⟩)
open import Data.Sum
open import Data.Vec using (Vec; []; _∷_)
open import Relation.Binary.PropositionalEquality
  using (_≑_; _β‰’_; refl; sym; cong; congβ‚‚; cong-app)
open import Relation.Nullary using (Β¬_)
open import Relation.Nullary.Negation using (contradiction)
open import Function using (_∘_)
open import plfa.part2.Untyped
  using (Context; β˜…; _βˆ‹_; βˆ…; _,_; Z; S_; _⊒_; `_; _Β·_; Ζ›_;
         #_; twoᢜ; ext; rename; exts; subst; subst-zero; _[_])
open import plfa.part2.Substitution using (Rename; extensionality; rename-id)

Values

The Value data type represents a finite portion of a function. We think of a value as a finite set of pairs that represent input-output mappings. The Value data type represents the set as a binary tree whose internal nodes are the union operator and whose leaves represent either a single mapping or the empty set.

  • The βŠ₯ value provides no information about the computation.

  • A value of the form v ↦ w is a single input-output mapping, from input v to output w.

  • A value of the form v βŠ” w is a function that maps inputs to outputs according to both v and w. Think of it as taking the union of the two sets.

infixr 7 _↦_
infixl 5 _βŠ”_

data Value : Set where
  βŠ₯ : Value
  _↦_ : Value β†’ Value β†’ Value
  _βŠ”_ : Value β†’ Value β†’ Value

The βŠ‘ relation adapts the familiar notion of subset to the Value data type. This relation plays the key role in enabling self-application. There are two rules that are specific to functions, βŠ‘-fun and βŠ‘-dist, which we discuss below.

infix 4 _βŠ‘_

data _βŠ‘_ : Value β†’ Value β†’ Set where

  βŠ‘-bot : βˆ€ {v} β†’ βŠ₯ βŠ‘ v

  βŠ‘-conj-L : βˆ€ {u v w}
    β†’ v βŠ‘ u
    β†’ w βŠ‘ u
      -----------
    β†’ (v βŠ” w) βŠ‘ u

  βŠ‘-conj-R1 : βˆ€ {u v w}
    β†’ u βŠ‘ v
      -----------
    β†’ u βŠ‘ (v βŠ” w)

  βŠ‘-conj-R2 : βˆ€ {u v w}
    β†’ u βŠ‘ w
      -----------
    β†’ u βŠ‘ (v βŠ” w)

  βŠ‘-trans : βˆ€ {u v w}
    β†’ u βŠ‘ v
    β†’ v βŠ‘ w
      -----
    β†’ u βŠ‘ w

  βŠ‘-fun : βˆ€ {v w vβ€² wβ€²}
    β†’ vβ€² βŠ‘ v
    β†’ w βŠ‘ wβ€²
      -------------------
    β†’ (v ↦ w) βŠ‘ (vβ€² ↦ wβ€²)

  βŠ‘-dist : βˆ€{v w wβ€²}
      ---------------------------------
    β†’ v ↦ (w βŠ” wβ€²) βŠ‘ (v ↦ w) βŠ” (v ↦ wβ€²)

The first five rules are straightforward. The rule βŠ‘-fun captures when it is OK to match a higher-order argument vβ€² ↦ wβ€² to a table entry whose input is v ↦ w. Considering a call to the higher-order argument. It is OK to pass a larger argument than expected, so v can be larger than vβ€². Also, it is OK to disregard some of the output, so w can be smaller than wβ€². The rule βŠ‘-dist says that if you have two entries for the same input, then you can combine them into a single entry and joins the two outputs.

The βŠ‘ relation is reflexive.

βŠ‘-refl : βˆ€ {v} β†’ v βŠ‘ v
βŠ‘-refl {βŠ₯} = βŠ‘-bot
βŠ‘-refl {v ↦ vβ€²} = βŠ‘-fun βŠ‘-refl βŠ‘-refl
βŠ‘-refl {v₁ βŠ” vβ‚‚} = βŠ‘-conj-L (βŠ‘-conj-R1 βŠ‘-refl) (βŠ‘-conj-R2 βŠ‘-refl)

The βŠ” operation is monotonic with respect to βŠ‘, that is, given two larger values it produces a larger value.

βŠ”βŠ‘βŠ” : βˆ€ {v w vβ€² wβ€²}
  β†’ v βŠ‘ vβ€²  β†’  w βŠ‘ wβ€²
    -----------------------
  β†’ (v βŠ” w) βŠ‘ (vβ€² βŠ” wβ€²)
βŠ”βŠ‘βŠ” d₁ dβ‚‚ = βŠ‘-conj-L (βŠ‘-conj-R1 d₁) (βŠ‘-conj-R2 dβ‚‚)

The βŠ‘-dist rule can be used to combine two entries even when the input values are not identical. One can first combine the two inputs using βŠ” and then apply the βŠ‘-dist rule to obtain the following property.

βŠ”β†¦βŠ”-dist : βˆ€{v vβ€² w wβ€² : Value}
  β†’ (v βŠ” vβ€²) ↦ (w βŠ” wβ€²) βŠ‘ (v ↦ w) βŠ” (vβ€² ↦ wβ€²)
βŠ”β†¦βŠ”-dist = βŠ‘-trans βŠ‘-dist (βŠ”βŠ‘βŠ” (βŠ‘-fun (βŠ‘-conj-R1 βŠ‘-refl) βŠ‘-refl)
                            (βŠ‘-fun (βŠ‘-conj-R2 βŠ‘-refl) βŠ‘-refl))

If the join u βŠ” v is less than another value w, then both u and v are less than w.

βŠ”βŠ‘-invL : βˆ€{u v w : Value}
  β†’ u βŠ” v βŠ‘ w
    ---------
  β†’ u βŠ‘ w
βŠ”βŠ‘-invL (βŠ‘-conj-L lt1 lt2) = lt1
βŠ”βŠ‘-invL (βŠ‘-conj-R1 lt) = βŠ‘-conj-R1 (βŠ”βŠ‘-invL lt)
βŠ”βŠ‘-invL (βŠ‘-conj-R2 lt) = βŠ‘-conj-R2 (βŠ”βŠ‘-invL lt)
βŠ”βŠ‘-invL (βŠ‘-trans lt1 lt2) = βŠ‘-trans (βŠ”βŠ‘-invL lt1) lt2

βŠ”βŠ‘-invR : βˆ€{u v w : Value}
  β†’ u βŠ” v βŠ‘ w
    ---------
  β†’ v βŠ‘ w
βŠ”βŠ‘-invR (βŠ‘-conj-L lt1 lt2) = lt2
βŠ”βŠ‘-invR (βŠ‘-conj-R1 lt) = βŠ‘-conj-R1 (βŠ”βŠ‘-invR lt)
βŠ”βŠ‘-invR (βŠ‘-conj-R2 lt) = βŠ‘-conj-R2 (βŠ”βŠ‘-invR lt)
βŠ”βŠ‘-invR (βŠ‘-trans lt1 lt2) = βŠ‘-trans (βŠ”βŠ‘-invR lt1) lt2

Environments

An environment gives meaning to the free variables in a term by mapping variables to values.

Env : Context β†’ Set
Env Ξ“ = βˆ€ (x : Ξ“ βˆ‹ β˜…) β†’ Value

We have the empty environment, and we can extend an environment.

`βˆ… : Env βˆ…
`βˆ… ()

infixl 5 _`,_

_`,_ : βˆ€ {Ξ“} β†’ Env Ξ“ β†’ Value β†’ Env (Ξ“ , β˜…)
(Ξ³ `, v) Z = v
(Ξ³ `, v) (S x) = Ξ³ x

We can recover the previous environment from an extended environment, and the last value. Putting them together again takes us back to where we started.

init : βˆ€ {Ξ“} β†’ Env (Ξ“ , β˜…) β†’ Env Ξ“
init Ξ³ x = Ξ³ (S x)

last : βˆ€ {Ξ“} β†’ Env (Ξ“ , β˜…) β†’ Value
last Ξ³ = Ξ³ Z

init-last : βˆ€ {Ξ“} β†’ (Ξ³ : Env (Ξ“ , β˜…)) β†’ Ξ³ ≑ (init Ξ³ `, last Ξ³)
init-last {Ξ“} Ξ³ = extensionality lemma
  where lemma : βˆ€ (x : Ξ“ , β˜… βˆ‹ β˜…) β†’ Ξ³ x ≑ (init Ξ³ `, last Ξ³) x
        lemma Z      =  refl
        lemma (S x)  =  refl

We extend the βŠ‘ relation point-wise to environments with the following definition.

_`βŠ‘_ : βˆ€ {Ξ“} β†’ Env Ξ“ β†’ Env Ξ“ β†’ Set
_`βŠ‘_ {Ξ“} Ξ³ Ξ΄ = βˆ€ (x : Ξ“ βˆ‹ β˜…) β†’ Ξ³ x βŠ‘ Ξ΄ x

We define a bottom environment and a join operator on environments, which takes the point-wise join of their values.

`βŠ₯ : βˆ€ {Ξ“} β†’ Env Ξ“
`βŠ₯ x = βŠ₯

_`βŠ”_ : βˆ€ {Ξ“} β†’ Env Ξ“ β†’ Env Ξ“ β†’ Env Ξ“
(Ξ³ `βŠ” Ξ΄) x = Ξ³ x βŠ” Ξ΄ x

The βŠ‘-refl, βŠ‘-conj-R1, and βŠ‘-conj-R2 rules lift to environments. So the join of two environments Ξ³ and Ξ΄ is greater than the first environment Ξ³ or the second environment Ξ΄.

`βŠ‘-refl : βˆ€ {Ξ“} {Ξ³ : Env Ξ“} β†’ Ξ³ `βŠ‘ Ξ³
`βŠ‘-refl {Ξ“} {Ξ³} x = βŠ‘-refl {Ξ³ x}

βŠ‘-env-conj-R1 : βˆ€ {Ξ“} β†’ (Ξ³ : Env Ξ“) β†’ (Ξ΄ : Env Ξ“) β†’ Ξ³ `βŠ‘ (Ξ³ `βŠ” Ξ΄)
βŠ‘-env-conj-R1 Ξ³ Ξ΄ x = βŠ‘-conj-R1 βŠ‘-refl

βŠ‘-env-conj-R2 : βˆ€ {Ξ“} β†’ (Ξ³ : Env Ξ“) β†’ (Ξ΄ : Env Ξ“) β†’ Ξ΄ `βŠ‘ (Ξ³ `βŠ” Ξ΄)
βŠ‘-env-conj-R2 Ξ³ Ξ΄ x = βŠ‘-conj-R2 βŠ‘-refl

Denotational Semantics

We define the semantics with a judgment of the form ρ ⊒ M ↓ v, where ρ is the environment, M the program, and v is a result value. For readers familiar with big-step semantics, this notation will feel quite natural, but don’t let the similarity fool you. There are subtle but important differences! So here is the definition of the semantics, which we discuss in detail in the following paragraphs.

infix 3 _⊒_↓_

data _⊒_↓_ : βˆ€{Ξ“} β†’ Env Ξ“ β†’ (Ξ“ ⊒ β˜…) β†’ Value β†’ Set where

  var : βˆ€ {Ξ“} {Ξ³ : Env Ξ“} {x}
      ---------------
    β†’ Ξ³ ⊒ (` x) ↓ Ξ³ x

  ↦-elim : βˆ€ {Ξ“} {Ξ³ : Env Ξ“} {L M v w}
    β†’ Ξ³ ⊒ L ↓ (v ↦ w)
    β†’ Ξ³ ⊒ M ↓ v
      ---------------
    β†’ Ξ³ ⊒ (L Β· M) ↓ w

  ↦-intro : βˆ€ {Ξ“} {Ξ³ : Env Ξ“} {N v w}
    β†’ Ξ³ `, v ⊒ N ↓ w
      -------------------
    β†’ Ξ³ ⊒ (Ζ› N) ↓ (v ↦ w)

  βŠ₯-intro : βˆ€ {Ξ“} {Ξ³ : Env Ξ“} {M}
      ---------
    β†’ Ξ³ ⊒ M ↓ βŠ₯

  βŠ”-intro : βˆ€ {Ξ“} {Ξ³ : Env Ξ“} {M v w}
    β†’ Ξ³ ⊒ M ↓ v
    β†’ Ξ³ ⊒ M ↓ w
      ---------------
    β†’ Ξ³ ⊒ M ↓ (v βŠ” w)

  sub : βˆ€ {Ξ“} {Ξ³ : Env Ξ“} {M v w}
    β†’ Ξ³ ⊒ M ↓ v
    β†’ w βŠ‘ v
      ---------
    β†’ Ξ³ ⊒ M ↓ w

Consider the rule for lambda abstractions, ↦-intro. It says that a lambda abstraction results in a single-entry table that maps the input v to the output w, provided that evaluating the body in an environment with v bound to its parameter produces the output w. As a simple example of this rule, we can see that the identity function maps βŠ₯ to βŠ₯ and also that it maps βŠ₯ ↦ βŠ₯ to βŠ₯ ↦ βŠ₯.

id : βˆ… ⊒ β˜…
id = Ζ› # 0

denot-id1 : βˆ€ {Ξ³} β†’ Ξ³ ⊒ id ↓ βŠ₯ ↦ βŠ₯
denot-id1 = ↦-intro var

denot-id2 : βˆ€ {Ξ³} β†’ Ξ³ ⊒ id ↓ (βŠ₯ ↦ βŠ₯) ↦ (βŠ₯ ↦ βŠ₯)
denot-id2 = ↦-intro var

Of course, we will need tables with many rows to capture the meaning of lambda abstractions. These can be constructed using the βŠ”-intro rule. If term M (typically a lambda abstraction) can produce both tables v and w, then it produces the combined table v βŠ” w. One can take an operational view of the rules ↦-intro and βŠ”-intro by imagining that when an interpreter first comes to a lambda abstraction, it pre-evaluates the function on a bunch of randomly chosen arguments, using many instances of the rule ↦-intro, and then joins them into a big table using many instances of the rule βŠ”-intro. In the following we show that the identity function produces a table containing both of the previous results, βŠ₯ ↦ βŠ₯ and (βŠ₯ ↦ βŠ₯) ↦ (βŠ₯ ↦ βŠ₯).

denot-id3 : `βˆ… ⊒ id ↓ (βŠ₯ ↦ βŠ₯) βŠ” (βŠ₯ ↦ βŠ₯) ↦ (βŠ₯ ↦ βŠ₯)
denot-id3 = βŠ”-intro denot-id1 denot-id2

We most often think of the judgment Ξ³ ⊒ M ↓ v as taking the environment Ξ³ and term M as input, producing the result v. However, it is worth emphasizing that the semantics is a relation. The above results for the identity function show that the same environment and term can be mapped to different results. However, the results for a given Ξ³ and M are not too different, they are all finite approximations of the same function. Perhaps a better way of thinking about the judgment Ξ³ ⊒ M ↓ v is that the Ξ³, M, and v are all inputs and the semantics either confirms or denies whether v is an accurate partial description of the result of M in environment Ξ³.

Next we consider the meaning of function application as given by the ↦-elim rule. In the premise of the rule we have that L maps v to w. So if M produces v, then the application of L to M produces w.

As an example of function application and the ↦-elim rule, we apply the identity function to itself. Indeed, we have both that βˆ… ⊒ id ↓ (u ↦ u) ↦ (u ↦ u) and also βˆ… ⊒ id ↓ (u ↦ u), so we can apply the rule ↦-elim.

id-app-id : βˆ€ {u : Value} β†’ `βˆ… ⊒ id Β· id ↓ (u ↦ u)
id-app-id {u} = ↦-elim (↦-intro var) (↦-intro var)

Next we revisit the Church numeral two: Ξ» f. Ξ» u. (f (f u)). This function has two parameters: a function f and an arbitrary value u, and it applies f twice. So f must map u to some value, which we’ll name v. Then for the second application, f must map v to some value. Let’s name it w. So the function’s table must include two entries, both u ↦ v and v ↦ w. For each application of the table, we extract the appropriate entry from it using the sub rule. In particular, we use the βŠ‘-conj-R1 and βŠ‘-conj-R2 to select u ↦ v and v ↦ w, respectively, from the table u ↦ v βŠ” v ↦ w. So the meaning of twoᢜ is that it takes this table and parameter u, and it returns w. Indeed we derive this as follows.

denot-twoᢜ : βˆ€{u v w : Value} β†’ `βˆ… ⊒ twoᢜ ↓ ((u ↦ v βŠ” v ↦ w) ↦ u ↦ w)
denot-twoᢜ {u}{v}{w} =
  ↦-intro (↦-intro (↦-elim (sub var lt1) (↦-elim (sub var lt2) var)))
  where lt1 : v ↦ w βŠ‘ u ↦ v βŠ” v ↦ w
        lt1 = βŠ‘-conj-R2 (βŠ‘-fun βŠ‘-refl βŠ‘-refl)

        lt2 : u ↦ v βŠ‘ u ↦ v βŠ” v ↦ w
        lt2 = (βŠ‘-conj-R1 (βŠ‘-fun βŠ‘-refl βŠ‘-refl))

Next we have a classic example of self application: Ξ” = Ξ»x. (x x). The input value for x needs to be a table, and it needs to have an entry that maps a smaller version of itself, call it v, to some value w. So the input value looks like v ↦ w βŠ” v. Of course, then the output of Ξ” is w. The derivation is given below. The first occurrences of x evaluates to v ↦ w, the second occurrence of x evaluates to v, and then the result of the application is w.

Ξ” : βˆ… ⊒ β˜…
Ξ” = (Ζ› (# 0) Β· (# 0))

denot-Ξ” : βˆ€ {v w} β†’ `βˆ… ⊒ Ξ” ↓ ((v ↦ w βŠ” v) ↦ w)
denot-Ξ” = ↦-intro (↦-elim (sub var (βŠ‘-conj-R1 βŠ‘-refl))
                          (sub var (βŠ‘-conj-R2 βŠ‘-refl)))

One might worry whether this semantics can deal with diverging programs. The βŠ₯ value and the βŠ₯-intro rule provide a way to handle them. (The βŠ₯-intro rule is also what enables Ξ² reduction on non-terminating arguments.) The classic Ξ© program is a particularly simple program that diverges. It applies Ξ” to itself. The semantics assigns to Ξ© the meaning βŠ₯. There are several ways to derive this, we shall start with one that makes use of the βŠ”-intro rule. First, denot-Ξ” tells us that Ξ” evaluates to ((βŠ₯ ↦ βŠ₯) βŠ” βŠ₯) ↦ βŠ₯ (choose v₁ = vβ‚‚ = βŠ₯). Next, Ξ” also evaluates to βŠ₯ ↦ βŠ₯ by use of ↦-intro and βŠ₯-intro and to βŠ₯ by βŠ₯-intro. As we saw previously, whenever we can show that a program evaluates to two values, we can apply βŠ”-intro to join them together, so Ξ” evaluates to (βŠ₯ ↦ βŠ₯) βŠ” βŠ₯. This matches the input of the first occurrence of Ξ”, so we can conclude that the result of the application is βŠ₯.

Ξ© : βˆ… ⊒ β˜…
Ξ© = Ξ” Β· Ξ”

denot-Ξ© : `βˆ… ⊒ Ξ© ↓ βŠ₯
denot-Ξ© = ↦-elim denot-Ξ” (βŠ”-intro (↦-intro βŠ₯-intro) βŠ₯-intro)

A shorter derivation of the same result is by just one use of the βŠ₯-intro rule.

denot-Ξ©' : `βˆ… ⊒ Ξ© ↓ βŠ₯
denot-Ξ©' = βŠ₯-intro

Just because one can derive βˆ… ⊒ M ↓ βŠ₯ for some closed term M doesn’t mean that M necessarily diverges. There may be other derivations that conclude with M producing some more informative value. However, if the only thing that a term evaluates to is βŠ₯, then it indeed diverges.

An attentive reader may have noticed a disconnect earlier in the way we planned to solve the self-application problem and the actual ↦-elim rule for application. We said at the beginning that we would relax the notion of table lookup, allowing an argument to match an input entry if the argument is equal or greater than the input entry. Instead, the ↦-elim rule seems to require an exact match. However, because of the sub rule, application really does allow larger arguments.

↦-elim2 : βˆ€ {Ξ“} {Ξ³ : Env Ξ“} {M₁ Mβ‚‚ v₁ vβ‚‚ v₃}
  β†’ Ξ³ ⊒ M₁ ↓ (v₁ ↦ v₃)
  β†’ Ξ³ ⊒ Mβ‚‚ ↓ vβ‚‚
  β†’ v₁ βŠ‘ vβ‚‚
    ------------------
  β†’ Ξ³ ⊒ (M₁ Β· Mβ‚‚) ↓ v₃
↦-elim2 d₁ dβ‚‚ lt = ↦-elim d₁ (sub dβ‚‚ lt)

Exercise denot-plusᢜ (practice)

What is a denotation for plusᢜ? That is, find a value v (other than βŠ₯) such that βˆ… ⊒ plusᢜ ↓ v. Also, give the proof of βˆ… ⊒ plusᢜ ↓ v for your choice of v.

-- Your code goes here

Denotations and denotational equality

Next we define a notion of denotational equality based on the above semantics. Its statement makes use of an if-and-only-if, which we define as follows.

_iff_ : Set β†’ Set β†’ Set
P iff Q = (P β†’ Q) Γ— (Q β†’ P)

Another way to view the denotational semantics is as a function that maps a term to a relation from environments to values. That is, the denotation of a term is a relation from environments to values.

Denotation : Context β†’ Set₁
Denotation Ξ“ = (Env Ξ“ β†’ Value β†’ Set)

The following function β„° gives this alternative view of the semantics, which really just amounts to changing the order of the parameters.

β„° : βˆ€{Ξ“} β†’ (M : Ξ“ ⊒ β˜…) β†’ Denotation Ξ“
β„° M = Ξ» Ξ³ v β†’ Ξ³ ⊒ M ↓ v

In general, two denotations are equal when they produce the same values in the same environment.

infix 3 _≃_

_≃_ : βˆ€ {Ξ“} β†’ (Denotation Ξ“) β†’ (Denotation Ξ“) β†’ Set
(_≃_ {Ξ“} D₁ Dβ‚‚) = (Ξ³ : Env Ξ“) β†’ (v : Value) β†’ D₁ Ξ³ v iff Dβ‚‚ Ξ³ v

Denotational equality is an equivalence relation.

≃-refl : βˆ€ {Ξ“ : Context} β†’ {M : Denotation Ξ“}
  β†’ M ≃ M
≃-refl Ξ³ v = ⟨ (Ξ» x β†’ x) , (Ξ» x β†’ x) ⟩

≃-sym : βˆ€ {Ξ“ : Context} β†’ {M N : Denotation Ξ“}
  β†’ M ≃ N
    -----
  β†’ N ≃ M
≃-sym eq Ξ³ v = ⟨ (projβ‚‚ (eq Ξ³ v)) , (proj₁ (eq Ξ³ v)) ⟩

≃-trans : βˆ€ {Ξ“ : Context} β†’ {M₁ Mβ‚‚ M₃ : Denotation Ξ“}
  β†’ M₁ ≃ Mβ‚‚
  β†’ Mβ‚‚ ≃ M₃
    -------
  β†’ M₁ ≃ M₃
≃-trans eq1 eq2 Ξ³ v = ⟨ (Ξ» z β†’ proj₁ (eq2 Ξ³ v) (proj₁ (eq1 Ξ³ v) z)) ,
                        (Ξ» z β†’ projβ‚‚ (eq1 Ξ³ v) (projβ‚‚ (eq2 Ξ³ v) z)) ⟩

Two terms M and N are denotational equal when their denotations are equal, that is, β„° M ≃ β„° N.

The following submodule introduces equational reasoning for the ≃ relation.

module ≃-Reasoning {Ξ“ : Context} where

  infix  1 start_
  infixr 2 _β‰ƒβŸ¨βŸ©_ _β‰ƒβŸ¨_⟩_
  infix  3 _☐

  start_ : βˆ€ {x y : Denotation Ξ“}
    β†’ x ≃ y
      -----
    β†’ x ≃ y
  start x≃y  =  x≃y

  _β‰ƒβŸ¨_⟩_ : βˆ€ (x : Denotation Ξ“) {y z : Denotation Ξ“}
    β†’ x ≃ y
    β†’ y ≃ z
      -----
    β†’ x ≃ z
  (x β‰ƒβŸ¨ x≃y ⟩ y≃z) =  ≃-trans x≃y y≃z

  _β‰ƒβŸ¨βŸ©_ : βˆ€ (x : Denotation Ξ“) {y : Denotation Ξ“}
    β†’ x ≃ y
      -----
    β†’ x ≃ y
  x β‰ƒβŸ¨βŸ© x≃y  =  x≃y

  _☐ : βˆ€ (x : Denotation Ξ“)
      -----
    β†’ x ≃ x
  (x ☐)  =  ≃-refl

Road map for the following chapters

The subsequent chapters prove that the denotational semantics has several desirable properties. First, we prove that the semantics is compositional, i.e., that the denotation of a term is a function of the denotations of its subterms. To do this we shall prove equations of the following shape.

β„° (` x) ≃ ...
β„° (Ζ› M) ≃ ... β„° M ...
β„° (M Β· N) ≃ ... β„° M ... β„° N ...

The compositionality property is not trivial because the semantics we have defined includes three rules that are not syntax directed: βŠ₯-intro, βŠ”-intro, and sub. The above equations suggest that the dentoational semantics can be defined as a recursive function, and indeed, we give such a definition and prove that it is equivalent to β„°.

Next we investigate whether the denotational semantics and the reduction semantics are equivalent. Recall that the job of a language semantics is to describe the observable behavior of a given program M. For the lambda calculus there are several choices that one can make, but they usually boil down to a single bit of information:

  • divergence: the program M executes forever.
  • termination: the program M halts.

We can characterize divergence and termination in terms of reduction.

  • divergence: Β¬ (M β€”β†  Ζ› N) for any term N.
  • termination: M β€”β†  Ζ› N for some term N.

We can also characterize divergence and termination using denotations.

  • divergence: Β¬ (βˆ… ⊒ M ↓ v ↦ w) for any v and w.
  • termination: βˆ… ⊒ M ↓ v ↦ w for some v and w.

Alternatively, we can use the denotation function β„°.

  • divergence: Β¬ (β„° M ≃ β„° (Ζ› N)) for any term N.
  • termination: β„° M ≃ β„° (Ζ› N) for some term N.

So the question is whether the reduction semantics and denotational semantics are equivalent.

(βˆƒ N. M β€”β†  Ζ› N)  iff  (βˆƒ N. β„° M ≃ β„° (Ζ› N))

We address each direction of the equivalence in the second and third chapters. In the second chapter we prove that reduction to a lambda abstraction implies denotational equality to a lambda abstraction. This property is called the soundness in the literature.

M β€”β†  Ζ› N  implies  β„° M ≃ β„° (Ζ› N)

In the third chapter we prove that denotational equality to a lambda abstraction implies reduction to a lambda abstraction. This property is called adequacy in the literature.

β„° M ≃ β„° (Ζ› N)  implies M β€”β†  Ζ› Nβ€² for some Nβ€²

The fourth chapter applies the results of the three preceeding chapters (compositionality, soundness, and adequacy) to prove that denotational equality implies a property called contextual equivalence. This property is important because it justifies the use of denotational equality in proving the correctness of program transformations such as performance optimizations.

The proofs of all of these properties rely on some basic results about the denotational semantics, which we establish in the rest of this chapter. We start with some lemmas about renaming, which are quite similar to the renaming lemmas that we have seen in previous chapters. We conclude with a proof of an important inversion lemma for the less-than relation regarding function values.

Renaming preserves denotations

We shall prove that renaming variables, and changing the environment accordingly, preserves the meaning of a term. We generalize the renaming lemma to allow the values in the new environment to be the same or larger than the original values. This generalization is useful in proving that reduction implies denotational equality.

As before, we need an extension lemma to handle the case where we proceed underneath a lambda abstraction. Suppose that ρ is a renaming that maps variables in γ into variables with equal or larger values in δ. This lemmas says that extending the renaming producing a renaming ext r that maps γ , v to δ , v.

ext-βŠ‘ : βˆ€ {Ξ“ Ξ” v} {Ξ³ : Env Ξ“} {Ξ΄ : Env Ξ”}
  β†’ (ρ : Rename Ξ“ Ξ”)
  β†’ Ξ³ `βŠ‘ (Ξ΄ ∘ ρ)
    ------------------------------
  β†’ (Ξ³ `, v) `βŠ‘ ((Ξ΄ `, v) ∘ ext ρ)
ext-βŠ‘ ρ lt Z = βŠ‘-refl
ext-βŠ‘ ρ lt (S nβ€²) = lt nβ€²

We proceed by cases on the de Bruijn index n.

  • If it is Z, then we just need to show that v ≑ v, which we have by refl.

  • If it is S nβ€², then the goal simplifies to Ξ³ nβ€² ≑ Ξ΄ (ρ nβ€²), which is an instance of the premise.

Now for the renaming lemma. Suppose we have a renaming that maps variables in Ξ³ into variables with the same values in Ξ΄. If M results in v when evaluated in environment Ξ³, then applying the renaming to M produces a program that results in the same value v when evaluated in Ξ΄.

rename-pres : βˆ€ {Ξ“ Ξ” v} {Ξ³ : Env Ξ“} {Ξ΄ : Env Ξ”} {M : Ξ“ ⊒ β˜…}
  β†’ (ρ : Rename Ξ“ Ξ”)
  β†’ Ξ³ `βŠ‘ (Ξ΄ ∘ ρ)
  β†’ Ξ³ ⊒ M ↓ v
    ---------------------
  β†’ Ξ΄ ⊒ (rename ρ M) ↓ v
rename-pres ρ lt (var {x = x}) = sub var (lt x)
rename-pres ρ lt (↦-elim d d₁) =
   ↦-elim (rename-pres ρ lt d) (rename-pres ρ lt d₁)
rename-pres ρ lt (↦-intro d) =
   ↦-intro (rename-pres (ext ρ) (ext-βŠ‘ ρ lt) d)
rename-pres ρ lt βŠ₯-intro = βŠ₯-intro
rename-pres ρ lt (βŠ”-intro d d₁) =
   βŠ”-intro (rename-pres ρ lt d) (rename-pres ρ lt d₁)
rename-pres ρ lt (sub d ltβ€²) =
   sub (rename-pres ρ lt d) ltβ€²

The proof is by induction on the semantics of M. As you can see, all of the cases are trivial except the cases for variables and lambda.

  • For a variable x, we make use of the premise to show that Ξ³ x ≑ Ξ΄ (ρ x).

  • For a lambda abstraction, the induction hypothesis requires us to extend the renaming. We do so, and use the ext-βŠ‘ lemma to show that the extended renaming maps variables to ones with equivalent values.

Environment strengthening and identity renaming

We shall need a corollary of the renaming lemma that says that replacing the environment with a larger one (a stronger one) does not change whether a term M results in particular value v. In particular, if Ξ³ ⊒ M ↓ v and Ξ³ βŠ‘ Ξ΄, then Ξ΄ ⊒ M ↓ v. What does this have to do with renaming? It’s renaming with the identity function. We apply the renaming lemma with the identity renaming, which gives us Ξ΄ ⊒ rename (Ξ» {A} x β†’ x) M ↓ v, and then we apply the rename-id lemma to obtain Ξ΄ ⊒ M ↓ v.

βŠ‘-env : βˆ€ {Ξ“} {Ξ³ : Env Ξ“} {Ξ΄ : Env Ξ“} {M v}
  β†’ Ξ³ ⊒ M ↓ v
  β†’ Ξ³ `βŠ‘ Ξ΄
    ----------
  β†’ Ξ΄ ⊒ M ↓ v
βŠ‘-env{Ξ“}{Ξ³}{Ξ΄}{M}{v} d lt
      with rename-pres{Ξ“}{Ξ“}{v}{Ξ³}{Ξ΄}{M} (Ξ» {A} x β†’ x) lt d
... | δ⊒id[M]↓v rewrite rename-id {Ξ“}{β˜…}{M} =
      δ⊒id[M]↓v

In the proof that substitution reflects denotations, in the case for lambda abstraction, we use a minor variation of βŠ‘-env, in which just the last element of the environment gets larger.

up-env : βˆ€ {Ξ“} {Ξ³ : Env Ξ“} {M v u₁ uβ‚‚}
  β†’ (Ξ³ `, u₁) ⊒ M ↓ v
  β†’ u₁ βŠ‘ uβ‚‚
    -----------------
  β†’ (Ξ³ `, uβ‚‚) ⊒ M ↓ v
up-env d lt = βŠ‘-env d (ext-le lt)
  where
  ext-le : βˆ€ {Ξ³ u₁ uβ‚‚} β†’ u₁ βŠ‘ uβ‚‚ β†’ (Ξ³ `, u₁) `βŠ‘ (Ξ³ `, uβ‚‚)
  ext-le lt Z = lt
  ext-le lt (S n) = βŠ‘-refl

Church numerals are more general than natural numbers in that they represent paths. A path consists of n edges and n + 1 vertices. We store the vertices in a vector of length n + 1 in reverse order. The edges in the path map the ith vertex to the i + 1 vertex. The following function D^suc (for denotation of successor) constructs a table whose entries are all the edges in the path.

D^suc : (n : β„•) β†’ Vec Value (suc n) β†’ Value
D^suc zero (a[0] ∷ []) = βŠ₯
D^suc (suc i) (a[i+1] ∷ a[i] ∷ ls) =  a[i] ↦ a[i+1]  βŠ”  D^suc i (a[i] ∷ ls)

We use the following auxilliary function to obtain the last element of a non-empty vector. (This formulation is more convenient for our purposes than the one in the Agda standard library.)

vec-last : βˆ€{n : β„•} β†’ Vec Value (suc n) β†’ Value
vec-last {0} (a ∷ []) = a
vec-last {suc n} (a ∷ b ∷ ls) = vec-last (b ∷ ls)

The function Dᢜ computes the denotation of the nth Church numeral for a given path.

Dᢜ : (n : β„•) β†’ Vec Value (suc n) β†’ Value
Dᢜ n (a[n] ∷ ls) = (D^suc n (a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n]

  • The Church numeral for 0 ignores its first argument and returns its second argument, so for the singleton path consisting of just a[0], its denotation is

      βŠ₯ ↦ a[0] ↦ a[0]

  • The Church numeral for suc n takes two arguments: a successor function whose denotation is given by D^suc, and the start of the path (last of the vector). It returns the n + 1 vertex in the path.

      (D^suc (suc n) (a[n+1] ∷ a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n+1]

The exercise is to prove that for any path ls, the meaning of the Church numeral n is Dᢜ n ls.

To fascilitate talking about arbitrary Church numerals, the following church function builds the term for the nth Church numeral, using the auxilliary function apply-n.

apply-n : (n : β„•) β†’ βˆ… , β˜… , β˜… ⊒ β˜…
apply-n zero = # 0
apply-n (suc n) = # 1 Β· apply-n n

church : (n : β„•) β†’ βˆ… ⊒ β˜…
church n = Ζ› Ζ› apply-n n

Prove the following theorem.

denot-church : βˆ€{n : β„•}{ls : Vec Value (suc n)}
   β†’ `βˆ… ⊒ church n ↓ Dᢜ n ls

-- Your code goes here

Inversion of the less-than relation for functions

What can we deduce from knowing that a function v ↦ w is less than some value u? What can we deduce about u? The answer to this question is called the inversion property of less-than for functions. This question is not easy to answer because of the βŠ‘-dist rule, which relates a function on the left to a pair of functions on the right. So u may include several functions that, as a group, relate to v ↦ w. Furthermore, because of the rules βŠ‘-conj-R1 and βŠ‘-conj-R2, there may be other values inside u, such as βŠ₯, that have nothing to do with v ↦ w. But in general, we can deduce that u includes a collection of functions where the join of their domains is less than v and the join of their codomains is greater than w.

To precisely state and prove this inversion property, we need to define what it means for a value to include a collection of values. We also need to define how to compute the join of their domains and codomains.

Value membership and inclusion

Recall that we think of a value as a set of entries with the join operator v βŠ” w acting like set union. The function value v ↦ w and bottom value βŠ₯ constitute the two kinds of elements of the set. (In other contexts one can instead think of βŠ₯ as the empty set, but here we must think of it as an element.) We write u ∈ v to say that u is an element of v, as defined below.

infix 5 _∈_

_∈_ : Value β†’ Value β†’ Set
u ∈ βŠ₯ = u ≑ βŠ₯
u ∈ v ↦ w = u ≑ v ↦ w
u ∈ (v βŠ” w) = u ∈ v ⊎ u ∈ w

So we can represent a collection of values simply as a value. We write v βŠ† w to say that all the elements of v are also in w.

infix 5 _βŠ†_

_βŠ†_ : Value β†’ Value β†’ Set
v βŠ† w = βˆ€{u} β†’ u ∈ v β†’ u ∈ w

The notions of membership and inclusion for values are closely related to the less-than relation. They are narrower relations in that they imply the less-than relation but not the other way around.

βˆˆβ†’βŠ‘ : βˆ€{u v : Value}
    β†’ u ∈ v
      -----
    β†’ u βŠ‘ v
βˆˆβ†’βŠ‘ {.βŠ₯} {βŠ₯} refl = βŠ‘-bot
βˆˆβ†’βŠ‘ {v ↦ w} {v ↦ w} refl = βŠ‘-refl
βˆˆβ†’βŠ‘ {u} {v βŠ” w} (inj₁ x) = βŠ‘-conj-R1 (βˆˆβ†’βŠ‘ x)
βˆˆβ†’βŠ‘ {u} {v βŠ” w} (injβ‚‚ y) = βŠ‘-conj-R2 (βˆˆβ†’βŠ‘ y)

βŠ†β†’βŠ‘ : βˆ€{u v : Value}
    β†’ u βŠ† v
      -----
    β†’ u βŠ‘ v
βŠ†β†’βŠ‘ {βŠ₯} s with s {βŠ₯} refl
... | x = βŠ‘-bot
βŠ†β†’βŠ‘ {u ↦ uβ€²} s with s {u ↦ uβ€²} refl
... | x = βˆˆβ†’βŠ‘ x
βŠ†β†’βŠ‘ {u βŠ” uβ€²} s = βŠ‘-conj-L (βŠ†β†’βŠ‘ (Ξ» z β†’ s (inj₁ z))) (βŠ†β†’βŠ‘ (Ξ» z β†’ s (injβ‚‚ z)))

We shall also need some inversion principles for value inclusion. If the union of u and v is included in w, then of course both u and v are each included in w.

βŠ”βŠ†-inv : βˆ€{u v w : Value}
       β†’ (u βŠ” v) βŠ† w
         ---------------
       β†’ u βŠ† w  Γ—  v βŠ† w
βŠ”βŠ†-inv uvw = ⟨ (Ξ» x β†’ uvw (inj₁ x)) , (Ξ» x β†’ uvw (injβ‚‚ x)) ⟩

In our value representation, the function value v ↦ w is both an element and also a singleton set. So if v ↦ w is a subset of u, then v ↦ w must be a member of u.

β†¦βŠ†β†’βˆˆ : βˆ€{v w u : Value}
     β†’ v ↦ w βŠ† u
       ---------
     β†’ v ↦ w ∈ u
β†¦βŠ†β†’βˆˆ incl = incl refl

Function values

To identify collections of functions, we define the following two predicates. We write Fun u if u is a function value, that is, if u ≑ v ↦ w for some values v and w. We write all-funs v if all the elements of v are functions.

data Fun : Value β†’ Set where
  fun : βˆ€{u v w} β†’ u ≑ (v ↦ w) β†’ Fun u

all-funs : Value β†’ Set
all-funs v = βˆ€{u} β†’ u ∈ v β†’ Fun u

The value βŠ₯ is not a function.

Β¬FunβŠ₯ : Β¬ (Fun βŠ₯)
Β¬FunβŠ₯ (fun ())

In our values-as-sets representation, our sets always include at least one element. Thus, if all the elements are functions, there is at least one that is a function.

all-funs∈ : βˆ€{u}
      β†’ all-funs u
      β†’ Ξ£[ v ∈ Value ] Ξ£[ w ∈ Value ] v ↦ w ∈ u
all-funs∈ {βŠ₯} f with f {βŠ₯} refl
... | fun ()
all-funs∈ {v ↦ w} f = ⟨ v , ⟨ w , refl ⟩ ⟩
all-funs∈ {u βŠ” uβ€²} f
    with all-funs∈ Ξ» z β†’ f (inj₁ z)
... | ⟨ v , ⟨ w , m ⟩ ⟩ = ⟨ v , ⟨ w , (inj₁ m) ⟩ ⟩

Domains and codomains

Returning to our goal, the inversion principle for less-than a function, we want to show that v ↦ w βŠ‘ u implies that u includes a set of function values such that the join of their domains is less than v and the join of their codomains is greater than w.

To this end we define the following ⨆dom and ⨆cod functions. Given some value u (that represents a set of entries), ⨆dom u returns the join of their domains and ⨆cod u returns the join of their codomains.

⨆dom : (u : Value) β†’ Value
⨆dom βŠ₯  = βŠ₯
⨆dom (v ↦ w) = v
⨆dom (u βŠ” uβ€²) = ⨆dom u βŠ” ⨆dom uβ€²

⨆cod : (u : Value) β†’ Value
⨆cod βŠ₯  = βŠ₯
⨆cod (v ↦ w) = w
⨆cod (u βŠ” uβ€²) = ⨆cod u βŠ” ⨆cod uβ€²

We need just one property each for ⨆dom and ⨆cod. Given a collection of functions represented by value u, and an entry v ↦ w ∈ u, we know that v is included in the domain of v.

β†¦βˆˆβ†’βŠ†β¨†dom : βˆ€{u v w : Value}
          β†’ all-funs u  β†’  (v ↦ w) ∈ u
            ----------------------
          β†’ v βŠ† ⨆dom u
β†¦βˆˆβ†’βŠ†β¨†dom {βŠ₯} fg () u∈v
β†¦βˆˆβ†’βŠ†β¨†dom {v ↦ w} fg refl u∈v = u∈v
β†¦βˆˆβ†’βŠ†β¨†dom {u βŠ” uβ€²} fg (inj₁ v↦w∈u) u∈v =
   let ih = β†¦βˆˆβ†’βŠ†β¨†dom (Ξ» z β†’ fg (inj₁ z)) v↦w∈u in
   inj₁ (ih u∈v)
β†¦βˆˆβ†’βŠ†β¨†dom {u βŠ” uβ€²} fg (injβ‚‚ v↦w∈uβ€²) u∈v =
   let ih = β†¦βˆˆβ†’βŠ†β¨†dom (Ξ» z β†’ fg (injβ‚‚ z)) v↦w∈uβ€² in
   injβ‚‚ (ih u∈v)

Regarding ⨆cod, suppose we have a collection of functions represented by u, but all of them are just copies of v ↦ w. Then the ⨆cod u is included in w.

βŠ†β†¦β†’β¨†codβŠ† : βˆ€{u v w : Value}
        β†’ u βŠ† v ↦ w
          ---------
        β†’ ⨆cod u βŠ† w
βŠ†β†¦β†’β¨†codβŠ† {βŠ₯} s refl with s {βŠ₯} refl
... | ()
βŠ†β†¦β†’β¨†codβŠ† {C ↦ Cβ€²} s m with s {C ↦ Cβ€²} refl
... | refl = m
βŠ†β†¦β†’β¨†codβŠ† {u βŠ” uβ€²} s (inj₁ x) = βŠ†β†¦β†’β¨†codβŠ† (Ξ» {C} z β†’ s (inj₁ z)) x
βŠ†β†¦β†’β¨†codβŠ† {u βŠ” uβ€²} s (injβ‚‚ y) = βŠ†β†¦β†’β¨†codβŠ† (Ξ» {C} z β†’ s (injβ‚‚ z)) y

With the ⨆dom and ⨆cod functions in hand, we can make precise the conclusion of the inversion principle for functions, which we package into the following predicate named factor. We say that v ↦ w factors u into uβ€² if uβ€² is a included in u, if uβ€² contains only functions, its domain is less than v, and its codomain is greater than w.

factor : (u : Value) β†’ (uβ€² : Value) β†’ (v : Value) β†’ (w : Value) β†’ Set
factor u uβ€² v w = all-funs uβ€²  Γ—  uβ€² βŠ† u  Γ—  ⨆dom uβ€² βŠ‘ v  Γ—  w βŠ‘ ⨆cod uβ€²

So the inversion principle for functions can be stated as

  v ↦ w βŠ‘ u
  ---------------
β†’ factor u uβ€² v w

We prove the inversion principle for functions by induction on the derivation of the less-than relation. To make the induction hypothesis stronger, we broaden the premise v ↦ w βŠ‘ u to u₁ βŠ‘ uβ‚‚, and strengthen the conclusion to say that for every function value v ↦ w ∈ u₁, we have that v ↦ w factors uβ‚‚ into some value u₃.

β†’ u₁ βŠ‘ uβ‚‚
  ------------------------------------------------------
β†’ βˆ€{v w} β†’ v ↦ w ∈ u₁ β†’ Ξ£[ u₃ ∈ Value ] factor uβ‚‚ u₃ v w

Inversion of less-than for functions, the case for βŠ‘-trans

The crux of the proof is the case for βŠ‘-trans.

u₁ βŠ‘ u   u βŠ‘ uβ‚‚
--------------- (βŠ‘-trans)
    u₁ βŠ‘ uβ‚‚

By the induction hypothesis for u₁ βŠ‘ u, we know that v ↦ w factors u into uβ€², for some value uβ€², so we have all-funs uβ€² and uβ€² βŠ† u. By the induction hypothesis for u βŠ‘ uβ‚‚, we know that for any vβ€² ↦ wβ€² ∈ u, vβ€² ↦ wβ€² factors uβ‚‚ into u₃. With these facts in hand, we proceed by induction on uβ€² to prove that (⨆dom uβ€²) ↦ (⨆cod uβ€²) factors uβ‚‚ into u₃. We discuss each case of the proof in the text below.

sub-inv-trans : βˆ€{uβ€² uβ‚‚ u : Value}
    β†’ all-funs uβ€²  β†’  uβ€² βŠ† u
    β†’ (βˆ€{vβ€² wβ€²} β†’ vβ€² ↦ wβ€² ∈ u β†’ Ξ£[ u₃ ∈ Value ] factor uβ‚‚ u₃ vβ€² wβ€²)
      ---------------------------------------------------------------
    β†’ Ξ£[ u₃ ∈ Value ] factor uβ‚‚ u₃ (⨆dom uβ€²) (⨆cod uβ€²)
sub-inv-trans {βŠ₯} {uβ‚‚} {u} fuβ€² uβ€²βŠ†u IH =
   βŠ₯-elim (contradiction (fuβ€² refl) Β¬FunβŠ₯)
sub-inv-trans {u₁′ ↦ uβ‚‚β€²} {uβ‚‚} {u} fg uβ€²βŠ†u IH = IH (β†¦βŠ†β†’βˆˆ uβ€²βŠ†u)
sub-inv-trans {u₁′ βŠ” uβ‚‚β€²} {uβ‚‚} {u} fg uβ€²βŠ†u IH
    with βŠ”βŠ†-inv uβ€²βŠ†u
... | ⟨ uβ‚β€²βŠ†u , uβ‚‚β€²βŠ†u ⟩
    with sub-inv-trans {u₁′} {uβ‚‚} {u} (Ξ» {vβ€²} z β†’ fg (inj₁ z)) uβ‚β€²βŠ†u IH
       | sub-inv-trans {uβ‚‚β€²} {uβ‚‚} {u} (Ξ» {vβ€²} z β†’ fg (injβ‚‚ z)) uβ‚‚β€²βŠ†u IH
... | ⟨ u₃₁ , ⟨ fu21' , ⟨ uβ‚ƒβ‚βŠ†uβ‚‚ , ⟨ duβ‚ƒβ‚βŠ‘du₁′ , cuβ‚β€²βŠ‘cu₃₁ ⟩ ⟩ ⟩ ⟩
    | ⟨ u₃₂ , ⟨ fu22' , ⟨ uβ‚ƒβ‚‚βŠ†uβ‚‚ , ⟨ duβ‚ƒβ‚‚βŠ‘duβ‚‚β€² , cuβ‚β€²βŠ‘cu₃₂ ⟩ ⟩ ⟩ ⟩ =
      ⟨ (u₃₁ βŠ” u₃₂) , ⟨ fuβ‚‚β€² , ⟨ uβ‚‚β€²βŠ†uβ‚‚ ,
      ⟨ βŠ”βŠ‘βŠ” duβ‚ƒβ‚βŠ‘du₁′ duβ‚ƒβ‚‚βŠ‘duβ‚‚β€² ,
        βŠ”βŠ‘βŠ” cuβ‚β€²βŠ‘cu₃₁ cuβ‚β€²βŠ‘cu₃₂ ⟩ ⟩ ⟩ ⟩
    where fuβ‚‚β€² : {vβ€² : Value} β†’ vβ€² ∈ u₃₁ ⊎ vβ€² ∈ u₃₂ β†’ Fun vβ€²
          fuβ‚‚β€² {vβ€²} (inj₁ x) = fu21' x
          fuβ‚‚β€² {vβ€²} (injβ‚‚ y) = fu22' y
          uβ‚‚β€²βŠ†uβ‚‚ : {C : Value} β†’ C ∈ u₃₁ ⊎ C ∈ u₃₂ β†’ C ∈ uβ‚‚
          uβ‚‚β€²βŠ†uβ‚‚ {C} (inj₁ x) = uβ‚ƒβ‚βŠ†uβ‚‚ x
          uβ‚‚β€²βŠ†uβ‚‚ {C} (injβ‚‚ y) = uβ‚ƒβ‚‚βŠ†uβ‚‚ y

  • Suppose uβ€² ≑ βŠ₯. Then we have a contradiction because it is not the case that Fun βŠ₯.

  • Suppose uβ€² ≑ u₁′ ↦ uβ‚‚β€². Then u₁′ ↦ uβ‚‚β€² ∈ u and we can apply the premise (the induction hypothesis from u βŠ‘ uβ‚‚) to obtain that u₁′ ↦ uβ‚‚β€² factors of uβ‚‚ into uβ‚‚β€². This case is complete because ⨆dom uβ€² ≑ u₁′ and ⨆cod uβ€² ≑ uβ‚‚β€².

  • Suppose uβ€² ≑ u₁′ βŠ” uβ‚‚β€². Then we have u₁′ βŠ† u and uβ‚‚β€² βŠ† u. We also have all-funs u₁′ and all-funs uβ‚‚β€², so we can apply the induction hypothesis for both u₁′ and uβ‚‚β€². So there exists values u₃₁ and u₃₂ such that (⨆dom u₁′) ↦ (⨆cod u₁′) factors u into u₃₁ and (⨆dom uβ‚‚β€²) ↦ (⨆cod uβ‚‚β€²) factors u into u₃₂. We will show that (⨆dom u) ↦ (⨆cod u) factors u into u₃₁ βŠ” u₃₂. So we need to show that

      ⨆dom (u₃₁ βŠ” u₃₂) βŠ‘ ⨆dom (u₁′ βŠ” uβ‚‚β€²)
  ⨆cod (u₁′ βŠ” uβ‚‚β€²) βŠ‘ ⨆cod (u₃₁ βŠ” u₃₂)

    But those both follow directly from the factoring of u into u₃₁ and u₃₂, using the monotonicity of βŠ” with respect to βŠ‘.

Inversion of less-than for functions

We come to the proof of the main lemma concerning the inversion of less-than for functions. We show that if u₁ βŠ‘ uβ‚‚, then for any v ↦ w ∈ u₁, we can factor uβ‚‚ into u₃ according to v ↦ w. We proceed by induction on the derivation of u₁ βŠ‘ uβ‚‚, and describe each case in the text after the Agda proof.

sub-inv : βˆ€{u₁ uβ‚‚ : Value}
        β†’ u₁ βŠ‘ uβ‚‚
        β†’ βˆ€{v w} β†’ v ↦ w ∈ u₁
          -------------------------------------
        β†’ Ξ£[ u₃ ∈ Value ] factor uβ‚‚ u₃ v w
sub-inv {βŠ₯} {uβ‚‚} βŠ‘-bot {v} {w} ()
sub-inv {u₁₁ βŠ” u₁₂} {uβ‚‚} (βŠ‘-conj-L lt1 lt2) {v} {w} (inj₁ x) = sub-inv lt1 x
sub-inv {u₁₁ βŠ” u₁₂} {uβ‚‚} (βŠ‘-conj-L lt1 lt2) {v} {w} (injβ‚‚ y) = sub-inv lt2 y
sub-inv {u₁} {u₂₁ βŠ” uβ‚‚β‚‚} (βŠ‘-conj-R1 lt) {v} {w} m
    with sub-inv lt m
... | ⟨ u₃₁ , ⟨ fu₃₁ , ⟨ uβ‚ƒβ‚βŠ†u₂₁ , ⟨ domuβ‚ƒβ‚βŠ‘v , wβŠ‘codu₃₁ ⟩ ⟩ ⟩ ⟩ =
      ⟨ u₃₁ , ⟨ fu₃₁ , ⟨ (Ξ» {w} z β†’ inj₁ (uβ‚ƒβ‚βŠ†u₂₁ z)) ,
                                   ⟨ domuβ‚ƒβ‚βŠ‘v , wβŠ‘codu₃₁ ⟩ ⟩ ⟩ ⟩
sub-inv {u₁} {u₂₁ βŠ” uβ‚‚β‚‚} (βŠ‘-conj-R2 lt) {v} {w} m
    with sub-inv lt m
... | ⟨ u₃₂ , ⟨ fu₃₂ , ⟨ uβ‚ƒβ‚‚βŠ†uβ‚‚β‚‚ , ⟨ domuβ‚ƒβ‚‚βŠ‘v , wβŠ‘codu₃₂ ⟩ ⟩ ⟩ ⟩ =
      ⟨ u₃₂ , ⟨ fu₃₂ , ⟨ (Ξ» {C} z β†’ injβ‚‚ (uβ‚ƒβ‚‚βŠ†uβ‚‚β‚‚ z)) ,
                                   ⟨ domuβ‚ƒβ‚‚βŠ‘v , wβŠ‘codu₃₂ ⟩ ⟩ ⟩ ⟩
sub-inv {u₁} {uβ‚‚} (βŠ‘-trans{v = u} uβ‚βŠ‘u uβŠ‘uβ‚‚) {v} {w} v↦w∈u₁
    with sub-inv uβ‚βŠ‘u v↦w∈u₁
... | ⟨ uβ€² , ⟨ fuβ€² , ⟨ uβ€²βŠ†u , ⟨ domuβ€²βŠ‘v , wβŠ‘coduβ€² ⟩ ⟩ ⟩ ⟩
    with sub-inv-trans {uβ€²} fuβ€² uβ€²βŠ†u (sub-inv uβŠ‘uβ‚‚)
... | ⟨ u₃ , ⟨ fu₃ , ⟨ uβ‚ƒβŠ†uβ‚‚ , ⟨ domuβ‚ƒβŠ‘domuβ€² , coduβ€²βŠ‘codu₃ ⟩ ⟩ ⟩ ⟩ =
      ⟨ u₃ , ⟨ fu₃ , ⟨ uβ‚ƒβŠ†uβ‚‚ , ⟨ βŠ‘-trans domuβ‚ƒβŠ‘domuβ€² domuβ€²βŠ‘v ,
                                    βŠ‘-trans wβŠ‘coduβ€² coduβ€²βŠ‘codu₃ ⟩ ⟩ ⟩ ⟩
sub-inv {u₁₁ ↦ u₁₂} {u₂₁ ↦ uβ‚‚β‚‚} (βŠ‘-fun lt1 lt2) refl =
    ⟨ u₂₁ ↦ uβ‚‚β‚‚ , ⟨ (Ξ» {w} β†’ fun) , ⟨ (Ξ» {C} z β†’ z) , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩
sub-inv {u₂₁ ↦ (uβ‚‚β‚‚ βŠ” u₂₃)} {u₂₁ ↦ uβ‚‚β‚‚ βŠ” u₂₁ ↦ u₂₃} βŠ‘-dist
    {.u₂₁} {.(uβ‚‚β‚‚ βŠ” u₂₃)} refl =
    ⟨ u₂₁ ↦ uβ‚‚β‚‚ βŠ” u₂₁ ↦ u₂₃ , ⟨ f , ⟨ g , ⟨ βŠ‘-conj-L βŠ‘-refl βŠ‘-refl , βŠ‘-refl ⟩ ⟩ ⟩ ⟩
  where f : all-funs (u₂₁ ↦ uβ‚‚β‚‚ βŠ” u₂₁ ↦ u₂₃)
        f (inj₁ x) = fun x
        f (injβ‚‚ y) = fun y
        g : (u₂₁ ↦ uβ‚‚β‚‚ βŠ” u₂₁ ↦ u₂₃) βŠ† (u₂₁ ↦ uβ‚‚β‚‚ βŠ” u₂₁ ↦ u₂₃)
        g (inj₁ x) = inj₁ x
        g (injβ‚‚ y) = injβ‚‚ y

Let v and w be arbitrary values.

  • Case βŠ‘-bot. So u₁ ≑ βŠ₯. We have v ↦ w ∈ βŠ₯, but that is impossible.

  • Case βŠ‘-conj-L.

      u₁₁ βŠ‘ uβ‚‚   u₁₂ βŠ‘ uβ‚‚
  -------------------
  u₁₁ βŠ” u₁₂ βŠ‘ uβ‚‚

    Given that v ↦ w ∈ u₁₁ βŠ” u₁₂, there are two subcases to consider.

    • Subcase v ↦ w ∈ u₁₁. We conclude by the induction hypothesis for u₁₁ βŠ‘ uβ‚‚.

    • Subcase v ↦ w ∈ u₁₂. We conclude by the induction hypothesis for u₁₂ βŠ‘ uβ‚‚.

  • Case βŠ‘-conj-R1.

      u₁ βŠ‘ u₂₁
  --------------
  u₁ βŠ‘ u₂₁ βŠ” uβ‚‚β‚‚

    Given that v ↦ w ∈ u₁, the induction hypothesis for u₁ βŠ‘ u₂₁ gives us that v ↦ w factors u₂₁ into u₃₁ for some u₃₁. To show that v ↦ w also factors u₂₁ βŠ” uβ‚‚β‚‚ into u₃₁, we just need to show that u₃₁ βŠ† u₂₁ βŠ” uβ‚‚β‚‚, but that follows directly from u₃₁ βŠ† u₂₁.

  • Case βŠ‘-conj-R2. This case follows by reasoning similar to the case for βŠ‘-conj-R1.

  • Case βŠ‘-trans.

      u₁ βŠ‘ u   u βŠ‘ uβ‚‚
  ---------------
      u₁ βŠ‘ uβ‚‚

    By the induction hypothesis for u₁ βŠ‘ u, we know that v ↦ w factors u into uβ€², for some value uβ€², so we have all-funs uβ€² and uβ€² βŠ† u. By the induction hypothesis for u βŠ‘ uβ‚‚, we know that for any vβ€² ↦ wβ€² ∈ u, vβ€² ↦ wβ€² factors uβ‚‚. Now we apply the lemma sub-inv-trans, which gives us some u₃ such that (⨆dom uβ€²) ↦ (⨆cod uβ€²) factors uβ‚‚ into u₃. We show that v ↦ w also factors uβ‚‚ into u₃. From ⨆dom u₃ βŠ‘ ⨆dom uβ€² and ⨆dom uβ€² βŠ‘ v, we have ⨆dom u₃ βŠ‘ v. From w βŠ‘ ⨆cod uβ€² and ⨆cod uβ€² βŠ‘ ⨆cod u₃, we have w βŠ‘ ⨆cod u₃, and this case is complete.

  • Case βŠ‘-fun.

      u₂₁ βŠ‘ u₁₁  u₁₂ βŠ‘ uβ‚‚β‚‚
  ---------------------
  u₁₁ ↦ u₁₂ βŠ‘ u₂₁ ↦ uβ‚‚β‚‚

    Given that v ↦ w ∈ u₁₁ ↦ u₁₂, we have v ≑ u₁₁ and w ≑ u₁₂. We show that u₁₁ ↦ u₁₂ factors u₂₁ ↦ uβ‚‚β‚‚ into itself. We need to show that ⨆dom (u₂₁ ↦ uβ‚‚β‚‚) βŠ‘ u₁₁ and u₁₂ βŠ‘ ⨆cod (u₂₁ ↦ uβ‚‚β‚‚), but that is equivalent to our premises u₂₁ βŠ‘ u₁₁ and u₁₂ βŠ‘ uβ‚‚β‚‚.

  • Case βŠ‘-dist.

      ---------------------------------------------
  u₂₁ ↦ (uβ‚‚β‚‚ βŠ” u₂₃) βŠ‘ (u₂₁ ↦ uβ‚‚β‚‚) βŠ” (u₂₁ ↦ u₂₃)

    Given that v ↦ w ∈ u₂₁ ↦ (uβ‚‚β‚‚ βŠ” u₂₃), we have v ≑ u₂₁ and w ≑ uβ‚‚β‚‚ βŠ” u₂₃. We show that u₂₁ ↦ (uβ‚‚β‚‚ βŠ” u₂₃) factors (u₂₁ ↦ uβ‚‚β‚‚) βŠ” (u₂₁ ↦ u₂₃) into itself. We have u₂₁ βŠ” u₂₁ βŠ‘ u₂₁, and also uβ‚‚β‚‚ βŠ” u₂₃ βŠ‘ uβ‚‚β‚‚ βŠ” u₂₃, so the proof is complete.

We conclude this section with two corollaries of the sub-inv lemma. First, we have the following property that is convenient to use in later proofs. We specialize the premise to just v ↦ w βŠ‘ u₁ and we modify the conclusion to say that for every vβ€² ↦ wβ€² ∈ uβ‚‚, we have vβ€² βŠ‘ v.

sub-inv-fun : βˆ€{v w u₁ : Value}
    β†’ (v ↦ w) βŠ‘ u₁
      -----------------------------------------------------
    β†’ Ξ£[ uβ‚‚ ∈ Value ] all-funs uβ‚‚ Γ— uβ‚‚ βŠ† u₁
        Γ— (βˆ€{vβ€² wβ€²} β†’ (vβ€² ↦ wβ€²) ∈ uβ‚‚ β†’ vβ€² βŠ‘ v) Γ— w βŠ‘ ⨆cod uβ‚‚
sub-inv-fun{v}{w}{u₁} abc
    with sub-inv abc {v}{w} refl
... | ⟨ uβ‚‚ , ⟨ f , ⟨ uβ‚‚βŠ†u₁ , ⟨ db , cc ⟩ ⟩ ⟩ ⟩ =
      ⟨ uβ‚‚ , ⟨ f , ⟨ uβ‚‚βŠ†u₁ , ⟨ G , cc ⟩ ⟩ ⟩ ⟩
   where G : βˆ€{D E} β†’ (D ↦ E) ∈ uβ‚‚ β†’ D βŠ‘ v
         G{D}{E} m = βŠ‘-trans (βŠ†β†’βŠ‘ (β†¦βˆˆβ†’βŠ†β¨†dom f m)) db

The second corollary is the inversion rule that one would expect for less-than with functions on the left and right-hand sides.

β†¦βŠ‘β†¦-inv : βˆ€{v w vβ€² wβ€²}
        β†’ v ↦ w βŠ‘ vβ€² ↦ wβ€²
          -----------------
        β†’ vβ€² βŠ‘ v Γ— w βŠ‘ wβ€²
β†¦βŠ‘β†¦-inv{v}{w}{vβ€²}{wβ€²} lt
    with sub-inv-fun lt
... | ⟨ Ξ“ , ⟨ f , ⟨ Ξ“βŠ†v34 , ⟨ lt1 , lt2 ⟩ ⟩ ⟩ ⟩
    with all-funs∈ f
... | ⟨ u , ⟨ uβ€² , u↦uβ€²βˆˆΞ“ ⟩ ⟩
    with Ξ“βŠ†v34 u↦uβ€²βˆˆΞ“
... | refl =
  let ⨆codΞ“βŠ†wβ€² = βŠ†β†¦β†’β¨†codβŠ† Ξ“βŠ†v34 in
  ⟨ lt1 u↦uβ€²βˆˆΞ“ , βŠ‘-trans lt2 (βŠ†β†’βŠ‘ ⨆codΞ“βŠ†wβ€²) ⟩

Notes

The denotational semantics presented in this chapter is an example of a filter model (Barendregt, Coppo, Dezani-Ciancaglini, 1983). Filter models use type systems with intersection types to precisely characterize runtime behavior (Coppo, Dezani-Ciancaglini, and Salle, 1979). The notation that we use in this chapter is not that of type systems and intersection types, but the Value data type is isomorphic to types (↦ is β†’, βŠ” is ∧, βŠ₯ is ⊀), the βŠ‘ relation is the inverse of subtyping <:, and the evaluation relation ρ ⊒ M ↓ v is isomorphic to a type system. Write Ξ“ instead of ρ, A instead of v, and replace ↓ with : and one has a typing judgement Ξ“ ⊒ M : A. By varying the definition of subtyping and using different choices of type atoms, intersection type systems provide semantics for many different untyped Ξ» calculi, from full beta to the lazy and call-by-value calculi (Alessi, Barbanera, and Dezani-Ciancaglini, 2006) (Rocca and Paolini, 2004). The denotational semantics in this chapter corresponds to the BCD system (Barendregt, Coppo, Dezani-Ciancaglini, 1983). Part 3 of the book Lambda Calculus with Types describes a framework for intersection type systems that enables results similar to the ones in this chapter, but for the entire family of intersection type systems (Barendregt, Dekkers, and Statman, 2013).

The two ideas of using finite tables to represent functions and of relaxing table lookup to enable self application first appeared in a technical report by Gordon Plotkin (1972) and are later described in an article in Theoretical Computer Science (Plotkin 1993). In that work, the inductive definition of Value is a bit different than the one we use:

Value = C + β„˜f(Value) Γ— β„˜f(Value)

where C is a set of constants and β„˜f means finite powerset. The pairs in β„˜f(Value) Γ— β„˜f(Value) represent input-output mappings, just as in this chapter. The finite powersets are used to enable a function table to appear in the input and in the output. These differences amount to changing where the recursion appears in the definition of Value. Plotkin’s model is an example of a graph model of the untyped lambda calculus (Barendregt, 1984). In a graph model, the semantics is presented as a function from programs and environments to (possibly infinite) sets of values. The semantics in this chapter is instead defined as a relation, but set-valued functions are isomorphic to relations. Indeed, we present the semantics as a function in the next chapter and prove that it is equivalent to the relational version.

Dana Scott’s β„˜(Ο‰) (1976) and Engeler’s B(A) (1981) are two more examples of graph models. Both use the following inductive definition of Value.

Value = C + β„˜f(Value) Γ— Value

The use of Value instead of β„˜f(Value) in the output does not restrict expressiveness compared to Plotkin’s model because the semantics use sets of values and a pair of sets (V, Vβ€²) can be represented as a set of pairs { (V, vβ€²) | vβ€² ∈ Vβ€² }. In Scott’s β„˜(Ο‰), the above values are mapped to and from the natural numbers using a kind of Godel encoding.

References

  • Intersection Types and Lambda Models. Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini, Theoretical Compututer Science, vol. 355, pages 108-126, 2006.

  • The Lambda Calculus. H.P. Barendregt, 1984.

  • A filter lambda model and the completeness of type assignment. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini, Journal of Symbolic Logic, vol. 48, pages 931-940, 1983.

  • Lambda Calculus with Types. Henk Barendregt, Wil Dekkers, and Richard Statman, Cambridge University Press, Perspectives in Logic, 2013.

  • Functional characterization of some semantic equalities inside Ξ»-calculus. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Patrick Salle, in Sixth Colloquium on Automata, Languages and Programming. Springer, pages 133–146, 1979.

  • Algebras and combinators. Erwin Engeler, Algebra Universalis, vol. 13, pages 389-392, 1981.

  • A Set-Theoretical Definition of Application. Gordon D. Plotkin, University of Edinburgh, Technical Report MIP-R-95, 1972.

  • Set-theoretical and other elementary models of the Ξ»-calculus. Gordon D. Plotkin, Theoretical Computer Science, vol. 121, pages 351-409, 1993.

  • The Parametric Lambda Calculus. Simona Ronchi Della Rocca and Luca Paolini, Springer, 2004.

  • Data Types as Lattices. Dana Scott, SIAM Journal on Computing, vol. 5, pages 522-587, 1976.

Unicode

This chapter uses the following unicode:

βŠ₯  U+22A5  UP TACK (\bot)
↦  U+21A6  RIGHTWARDS ARROW FROM BAR (\mapsto)
βŠ”  U+2294  SQUARE CUP (\lub)
βŠ‘  U+2291  SQUARE IMAGE OF OR EQUAL TO (\sqsubseteq)
⨆ U+2A06  N-ARY SQUARE UNION OPERATOR (\Lub)
⊒  U+22A2  RIGHT TACK (\|- or \vdash)
↓  U+2193  DOWNWARDS ARROW (\d)
ᢜ  U+1D9C  MODIFIER LETTER SMALL C (\^c)
β„°  U+2130  SCRIPT CAPITAL E (\McE)
≃  U+2243  ASYMPTOTICALLY EQUAL TO (\~- or \simeq)
∈  U+2208  ELEMENT OF (\in)
βŠ†  U+2286  SUBSET OF OR EQUAL TO (\sub= or \subseteq)