Denotational: Denotational semantics of untyped lambda calculus π§
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 functionsastables. 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 selfapplication, 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 selfapplication, 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 selfapplication, 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β; congapp) 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; substzero; _[_]) open import plfa.part2.Substitution using (Rename; extensionality; renameid)
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 inputoutput
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 inputoutput mapping, from inputv
to outputw
. 
A value of the form
v β w
is a function that maps inputs to outputs according to bothv
andw
. 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 selfapplication.
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 βconjL : β {u v w} β v β u β w β u  β (v β w) β u βconjR1 : β {u v w} β u β v  β u β (v β w) βconjR2 : β {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 higherorder argument
vβ² β¦ wβ²
to a table entry whose input is v β¦ w
. Considering a
call to the higherorder 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β} = βconjL (βconjR1 βrefl) (βconjR2 β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β = βconjL (βconjR1 dβ) (βconjR2 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 (βconjR1 βrefl) βrefl) (βfun (βconjR2 β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 (βconjL lt1 lt2) = lt1 ββinvL (βconjR1 lt) = βconjR1 (ββinvL lt) ββinvL (βconjR2 lt) = βconjR2 (ββinvL lt) ββinvL (βtrans lt1 lt2) = βtrans (ββinvL lt1) lt2 ββinvR : β{u v w : Value} β u β v β w  β v β w ββinvR (βconjL lt1 lt2) = lt2 ββinvR (βconjR1 lt) = βconjR1 (ββinvR lt) ββinvR (βconjR2 lt) = βconjR2 (ββ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 initlast : β {Ξ} β (Ξ³ : Env (Ξ , β )) β Ξ³ β‘ (init Ξ³ `, last Ξ³) initlast {Ξ} Ξ³ = extensionality lemma where lemma : β (x : Ξ , β β β ) β Ξ³ x β‘ (init Ξ³ `, last Ξ³) x lemma Z = refl lemma (S x) = refl
We extend the β
relation pointwise 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 pointwise join of their values.
`β₯ : β {Ξ} β Env Ξ `β₯ x = β₯ _`β_ : β {Ξ} β Env Ξ β Env Ξ β Env Ξ (Ξ³ `β Ξ΄) x = Ξ³ x β Ξ΄ x
The βrefl
, βconjR1
, and βconjR2
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} βenvconjR1 : β {Ξ} β (Ξ³ : Env Ξ) β (Ξ΄ : Env Ξ) β Ξ³ `β (Ξ³ `β Ξ΄) βenvconjR1 Ξ³ Ξ΄ x = βconjR1 βrefl βenvconjR2 : β {Ξ} β (Ξ³ : Env Ξ) β (Ξ΄ : Env Ξ) β Ξ΄ `β (Ξ³ `β Ξ΄) βenvconjR2 Ξ³ Ξ΄ x = βconjR2 β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 bigstep 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 singleentry 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
denotid1 : β {Ξ³} β Ξ³ β’ id β β₯ β¦ β₯ denotid1 = β¦intro var denotid2 : β {Ξ³} β Ξ³ β’ id β (β₯ β¦ β₯) β¦ (β₯ β¦ β₯) denotid2 = β¦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 preevaluates 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
(β₯ β¦ β₯) β¦ (β₯ β¦ β₯)
.
denotid3 : `β β’ id β (β₯ β¦ β₯) β (β₯ β¦ β₯) β¦ (β₯ β¦ β₯) denotid3 = βintro denotid1 denotid2
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
.
idappid : β {u : Value} β `β β’ id Β· id β (u β¦ u) idappid {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 βconjR1 and
βconjR2 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.
denottwoαΆ : β{u v w : Value} β `β β’ twoαΆ β ((u β¦ v β v β¦ w) β¦ u β¦ w) denottwoαΆ {u}{v}{w} = β¦intro (β¦intro (β¦elim (sub var lt1) (β¦elim (sub var lt2) var))) where lt1 : v β¦ w β u β¦ v β v β¦ w lt1 = βconjR2 (βfun βrefl βrefl) lt2 : u β¦ v β u β¦ v β v β¦ w lt2 = (βconjR1 (β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 (βconjR1 βrefl)) (sub var (βconjR2 β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
nonterminating 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 selfapplication 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 denotplusαΆ
(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 ifandonlyif, 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 termN
.  termination:
M ββ Ζ N
for some termN
.
We can also characterize divergence and termination using denotations.
 divergence:
Β¬ (β β’ M β v β¦ w)
for anyv
andw
.  termination:
β β’ M β v β¦ w
for somev
andw
.
Alternatively, we can use the denotation function β°
.
 divergence:
Β¬ (β° M β β° (Ζ N))
for any termN
.  termination:
β° M β β° (Ζ N)
for some termN
.
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 lessthan 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 thatv β‘ v
, which we have byrefl
. 
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 Ξ΄
.
renamepres : β {Ξ Ξ v} {Ξ³ : Env Ξ} {Ξ΄ : Env Ξ} {M : Ξ β’ β } β (Ο : Rename Ξ Ξ) β Ξ³ `β (Ξ΄ β Ο) β Ξ³ β’ M β v  β Ξ΄ β’ (rename Ο M) β v renamepres Ο lt (var {x = x}) = sub var (lt x) renamepres Ο lt (β¦elim d dβ) = β¦elim (renamepres Ο lt d) (renamepres Ο lt dβ) renamepres Ο lt (β¦intro d) = β¦intro (renamepres (ext Ο) (extβ Ο lt) d) renamepres Ο lt β₯intro = β₯intro renamepres Ο lt (βintro d dβ) = βintro (renamepres Ο lt d) (renamepres Ο lt dβ) renamepres Ο lt (sub d ltβ²) = sub (renamepres Ο 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
renameid
lemma to obtain Ξ΄ β’ M β v
.
βenv : β {Ξ} {Ξ³ : Env Ξ} {Ξ΄ : Env Ξ} {M v} β Ξ³ β’ M β v β Ξ³ `β Ξ΄  β Ξ΄ β’ M β v βenv{Ξ}{Ξ³}{Ξ΄}{M}{v} d lt with renamepres{Ξ}{Ξ}{v}{Ξ³}{Ξ΄}{M} (Ξ» {A} x β x) lt d ...  Ξ΄β’id[M]βv rewrite renameid {Ξ}{β }{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.
upenv : β {Ξ} {Ξ³ : Env Ξ} {M v uβ uβ} β (Ξ³ `, uβ) β’ M β v β uβ β uβ  β (Ξ³ `, uβ) β’ M β v upenv d lt = βenv d (extle lt) where extle : β {Ξ³ uβ uβ} β uβ β uβ β (Ξ³ `, uβ) `β (Ξ³ `, uβ) extle lt Z = lt extle lt (S n) = βrefl
Exercise denotchurch
(recommended)
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 nonempty vector. (This formulation is more convenient for our purposes than the one in the Agda standard library.)
veclast : β{n : β} β Vec Value (suc n) β Value veclast {0} (a β· []) = a veclast {suc n} (a β· b β· ls) = veclast (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)) β¦ (veclast (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 byD^suc
, and the start of the path (last of the vector). It returns then + 1
vertex in the path.(D^suc (suc n) (a[n+1] β· a[n] β· ls)) β¦ (veclast (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 applyn
.
applyn : (n : β) β β , β , β β’ β applyn zero = # 0 applyn (suc n) = # 1 Β· applyn n church : (n : β) β β β’ β church n = Ζ Ζ applyn n
Prove the following theorem.
denotchurch : β{n : β}{ls : Vec Value (suc n)}
β `β
β’ church n β DαΆ n ls
 Your code goes here
Inversion of the lessthan 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 lessthan 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 βconjR1
and βconjR2
,
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 lessthan relation. They are narrower relations in that they imply the lessthan 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) = βconjR1 (βββ x) βββ {u} {v β w} (injβ y) = βconjR2 (βββ 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 = βconjL (βββ (Ξ» 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 allfuns v
if all the elements
of v
are functions.
data Fun : Value β Set where fun : β{u v w} β u β‘ (v β¦ w) β Fun u allfuns : Value β Set allfuns v = β{u} β u β v β Fun u
The value β₯
is not a function.
Β¬Funβ₯ : Β¬ (Fun β₯) Β¬Funβ₯ (fun ())
In our valuesassets 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.
allfunsβ : β{u} β allfuns u β Ξ£[ v β Value ] Ξ£[ w β Value ] v β¦ w β u allfunsβ {β₯} f with f {β₯} refl ...  fun () allfunsβ {v β¦ w} f = β¨ v , β¨ w , refl β© β© allfunsβ {u β uβ²} f with allfunsβ Ξ» z β f (injβ z) ...  β¨ v , β¨ w , m β© β© = β¨ v , β¨ w , (injβ m) β© β©
Domains and codomains
Returning to our goal, the inversion principle for lessthan 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} β allfuns 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 = allfuns 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 lessthan 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 lessthan 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 allfuns 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.
subinvtrans : β{uβ² uβ u : Value} β allfuns uβ² β uβ² β u β (β{vβ² wβ²} β vβ² β¦ wβ² β u β Ξ£[ uβ β Value ] factor uβ uβ vβ² wβ²)  β Ξ£[ uβ β Value ] factor uβ uβ (β¨dom uβ²) (β¨cod uβ²) subinvtrans {β₯} {uβ} {u} fuβ² uβ²βu IH = β₯elim (contradiction (fuβ² refl) Β¬Funβ₯) subinvtrans {uββ² β¦ uββ²} {uβ} {u} fg uβ²βu IH = IH (β¦βββ uβ²βu) subinvtrans {uββ² β uββ²} {uβ} {u} fg uβ²βu IH with ββinv uβ²βu ...  β¨ uββ²βu , uββ²βu β© with subinvtrans {uββ²} {uβ} {u} (Ξ» {vβ²} z β fg (injβ z)) uββ²βu IH  subinvtrans {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 thatFun β₯
. 
Suppose
uβ² β‘ uββ² β¦ uββ²
. Thenuββ² β¦ uββ² β u
and we can apply the premise (the induction hypothesis fromu β uβ
) to obtain thatuββ² β¦ uββ²
factors ofuβ into uββ²
. This case is complete becauseβ¨dom uβ² β‘ uββ²
andβ¨cod uβ² β‘ uββ²
. 
Suppose
uβ² β‘ uββ² β uββ²
. Then we haveuββ² β u
anduββ² β u
. We also haveallfuns uββ²
andallfuns uββ²
, so we can apply the induction hypothesis for bothuββ²
anduββ²
. So there exists valuesuββ
anduββ
such that(β¨dom uββ²) β¦ (β¨cod uββ²)
factorsu
intouββ
and(β¨dom uββ²) β¦ (β¨cod uββ²)
factorsu
intouββ
. We will show that(β¨dom u) β¦ (β¨cod u)
factorsu
intouββ β 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
intouββ
anduββ
, using the monotonicity ofβ
with respect toβ
.
Inversion of lessthan for functions
We come to the proof of the main lemma concerning the inversion of
lessthan 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.
subinv : β{uβ uβ : Value} β uβ β uβ β β{v w} β v β¦ w β uβ  β Ξ£[ uβ β Value ] factor uβ uβ v w subinv {β₯} {uβ} βbot {v} {w} () subinv {uββ β uββ} {uβ} (βconjL lt1 lt2) {v} {w} (injβ x) = subinv lt1 x subinv {uββ β uββ} {uβ} (βconjL lt1 lt2) {v} {w} (injβ y) = subinv lt2 y subinv {uβ} {uββ β uββ} (βconjR1 lt) {v} {w} m with subinv lt m ...  β¨ uββ , β¨ fuββ , β¨ uβββuββ , β¨ domuβββv , wβcoduββ β© β© β© β© = β¨ uββ , β¨ fuββ , β¨ (Ξ» {w} z β injβ (uβββuββ z)) , β¨ domuβββv , wβcoduββ β© β© β© β© subinv {uβ} {uββ β uββ} (βconjR2 lt) {v} {w} m with subinv lt m ...  β¨ uββ , β¨ fuββ , β¨ uβββuββ , β¨ domuβββv , wβcoduββ β© β© β© β© = β¨ uββ , β¨ fuββ , β¨ (Ξ» {C} z β injβ (uβββuββ z)) , β¨ domuβββv , wβcoduββ β© β© β© β© subinv {uβ} {uβ} (βtrans{v = u} uββu uβuβ) {v} {w} vβ¦wβuβ with subinv uββu vβ¦wβuβ ...  β¨ uβ² , β¨ fuβ² , β¨ uβ²βu , β¨ domuβ²βv , wβcoduβ² β© β© β© β© with subinvtrans {uβ²} fuβ² uβ²βu (subinv uβuβ) ...  β¨ uβ , β¨ fuβ , β¨ uββuβ , β¨ domuββdomuβ² , coduβ²βcoduβ β© β© β© β© = β¨ uβ , β¨ fuβ , β¨ uββuβ , β¨ βtrans domuββdomuβ² domuβ²βv , βtrans wβcoduβ² coduβ²βcoduβ β© β© β© β© subinv {uββ β¦ uββ} {uββ β¦ uββ} (βfun lt1 lt2) refl = β¨ uββ β¦ uββ , β¨ (Ξ» {w} β fun) , β¨ (Ξ» {C} z β z) , β¨ lt1 , lt2 β© β© β© β© subinv {uββ β¦ (uββ β uββ)} {uββ β¦ uββ β uββ β¦ uββ} βdist {.uββ} {.(uββ β uββ)} refl = β¨ uββ β¦ uββ β uββ β¦ uββ , β¨ f , β¨ g , β¨ βconjL βrefl βrefl , βrefl β© β© β© β© where f : allfuns (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
. Souβ β‘ β₯
. We havev β¦ w β β₯
, but that is impossible. 
Case
βconjL
.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 foruββ β uβ
. 
Subcase
v β¦ w β uββ
. We conclude by the induction hypothesis foruββ β uβ
.


Case
βconjR1
.uβ β uββ  uβ β uββ β uββ
Given that
v β¦ w β uβ
, the induction hypothesis foruβ β uββ
gives us thatv β¦ w
factorsuββ
intouββ
for someuββ
. To show thatv β¦ w
also factorsuββ β uββ
intouββ
, we just need to show thatuββ β uββ β uββ
, but that follows directly fromuββ β uββ
. 
Case
βconjR2
. This case follows by reasoning similar to the case forβconjR1
. 
Case
βtrans
.uβ β u u β uβ  uβ β uβ
By the induction hypothesis for
uβ β u
, we know thatv β¦ w
factorsu
intouβ²
, for some valueuβ²
, so we haveallfuns uβ²
anduβ² β u
. By the induction hypothesis foru β uβ
, we know that for anyvβ² β¦ wβ² β u
,vβ² β¦ wβ²
factorsuβ
. Now we apply the lemma subinvtrans, which gives us someuβ
such that(β¨dom uβ²) β¦ (β¨cod uβ²)
factorsuβ
intouβ
. We show thatv β¦ w
also factorsuβ
intouβ
. Fromβ¨dom uβ β β¨dom uβ²
andβ¨dom uβ² β v
, we haveβ¨dom uβ β v
. Fromw β β¨cod uβ²
andβ¨cod uβ² β β¨cod uβ
, we havew β β¨cod uβ
, and this case is complete. 
Case
βfun
.uββ β uββ uββ β uββ  uββ β¦ uββ β uββ β¦ uββ
Given that
v β¦ w β uββ β¦ uββ
, we havev β‘ uββ
andw β‘ uββ
. We show thatuββ β¦ uββ
factorsuββ β¦ uββ
into itself. We need to show thatβ¨dom (uββ β¦ uββ) β uββ
anduββ β β¨cod (uββ β¦ uββ)
, but that is equivalent to our premisesuββ β uββ
anduββ β uββ
. 
Case
βdist
. uββ β¦ (uββ β uββ) β (uββ β¦ uββ) β (uββ β¦ uββ)
Given that
v β¦ w β uββ β¦ (uββ β uββ)
, we havev β‘ uββ
andw β‘ uββ β uββ
. We show thatuββ β¦ (uββ β uββ)
factors(uββ β¦ uββ) β (uββ β¦ uββ)
into itself. We haveuββ β uββ β uββ
, and alsouββ β uββ β uββ β uββ
, so the proof is complete.
We conclude this section with two corollaries of the subinv 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
.
subinvfun : β{v w uβ : Value} β (v β¦ w) β uβ  β Ξ£[ uβ β Value ] allfuns uβ Γ uβ β uβ Γ (β{vβ² wβ²} β (vβ² β¦ wβ²) β uβ β vβ² β v) Γ w β β¨cod uβ subinvfun{v}{w}{uβ} abc with subinv 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 lessthan with functions on the left and righthand sides.
β¦ββ¦inv : β{v w vβ² wβ²} β v β¦ w β vβ² β¦ wβ²  β vβ² β v Γ w β wβ² β¦ββ¦inv{v}{w}{vβ²}{wβ²} lt with subinvfun lt ...  β¨ Ξ , β¨ f , β¨ Ξβv34 , β¨ lt1 , lt2 β© β© β© β© with allfunsβ 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, DezaniCiancaglini, 1983). Filter
models use type systems with intersection types to precisely
characterize runtime behavior (Coppo, DezaniCiancaglini, 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 callbyvalue calculi
(Alessi, Barbanera, and DezaniCiancaglini, 2006) (Rocca and Paolini, 2004).
The denotational semantics in this chapter corresponds to the BCD
system (Barendregt, Coppo, DezaniCiancaglini, 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 inputoutput 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 setvalued 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 DezaniCiancaglini, Theoretical Compututer Science, vol. 355, pages 108126, 2006.

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

A filter lambda model and the completeness of type assignment. Henk Barendregt, Mario Coppo, and Mariangiola DezaniCiancaglini, Journal of Symbolic Logic, vol. 48, pages 931940, 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 DezaniCiancaglini, 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 389392, 1981.

A SetTheoretical Definition of Application. Gordon D. Plotkin, University of Edinburgh, Technical Report MIPR95, 1972.

Settheoretical and other elementary models of the Ξ»calculus. Gordon D. Plotkin, Theoretical Computer Science, vol. 121, pages 351409, 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 522587, 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 NARY 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)