my forest
add PCF
+172
-5
+2
-4
trees/dt/dt-001Z.tree
+2
-4
trees/dt/dt-001Z.tree
···
3
3
\taxon{Lecture}
4
4
\title{Constructions on [cpos](dt-001D) and PCF}
5
5
\author{liamoc}
6
-
\p{This lecture is based on material from [[haskellhutt]], [[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
6
+
\p{This lecture is based on material from [[haskellhutt]], [[jlongley]],[[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
7
7
\transclude{dt-002K}
8
8
\transclude{dt-002Z}
9
9
\transclude{dt-0030}
10
10
\transclude{dt-003E}
11
-
\subtree{
12
-
\title{PCF}
13
-
}
11
+
\transclude{dt-003T}
+13
trees/dt/dt-003M.tree
+13
trees/dt/dt-003M.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{The language PCF}
5
+
\p{
6
+
The language for \strong{P}rogramming \strong{C}omputable \strong{F}unctions (PCF) is a variant of typed #{\lambda}-calculus with minimal extensions to be Turing-complete.
7
+
##{
8
+
\begin{array}{lcl}
9
+
e & \Coloneqq & n \mid x \mid \lambda x : \tau.\ e \mid e_1\ e_2\mid\mathsf{succ} \mid \mathsf{pred} \mid \mathsf{ifz}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \mid \mathsf{fix}\ x : \tau.\ e \\
10
+
\tau & \Coloneqq & \mathsf{nat} \mid \tau_1 \rightarrow \tau_2
11
+
\end{array}
12
+
}
13
+
}
+16
trees/dt/dt-003N.tree
+16
trees/dt/dt-003N.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{Typing rules for [PCF](dt-003M)}
5
+
\p{
6
+
##{
7
+
\inferrule{n \in \mathbb{N}}{\Gamma \vdash n : \mathsf{nat}}\quad
8
+
\inferrule{x : \tau \in \Gamma}{\Gamma \vdash x : \tau}\quad
9
+
\inferrule{\Gamma, x : \tau_1 \vdash e : \tau_2 }{ \Gamma \vdash \lambda x : \tau_1.\ e : \tau_1 \rightarrow \tau_2}\quad
10
+
\inferrule{\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \quad \Gamma \vdash e_2 : \tau_1}{\Gamma \vdash e_1\ e_2 : \tau_2}\\[2em]
11
+
\inferrule{ }{ \Gamma \vdash \mathsf{succ} : \mathsf{nat} \rightarrow \mathsf{nat}}\quad
12
+
\inferrule{ }{ \Gamma \vdash \mathsf{pred} : \mathsf{nat} \rightarrow \mathsf{nat}}\quad
13
+
\inferrule{ \Gamma \vdash e_1 : \mathsf{nat} \quad \Gamma \vdash e_2 : \tau \quad \Gamma \vdash e_3 : \tau }{ \Gamma \vdash \mathsf{ifz}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 : \tau}\quad
14
+
\inferrule{ \Gamma, x : \tau \vdash e : \tau }{\Gamma \vdash \mathsf{fix}\ x : \tau.\ e : \tau}
15
+
}
16
+
}
+21
trees/dt/dt-003O.tree
+21
trees/dt/dt-003O.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{Type-dependent denotations}
4
+
\p{
5
+
Because [PCF](dt-003M) is [typed](dt-003N), we shall assign denotations only to well-typed expressions.
6
+
The range of our [denotation function](dt-0001) for expressions is determined by the \em{type} of its input expression. That is, the denotation of a type #{\tau} \em{is} the [cpo](dt-001D) whose elements will be the denotations of expressions of type #{\tau}.
7
+
8
+
The denotation of the type #{\mathsf{nat}}, then, is merely the [flat domain](dt-0008) of the natural numbers #{\mathbb{N}_\bot}:
9
+
##{
10
+
\llbracket \mathsf{nat} \rrbracket = \mathbb{N}_\bot
11
+
}
12
+
And, the denotation of the function type is the domain of [continuous functions](dt-002F) on cpos:
13
+
##{
14
+
\llbracket \tau_1 \rightarrow \tau_2 \rrbracket = \llbracket \tau_1 \rrbracket \contto \llbracket \tau_2 \rrbracket
15
+
}
16
+
A \em{closed} term #{e : \tau} with no free variables denotes an element of #{\llbracket \tau \rrbracket}, so we might be tempted to define our denotation function for expressions #{e : \tau} like so: ##{\llbracket e \rrbracket : \llbracket \tau \rrbracket}
17
+
However, if #{e : \tau} involves free variables from our context #{\Gamma}, the valuation of #{e} will depend on the values assigned to all the variables. Thus, the denotation of a typed expression #{\Gamma \vdash e : \tau} is defined instead as a [continuous](dt-001J) function:
18
+
##{\llbracket e \rrbracket_\Gamma : \llbracket \Gamma \rrbracket \contto \llbracket \tau \rrbracket}
19
+
where the meaning of a context #{\Gamma = (x_0 : \tau_0, x_1 : \tau_1,\dots, x_n : \tau_n)} will be a a big #{n}-tuple of the values assigned to each variable:
20
+
##{\llbracket \Gamma \rrbracket = \llbracket \tau_0 \rrbracket \times \llbracket \tau_1 \rrbracket \times \cdots \times \llbracket \tau_n \rrbracket}
21
+
}
+31
trees/dt/dt-003P.tree
+31
trees/dt/dt-003P.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\title{Semantics of [PCF](dt-003M)}
5
+
\subblock{Types}{
6
+
##{
7
+
\begin{array}{lcl}
8
+
\llbracket \mathsf{nat} \rrbracket &=& \mathbb{N}_\bot\\
9
+
\llbracket \tau_1 \rightarrow \tau_2 \rrbracket &=& \llbracket \tau_1 \rrbracket \contto \llbracket \tau_2 \rrbracket
10
+
\end{array}
11
+
}}
12
+
\subblock{Expressions}{
13
+
For #{\Gamma : e : \tau}, we have #{\llbracket e \rrbracket_\Gamma : \llbracket \tau \rrbracket } defined as follows:
14
+
##{
15
+
\begin{array}{lcl}
16
+
\llbracket n \rrbracket_\Gamma(\vec{z}) & =& n\\
17
+
\llbracket x \rrbracket_\Gamma(\vec{z}) & = & z_j\ \text{where}\ j\ \text{is largest}\ j\ \text{s.t.}\ x = x_j \\
18
+
\llbracket \lambda x : \tau_1.\ e \rrbracket_\Gamma(\vec{z}) & = & (\boldsymbol{\lambda} v \in \llbracket \tau_1 \rrbracket.\ \llbracket e\rrbracket_{\Gamma, x : \tau_1}(\vec{z}, v))\\
19
+
\llbracket e_1\ e_2 \rrbracket_\Gamma(\vec{z}) & = & \llbracket e_1 \rrbracket_\Gamma(\vec{z})(\llbracket e_2 \rrbracket_\Gamma(\vec{z}))\\
20
+
\llbracket \mathsf{succ} \rrbracket_\Gamma(\vec{z}) & = & (\boldsymbol{\lambda} v \in \mathbb{N}_\bot.\ v + 1)\\
21
+
\llbracket \mathsf{pred} \rrbracket_\Gamma(\vec{z}) & = & (\boldsymbol{\lambda} v \in \mathbb{N}_\bot.\ v - 1)\\
22
+
\llbracket \mathsf{ifz}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \rrbracket_\Gamma(\vec{z}) & = & \begin{cases}
23
+
\llbracket e_2 \rrbracket_\Gamma(\vec{z}) & \text{if}\ \llbracket e_1 \rrbracket_\Gamma(\vec{z}) > 0 \\
24
+
\llbracket e_3 \rrbracket_\Gamma(\vec{z}) & \text{if}\ \llbracket e_1 \rrbracket_\Gamma(\vec{z}) = 0 \\
25
+
\bot & \text{if}\ \llbracket e_1 \rrbracket_\Gamma(\vec{z}) = \bot
26
+
\end{cases}\\
27
+
\llbracket \mathsf{fix}\ x : \tau.\ e \rrbracket_\Gamma(\vec{z}) &= & \mathbf{fix}(\boldsymbol{\lambda} v \in \llbracket \tau \rrbracket.\ \llbracket e\rrbracket_{\Gamma, x : \tau}(\vec{z}, v))
28
+
\end{array}
29
+
}
30
+
In the above definitions a boldface lambda #{\boldsymbol{\lambda}} is used for an anonymous [continuous function](dt-001J) — boldface to distinguish it from the lambda in the [syntax of PCF](dt-003M). Verifying that these functions are indeed [continuous](dt-001J) is straightforward, but is necessary to justify the use of [the #{\mathbf{fix}} operator](dt-001Q).
31
+
}
+8
trees/dt/dt-003Q.tree
+8
trees/dt/dt-003Q.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\title{Notation for #{n}-tuples}
5
+
\p{Given an #{n}-tuple, i.e. elements of the #{n}-ary [product](dm-0005) #{X_0 \times X_1 \times X_2 \times \dots \times X_n}, we typically denote the entire #{n}-tuple as in vector notation: ##{\vec{x} : X_0 \times X_1 \times X_2 \times \dots \times X_n}
6
+
And individual elements of the tuple are accessed with numeric subscripts:
7
+
##{x_0 : X_0 \quad x_2 : X_2 \quad \cdots}
8
+
}
+25
trees/dt/dt-003R.tree
+25
trees/dt/dt-003R.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{Extending [PCF](dt-003M) with product types}
4
+
\p{We shall extend [the syntax of PCF](dt-003M) with a new type former, #{\tau_1 \times \tau_2} and three expression-level constructs for constructing and deconstructing pairs:
5
+
##{
6
+
\begin{array}{lcl}
7
+
e & \Coloneqq & \cdots \mid (e_1,e_2) \mid \mathsf{fst}\ e \mid \mathsf{snd}\ e \\
8
+
\tau & \Coloneqq & \cdots \mid \tau_1 \times \tau_2
9
+
\end{array}
10
+
}
11
+
Adding to our [typing rules](dt-003N) similarly:
12
+
##{
13
+
\inferrule{\Gamma \vdash e_1 : \tau_1 \quad e_2 : \tau_2}{(e_1,e_2) : \tau_1 \times \tau_2}\\[2em]
14
+
\inferrule{\Gamma \vdash e : \tau_1 \times \tau_2}{\Gamma \vdash \mathsf{fst}\ e : \tau_1}\quad
15
+
\inferrule{\Gamma \vdash e : \tau_1 \times \tau_2}{\Gamma \vdash \mathsf{snd}\ e : \tau_2}
16
+
}
17
+
To extend our [semantics](dt-003P), we make the product type #{\tau_1 \times \tau_2} denote the [product cpo](dt-0021) #{\llbracket \tau_1 \rrbracket \times \llbracket \tau_2 \rrbracket}, and our expression semantics are expressed straightforwardly using our [projection](dt-0020) and [split](dt-0023) operations for [products](dt-002K):
18
+
##{
19
+
\begin{array}{lcl}
20
+
\llbracket (e_1, e_2) \rrbracket_\Gamma &=& \langle \llbracket e_1 \rrbracket_\Gamma, \llbracket e_2 \rrbracket_\Gamma \rangle \\
21
+
\llbracket \mathsf{fst}\ e \rrbracket_\Gamma & = & \pi_0 \circ \llbracket e \rrbracket_\Gamma \\
22
+
\llbracket \mathsf{snd}\ e \rrbracket_\Gamma & = & \pi_1 \circ \llbracket e \rrbracket_\Gamma \\
23
+
\end{array}
24
+
}
25
+
}
+29
trees/dt/dt-003S.tree
+29
trees/dt/dt-003S.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{Extending [PCF](dt-003M) with sum types}
4
+
\p{We shall extend [the syntax of PCF](dt-003M) with a new type former, #{\tau_1 + \tau_2} and three expression-level constructs for constructing and deconstructing sums:
5
+
##{
6
+
\begin{array}{lcl}
7
+
e & \Coloneqq & \cdots \mid \mathsf{inl}\ e \mid \mathsf{inr}\ e \mid \mathsf{case}\ e_0\ \mathsf{of}\ \mathsf{inl}\ x \rightarrow e_1 ; \mathsf{inr}\ y \rightarrow e_2 \\
8
+
\tau & \Coloneqq & \cdots \mid \tau_1 + \tau_2
9
+
\end{array}
10
+
}
11
+
Adding to our [typing rules](dt-003N) similarly:
12
+
##{
13
+
\inferrule{\Gamma \vdash e : \tau_1}{\Gamma \vdash \mathsf{inl}\ e : \tau_1 + \tau_2}\quad
14
+
\inferrule{\Gamma \vdash e : \tau_2}{\Gamma \vdash \mathsf{inr}\ e : \tau_1 + \tau_2}\\[2em]
15
+
\inferrule{\Gamma \vdash e_0 : \tau_1 + \tau_2 \quad \Gamma, x : \tau_1 \vdash e_1 : \tau \quad \Gamma, y : \tau_2 \vdash e_2 : \tau}{ \Gamma \vdash \mathsf{case}\ e_0\ \mathsf{of}\ \mathsf{inl}\ x \rightarrow e_1 ; \mathsf{inr}\ y \rightarrow e_2 : \tau}
16
+
}
17
+
To extend our [semantics](dt-003P), we make the sum type #{\tau_1 + \tau_2} denote the [sum cpo](dt-0031) #{\llbracket \tau_1 \rrbracket + \llbracket \tau_2 \rrbracket}, and our expression semantics are expressed using our [primitive functions for sums](dt-003D).
18
+
##{
19
+
\begin{array}{lcl}
20
+
\llbracket \mathsf{inl}\ e \rrbracket_\Gamma & = & \mathit{inl} \circ \llbracket e \rrbracket_\Gamma \\
21
+
\llbracket \mathsf{inr}\ e \rrbracket_\Gamma & = & \mathit{inr} \circ \llbracket e \rrbracket_\Gamma
22
+
\end{array}
23
+
}
24
+
##{
25
+
\begin{array}{l}\llbracket \mathsf{case}\ e_0\ \mathsf{of}\ \mathsf{inl}\ x \rightarrow e_1 ; \mathsf{inr}\ y \rightarrow e_2 \rrbracket_\Gamma(\vec{z}) \\
26
+
\quad =
27
+
[ \boldsymbol{\lambda}v. \llbracket e_1 \rrbracket_{\Gamma,x:\tau_1}(\vec{z},v), \boldsymbol{\lambda}v. \llbracket e_2 \rrbracket_{\Gamma,y:\tau_2}(\vec{z},v)] (\llbracket e_0 \rrbracket_\Gamma(\vec{z}))\end{array}
28
+
}
29
+
}
+10
trees/dt/dt-003T.tree
+10
trees/dt/dt-003T.tree
···
1
+
\title{PCF}
2
+
\author{liamoc}
3
+
\p{For most purposes in [semantics](dt-0001), describing semantics in terms of ([continuous](dt-001J) functions on) [cpos](dt-001D) is enough. To demonstrate, we will give semantics to PCF: a Turing-complete, higher order functional programming language. We will then extend PCF to include more features, namely pairs (product types) and sum types.}
4
+
\transclude{dt-003M}
5
+
\transclude{dt-003N}
6
+
\transclude{dt-003O}
7
+
\transclude{dt-003Q}
8
+
\transclude{dt-003P}
9
+
\transclude{dt-003R}
10
+
\transclude{dt-003S}
+8
trees/dt/dt-macros.tree
+8
trees/dt/dt-macros.tree
···
1
1
\def\cal[body]{#{\mathcal{\body}}}
2
2
\def\syn[body]{#{\mathsf{\body}}}
3
+
\def\inferrule[top][bottom]{\dfrac{\top}{\bottom}}
3
4
\def\proofblock[body]{\scope{
4
5
\put\transclude/toc{false}
5
6
\put\transclude/numbered{false}
6
7
\subtree{\taxon{Proof}
7
8
\body
9
+
}}}
10
+
\def\subblock[tile][body]{\scope{
11
+
\put\transclude/toc{false}
12
+
\put\transclude/numbered{false}
13
+
\subtree{
14
+
\title{\tile}
15
+
\body
8
16
}}}
9
17
\def\upshotblock[body]{\scope{
10
18
\put\transclude/toc{false}
+1
-1
trees/people/jcb.tree
+1
-1
trees/people/jcb.tree