michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Finished implementing Maps

Browse source
This commit is contained in:
Wen Kokke 2017-06-21 16:59:10 +02:00
parent 044f4d0263
commit 1c9b86fb26
No known key found for this signature in database
GPG key ID: EF467CD387487CB8
5 changed files with 246 additions and 785 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
Gemfile
View file

@ -1,28 +1,10 @@
source "https://rubygems.org"
ruby RUBY_VERSION
# Hello! This is where you manage which Jekyll version is used to run.
# When you want to use a different version, change it below, save the
# file and run `bundle install`. Run Jekyll with `bundle exec`, like so:
#
# bundle exec jekyll serve
#
# This will help ensure the proper Jekyll version is running.
# Happy Jekylling!
gem "jekyll", "3.4.2"
# This is the default theme for new Jekyll sites. You may change this to anything you like.
gem "minima", "~> 2.0"
gem "github-pages", group: :jekyll_plugins
# If you want to use GitHub Pages, remove the "gem "jekyll"" above and
# uncomment the line below. To upgrade, run `bundle update github-pages`.
# gem "github-pages", group: :jekyll_plugins
# If you have any plugins, put them here!
group :jekyll_plugins do
gem "jekyll-feed", "~> 0.6"
end
# Windows does not include zoneinfo files, so bundle the tzinfo-data gem
gem 'tzinfo-data', platforms: [:mingw, :mswin, :x64_mingw, :jruby]

175
Gemfile.lock
View file

@ -1,12 +1,79 @@
GEM
remote: https://rubygems.org/
specs:
addressable (2.5.0)
activesupport (4.2.8)
i18n (~> 0.7)
minitest (~> 5.1)
thread_safe (~> 0.3, >= 0.3.4)
tzinfo (~> 1.1)
addressable (2.5.1)
public_suffix (~> 2.0, >= 2.0.2)
coffee-script (2.4.1)
coffee-script-source
execjs
coffee-script-source (1.12.2)
colorator (1.1.0)
ethon (0.10.1)
ffi (>= 1.3.0)
execjs (2.7.0)
faraday (0.12.1)
multipart-post (>= 1.2, < 3)
ffi (1.9.18)
forwardable-extended (2.6.0)
jekyll (3.4.2)
gemoji (3.0.0)
github-pages (140)
activesupport (= 4.2.8)
github-pages-health-check (= 1.3.4)
jekyll (= 3.4.3)
jekyll-avatar (= 0.4.2)
jekyll-coffeescript (= 1.0.1)
jekyll-default-layout (= 0.1.4)
jekyll-feed (= 0.9.2)
jekyll-gist (= 1.4.0)
jekyll-github-metadata (= 2.3.1)
jekyll-mentions (= 1.2.0)
jekyll-optional-front-matter (= 0.1.2)
jekyll-paginate (= 1.1.0)
jekyll-readme-index (= 0.1.0)
jekyll-redirect-from (= 0.12.1)
jekyll-relative-links (= 0.4.0)
jekyll-sass-converter (= 1.5.0)
jekyll-seo-tag (= 2.2.3)
jekyll-sitemap (= 1.0.0)
jekyll-swiss (= 0.4.0)
jekyll-theme-architect (= 0.0.4)
jekyll-theme-cayman (= 0.0.4)
jekyll-theme-dinky (= 0.0.4)
jekyll-theme-hacker (= 0.0.4)
jekyll-theme-leap-day (= 0.0.4)
jekyll-theme-merlot (= 0.0.4)
jekyll-theme-midnight (= 0.0.4)
jekyll-theme-minimal (= 0.0.4)
jekyll-theme-modernist (= 0.0.4)
jekyll-theme-primer (= 0.2.1)
jekyll-theme-slate (= 0.0.4)
jekyll-theme-tactile (= 0.0.4)
jekyll-theme-time-machine (= 0.0.4)
jekyll-titles-from-headings (= 0.1.5)
jemoji (= 0.8.0)
kramdown (= 1.13.2)
liquid (= 3.0.6)
listen (= 3.0.6)
mercenary (~> 0.3)
minima (= 2.1.1)
rouge (= 1.11.1)
terminal-table (~> 1.4)
github-pages-health-check (1.3.4)
addressable (~> 2.3)
net-dns (~> 0.8)
octokit (~> 4.0)
public_suffix (~> 2.0)
typhoeus (~> 0.7)
html-pipeline (2.6.0)
activesupport (>= 2)
nokogiri (>= 1.4)
i18n (0.8.4)
jekyll (3.4.3)
addressable (~> 2.4)
colorator (~> 1.0)
jekyll-sass-converter (~> 1.0)
@ -17,41 +84,119 @@ GEM
pathutil (~> 0.9)
rouge (~> 1.7)
safe_yaml (~> 1.0)
jekyll-feed (0.9.1)
jekyll-avatar (0.4.2)
jekyll (~> 3.0)
jekyll-coffeescript (1.0.1)
coffee-script (~> 2.2)
jekyll-default-layout (0.1.4)
jekyll (~> 3.0)
jekyll-feed (0.9.2)
jekyll (~> 3.3)
jekyll-gist (1.4.0)
octokit (~> 4.2)
jekyll-github-metadata (2.3.1)
jekyll (~> 3.1)
octokit (~> 4.0, != 4.4.0)
jekyll-mentions (1.2.0)
activesupport (~> 4.0)
html-pipeline (~> 2.3)
jekyll (~> 3.0)
jekyll-optional-front-matter (0.1.2)
jekyll (~> 3.0)
jekyll-paginate (1.1.0)
jekyll-readme-index (0.1.0)
jekyll (~> 3.0)
jekyll-redirect-from (0.12.1)
jekyll (~> 3.3)
jekyll-relative-links (0.4.0)
jekyll (~> 3.3)
jekyll-sass-converter (1.5.0)
sass (~> 3.4)
jekyll-seo-tag (2.2.3)
jekyll (~> 3.3)
jekyll-sitemap (1.0.0)
jekyll (~> 3.3)
jekyll-swiss (0.4.0)
jekyll-theme-architect (0.0.4)
jekyll (~> 3.3)
jekyll-theme-cayman (0.0.4)
jekyll (~> 3.3)
jekyll-theme-dinky (0.0.4)
jekyll (~> 3.3)
jekyll-theme-hacker (0.0.4)
jekyll (~> 3.3)
jekyll-theme-leap-day (0.0.4)
jekyll (~> 3.3)
jekyll-theme-merlot (0.0.4)
jekyll (~> 3.3)
jekyll-theme-midnight (0.0.4)
jekyll (~> 3.3)
jekyll-theme-minimal (0.0.4)
jekyll (~> 3.3)
jekyll-theme-modernist (0.0.4)
jekyll (~> 3.3)
jekyll-theme-primer (0.2.1)
jekyll (~> 3.3)
jekyll-theme-slate (0.0.4)
jekyll (~> 3.3)
jekyll-theme-tactile (0.0.4)
jekyll (~> 3.3)
jekyll-theme-time-machine (0.0.4)
jekyll (~> 3.3)
jekyll-titles-from-headings (0.1.5)
jekyll (~> 3.3)
jekyll-watch (1.5.0)
listen (~> 3.0, < 3.1)
jemoji (0.8.0)
activesupport (~> 4.0)
gemoji (~> 3.0)
html-pipeline (~> 2.2)
jekyll (>= 3.0)
kramdown (1.13.2)
liquid (3.0.6)
listen (3.0.8)
rb-fsevent (~> 0.9, >= 0.9.4)
rb-inotify (~> 0.9, >= 0.9.7)
listen (3.0.6)
rb-fsevent (>= 0.9.3)
rb-inotify (>= 0.9.7)
mercenary (0.3.6)
minima (2.1.0)
mini_portile2 (2.2.0)
minima (2.1.1)
jekyll (~> 3.3)
minitest (5.10.2)
multipart-post (2.0.0)
net-dns (0.8.0)
nokogiri (1.8.0)
mini_portile2 (~> 2.2.0)
octokit (4.7.0)
sawyer (~> 0.8.0, >= 0.5.3)
pathutil (0.14.0)
forwardable-extended (~> 2.6)
public_suffix (2.0.5)
rb-fsevent (0.9.8)
rb-inotify (0.9.8)
ffi (>= 0.5.0)
rb-inotify (0.9.10)
ffi (>= 0.5.0, < 2)
rouge (1.11.1)
safe_yaml (1.0.4)
sass (3.4.23)
sass (3.4.24)
sawyer (0.8.1)
addressable (>= 2.3.5, < 2.6)
faraday (~> 0.8, < 1.0)
terminal-table (1.8.0)
unicode-display_width (~> 1.1, >= 1.1.1)
thread_safe (0.3.6)
typhoeus (0.8.0)
ethon (>= 0.8.0)
tzinfo (1.2.3)
thread_safe (~> 0.1)
unicode-display_width (1.3.0)
PLATFORMS
ruby
DEPENDENCIES
jekyll (= 3.4.2)
github-pages
jekyll-feed (~> 0.6)
minima (~> 2.0)
tzinfo-data
RUBY VERSION
ruby 2.4.0p0
BUNDLED WITH
1.14.6
1.15.0

30
out/Basics.md
View file

@ -4,7 +4,8 @@ layout : page
permalink : /Basics
---
<pre class="Agda">{% raw %}
<pre class="Agda">
<a name="113" class="Keyword"
>open</a
><a name="117"
@ -34,7 +35,8 @@ permalink : /Basics
><a name="179" class="Symbol"
>)</a
>
{% endraw %}</pre>
</pre>
The functional programming style brings programming closer to
simple, everyday mathematics: If a procedure or method has no side
@ -87,7 +89,8 @@ very simple example.
The following declaration tells Agda that we are defining
a new set of data values -- a *type*.
<pre class="Agda">{% raw %}
<pre class="Agda">
<a name="2469" class="Keyword"
>data</a
><a name="2473"
@ -198,7 +201,8 @@ a new set of data values -- a *type*.
><a name="2612" href="Basics.html#2474" class="Datatype"
>Day</a
>
{% endraw %}</pre>
</pre>
The type is called `day`, and its members are `monday`,
`tuesday`, etc. The second and following lines of the definition
@ -207,7 +211,8 @@ can be read "`monday` is a `day`, `tuesday` is a `day`, etc."
Having defined `day`, we can write functions that operate on
days.
<pre class="Agda">{% raw %}
<pre class="Agda">
<a name="2894" href="Basics.html#2894" class="Function"
>nextWeekday</a
><a name="2905"
@ -346,7 +351,8 @@ days.
><a name="3135" href="Basics.html#2492" class="InductiveConstructor"
>monday</a
>
{% endraw %}</pre>
</pre>
One thing to note is that the argument and return types of
this function are explicitly declared. Like most functional
@ -369,7 +375,8 @@ above example to Agda, and observe the result.
Second, we can record what we *expect* the result to be in the
form of an Agda type:
<pre class="Agda">{% raw %}
<pre class="Agda">
<a name="4097" href="Basics.html#4097" class="Function Operator"
>test_nextWeekday</a
><a name="4113"
@ -401,7 +408,8 @@ form of an Agda type:
><a name="4153" href="Basics.html#2510" class="InductiveConstructor"
>tuesday</a
>
{% endraw %}</pre>
</pre>
This declaration does two things: it makes an assertion (that the second
weekday after `saturday` is `tuesday`), and it gives the assertion a name
@ -410,7 +418,8 @@ that can be used to refer to it later.
Having made the assertion, we must also verify it. We do this by giving
a term of the above type:
<pre class="Agda">{% raw %}
<pre class="Agda">
<a name="4472" href="Basics.html#4097" class="Function Operator"
>test_nextWeekday</a
><a name="4488"
@ -422,7 +431,8 @@ a term of the above type:
><a name="4491" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
{% endraw %}</pre>
</pre>
There is no essential difference between the definition for
`test_nextWeekday` here and the definition for `nextWeekday` above,

84
src/Maps.lagda
View file

@ -11,7 +11,7 @@ a nice case study using ideas we've seen in previous chapters, including
building data structures out of higher-order functions (from [Basics]({{
"Basics" | relative_url }}) and [Poly]({{ "Poly" | relative_url }}) and the use
of reflection to streamline proofs (from [IndProp]({{ "IndProp" | relative_url
}})).
}})).
We'll define two flavors of maps: _total_ maps, which include a
"default" element to be returned when a key being looked up
@ -64,7 +64,7 @@ contrapositive : ∀ {ℓ₁ ℓ₂} {P : Set ℓ₁} {Q : Set ℓ₂} → (P
contrapositive p→q ¬q p = ¬q (p→q p)
\end{code}
Using the above, we can decide equality of two identifiers
Using the above, we can decide equality of two identifiers
by deciding equality on the underlying strings.
\begin{code}
@ -143,6 +143,12 @@ function that behaves like the desired map.
We define handy abbreviations for updating a map two, three, or four times.
<div class="note hidden">
Wen: you don't actually need to define these, you can simply declare `_,_↦_` to
be a left-associative infix operator with an `infixl` statement, and then you'll
be able to just evaluate `M , x ↦ y , z ↦ w` as `(M , x ↦ y) , z ↦ w`.
</div>
\begin{code}
_,_↦_,_↦_ : ∀ {A} → TotalMap A → Id → A → Id → A → TotalMap A
ρ , x₁ ↦ v₁ , x₂ ↦ v₂ = (ρ , x₁ ↦ v₁), x₂ ↦ v₂
@ -180,7 +186,7 @@ application!
To use maps in later chapters, we'll need several fundamental
facts about how they behave. Even if you don't work the following
exercises, make sure you understand the statements of
the lemmas!
the lemmas!
#### Exercise: 1 star, optional (apply-empty)
First, the empty map returns its default element for all keys:
@ -290,25 +296,65 @@ updates.
\begin{code}
update-permute′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A) (z : Id)
→ x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
update-permute′ {A} ρ x v y w z x≢y with x ≟ z | y ≟ z
... | yes x≡z | yes y≡z = ⊥-elim (x≢y (trans x≡z (sym y≡z)))
... | no x≢z | yes y≡z rewrite y≡z = {! sym (update-eq′ ρ z w)!}
... | yes x≡z | no y≢z rewrite x≡z = {! update-eq′ ρ z v!}
... | no x≢z | no y≢z = {! trans (update-neq ρ y w z y≢z) (sym (update-neq ρ x v z x≢z))!}
{-
Holes are typed as follows. What do the "| z ≟ z" mean, and how can I deal with them?
Why does "λ y₁" appear in the final hole?
?0 : w ≡ ((ρ , z ↦ w) z | z ≟ z)
?1 : ((ρ , z ↦ v) z | z ≟ z) ≡ v
?2 : (((λ y₁ → (ρ , x ↦ v) y₁ | x ≟ y₁) , y ↦ w) z | no y≢z) ≡
(((λ y₁ → (ρ , y ↦ w) y₁ | y ≟ y₁) , x ↦ v) z | no x≢z)
-}
update-permute′ {A} ρ x v y w z x≢y
with x ≟ z | y ≟ z
update-permute′ {A} ρ x v y w z x≢y
| yes x≡z | yes y≡z = ⊥-elim (x≢y (trans x≡z (sym y≡z)))
update-permute′ {A} ρ x v y w z x≢y
| no x≢z | yes y≡z rewrite y≡z
with z ≟ z
update-permute′ {A} ρ x v y w z x≢y
| no x≢z | yes y≡z | yes z≡z = refl
update-permute′ {A} ρ x v y w z x≢y
| no x≢z | yes y≡z | no z≢z = ⊥-elim (z≢z refl)
update-permute′ {A} ρ x v y w z x≢y
| yes x≡z | no y≢z rewrite x≡z
with z ≟ z
update-permute′ {A} ρ x v y w z x≢y
| yes x≡z | no y≢z | yes z≡z = refl
update-permute′ {A} ρ x v y w z x≢y
| yes x≡z | no y≢z | no z≢z = ⊥-elim (z≢z refl)
update-permute′ {A} ρ x v y w z x≢y
| no x≢z | no y≢z
with x ≟ z | y ≟ z
update-permute′ {A} ρ x v y w z x≢y
| no _ | no _ | no x≢z | no y≢z
= refl
update-permute′ {A} ρ x v y w z x≢y
| no x≢z | no y≢z | yes x≡z | _
= ⊥-elim (x≢z x≡z)
update-permute′ {A} ρ x v y w z x≢y
| no x≢z | no y≢z | _ | yes y≡z
= ⊥-elim (y≢z y≡z)
\end{code}
</div>
<div class="note hidden">
Phil:
Holes are typed as follows. What do the "| z ≟ z" mean, and how can I deal
with them? Why does "λ y₁" appear in the final hole?
?0 : w ≡ ((ρ , z ↦ w) z | z ≟ z)
?1 : ((ρ , z ↦ v) z | z ≟ z) ≡ v
?2 : (((λ y₁ → (ρ , x ↦ v) y₁ | x ≟ y₁) , y ↦ w) z | no y≢z) ≡
(((λ y₁ → (ρ , y ↦ w) y₁ | y ≟ y₁) , x ↦ v) z | no x≢z)
Wen:
The "| z ≟ z" term appears because there is a comparison on the two strings z
and z somewhere in the code. Because the decidable equality (and in fact all
functions on strings) are postulate, they do not reduce during type checking.
In order to stop this, you would have to insert a with clause at the location
where you want the term to reduce, i.e. "with z ≟ z", so that you can cover
both possible outputs, even if you already know that "z ≡ z", e.g. due to
reflexivity. You can cover the other case with a ⊥-elim fairly easily, but
it's not pretty. This is why I used naturals, because their equality test is
implemented in Agda and therefore can reduce. However, I'm not sure if
switching would in fact solve this problem, due to the fact that we're dealing
with variables, but I think so. See the completed code above for the
not-so-pretty way of actually implementing update-permute'.
</div>
## Partial maps
Finally, we define _partial maps_ on top of total maps. A partial

722
src/StlcOld.lagda
View file

@ -1,722 +0,0 @@
---
title : "StlcOld: The Simply Typed Lambda-Calculus (Old)"
layout : page
permalink : /StlcOld
---
<div class="foldable">
\begin{code}
open import Maps using (Id; id; _≟_; PartialMap; module PartialMap)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (ℕ; suc; zero; _+_)
open import Data.Product using (∃; ∄; _,_)
open import Function using (_∘_; _$_)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
\end{code}
</div>
The simply typed lambda-calculus (STLC) is a tiny core
calculus embodying the key concept of _functional abstraction_,
which shows up in pretty much every real-world programming
language in some form (functions, procedures, methods, etc.).
We will follow exactly the same pattern as in the previous chapter
when formalizing this calculus (syntax, small-step semantics,
typing rules) and its main properties (progress and preservation).
The new technical challenges arise from the mechanisms of
_variable binding_ and _substitution_. It which will take some
work to deal with these.
## Overview
The STLC is built on some collection of _base types_:
booleans, numbers, strings, etc. The exact choice of base types
doesn't matter much---the construction of the language and its
theoretical properties work out the same no matter what we
choose---so for the sake of brevity let's take just $$bool$$ for
the moment. At the end of the chapter we'll see how to add more
base types, and in later chapters we'll enrich the pure STLC with
other useful constructs like pairs, records, subtyping, and
mutable state.
Starting from boolean constants and conditionals, we add three
things:
- variables
- function abstractions
- application
This gives us the following collection of abstract syntax
constructors (written out first in informal BNF notation---we'll
formalize it below).
$$
\begin{array}{rll}
\text{Terms}\;s,t,u
::= & x & \text{variable} \\
\mid & \lambda x : A . t & \text{abstraction} \\
\mid & s\;t & \text{application} \\
\mid & true & \text{constant true} \\
\mid & false & \text{constant false} \\
\mid & \text{if }s\text{ then }t\text{ else }u & \text{conditional}
\end{array}
$$
In a lambda abstraction $$\lambda x : A . t$$, the variable $$x$$ is called the
_parameter_ to the function; the term $$t$$ is its _body_. The annotation $$:A$$
specifies the type of arguments that the function can be applied to.
Some examples:
- The identity function for booleans:
$$\lambda x:bool. x$$.
- The identity function for booleans, applied to the boolean $$true$$:
$$(\lambda x:bool. x)\;true$$.
- The boolean "not" function:
$$\lambda x:bool. \text{if }x\text{ then }false\text{ else }true$$.
- The constant function that takes every (boolean) argument to $$true$$:
$$\lambda x:bool. true$$.
- A two-argument function that takes two booleans and returns the
first one:
$$\lambda x:bool. \lambda y:bool. x$$.
As in Agda, a two-argument function is really a
one-argument function whose body is also a one-argument function.
- A two-argument function that takes two booleans and returns the
first one, applied to the booleans $$false$$ and $$true$$:
$$(\lambda x:bool. \lambda y:bool. x)\;false\;true$$.
As in Agda, application associates to the left---i.e., this
expression is parsed as
$$((\lambda x:bool. \lambda y:bool. x)\;false)\;true$$.
- A higher-order function that takes a _function_ $$f$$ (from booleans
to booleans) as an argument, applies $$f$$ to $$true$$, and applies
$$f$$ again to the result:
$$\lambda f:bool\rightarrow bool. f\;(f\;true)$$.
- The same higher-order function, applied to the constantly $$false$$
function:
$$(\lambda f:bool\rightarrow bool. f\;(f\;true))\;(\lambda x:bool. false)$$.
As the last several examples show, the STLC is a language of
_higher-order_ functions: we can write down functions that take
other functions as arguments and/or return other functions as
results.
The STLC doesn't provide any primitive syntax for defining _named_
functions---all functions are "anonymous." We'll see in chapter
`MoreStlc` that it is easy to add named functions to what we've
got---indeed, the fundamental naming and binding mechanisms are
exactly the same.
The _types_ of the STLC include $$bool$$, which classifies the
boolean constants $$true$$ and $$false$$ as well as more complex
computations that yield booleans, plus _arrow types_ that classify
functions.
$$
\text{Types}\;A,B ::= bool \mid A \rightarrow B
$$
For example:
- $$\lambda x:bool. false$$ has type $$bool\rightarrow bool$$;
- $$\lambda x:bool. x$$ has type $$bool\rightarrow bool$$;
- $$(\lambda x:bool. x)\;true$$ has type $$bool$$;
- $$\lambda x:bool. \lambda y:bool. x$$ has type
$$bool\rightarrow bool\rightarrow bool$$
(i.e., $$bool\rightarrow (bool\rightarrow bool)$$)
- $$(\lambda x:bool. \lambda y:bool. x)\;false$$ has type $$bool\rightarrow bool$$
- $$(\lambda x:bool. \lambda y:bool. x)\;false\;true$$ has type $$bool$$
## Syntax
We begin by formalizing the syntax of the STLC.
Unfortunately, $$\rightarrow$$ is already used for Agda's function type,
so we will STLC's function type as `_⇒_`.
### Types
\begin{code}
data Type : Set where
bool : Type
_⇒_ : Type → Type → Type
infixr 5 _⇒_
\end{code}
### Terms
\begin{code}
data Term : Set where
var : Id → Term
app : Term → Term → Term
abs : Id → Type → Term → Term
true : Term
false : Term
if_then_else_ : Term → Term → Term → Term
\end{code}
<div class="hidden">
\begin{code}
infixr 8 if_then_else_
\end{code}
</div>
Note that an abstraction $$\lambda x:A.t$$ (formally, `abs x A t`) is
always annotated with the type $$A$$ of its parameter, in contrast
to Agda (and other functional languages like ML, Haskell, etc.),
which use _type inference_ to fill in missing annotations. We're
not considering type inference here.
We introduce $$x, y, z$$ as names for variables. The pragmas ensure
that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
\begin{code}
x = id 0
y = id 1
z = id 2
{-# DISPLAY id zero = x #-}
{-# DISPLAY id (suc zero) = y #-}
{-# DISPLAY id (suc (suc zero)) = z #-}
\end{code}
Some examples...
$$\text{idB} = \lambda x:bool. x$$.
\begin{code}
idB = (abs x bool (var x))
\end{code}
$$\text{idBB} = \lambda x:bool\rightarrow bool. x$$.
\begin{code}
idBB = (abs x (bool ⇒ bool) (var x))
\end{code}
$$\text{idBBBB} = \lambda x:(bool\rightarrow bool)\rightarrow (bool\rightarrow bool). x$$.
\begin{code}
idBBBB = (abs x ((bool ⇒ bool) ⇒ (bool ⇒ bool)) (var x))
\end{code}
$$\text{k} = \lambda x:bool. \lambda y:bool. x$$.
\begin{code}
k = (abs x bool (abs y bool (var x)))
\end{code}
$$\text{notB} = \lambda x:bool. \text{if }x\text{ then }false\text{ else }true$$.
\begin{code}
notB = (abs x bool (if (var x) then false else true))
\end{code}
<div class="hidden">
\begin{code}
{-# DISPLAY abs 0 bool (var 0) = idB #-}
{-# DISPLAY abs 0 (bool ⇒ bool) (var 0) = idBB #-}
{-# DISPLAY abs 0 ((bool ⇒ bool) ⇒ (bool ⇒ bool)) (var 0) = idBBBB #-}
{-# DISPLAY abs 0 bool (abs y bool (var 0)) = k #-}
{-# DISPLAY abs 0 bool (if (var 0) then false else true) = notB #-}
\end{code}
</div>
## Operational Semantics
To define the small-step semantics of STLC terms, we begin,
as always, by defining the set of values. Next, we define the
critical notions of _free variables_ and _substitution_, which are
used in the reduction rule for application expressions. And
finally we give the small-step relation itself.
### Values
To define the values of the STLC, we have a few cases to consider.
First, for the boolean part of the language, the situation is
clear: $$true$$ and $$false$$ are the only values. An $$\text{if}$$
expression is never a value.
Second, an application is clearly not a value: It represents a
function being invoked on some argument, which clearly still has
work left to do.
Third, for abstractions, we have a choice:
- We can say that $$\lambda x:A. t$$ is a value only when $$t$$ is a
value---i.e., only if the function's body has been
reduced (as much as it can be without knowing what argument it
is going to be applied to).
- Or we can say that $$\lambda x:A. t$$ is always a value, no matter
whether $$t$$ is one or not---in other words, we can say that
reduction stops at abstractions.
Agda makes the first choice---for example,
\begin{code}
test_normalizeUnderLambda : (λ (x : ℕ) → 3 + 4) ≡ (λ (x : ℕ) → 7)
test_normalizeUnderLambda = refl
\end{code}
Most real-world functional programming languages make the second
choice---reduction of a function's body only begins when the
function is actually applied to an argument. We also make the
second choice here.
\begin{code}
data Value : Term → Set where
abs : ∀ {x A t}
→ Value (abs x A t)
true : Value true
false : Value false
\end{code}
Finally, we must consider what constitutes a _complete_ program.
Intuitively, a "complete program" must not refer to any undefined
variables. We'll see shortly how to define the _free_ variables
in a STLC term. A complete program is _closed_---that is, it
contains no free variables.
Having made the choice not to reduce under abstractions, we don't
need to worry about whether variables are values, since we'll
always be reducing programs "from the outside in," and that means
the small-step relation will always be working with closed terms.
### Substitution
Now we come to the heart of the STLC: the operation of
substituting one term for a variable in another term. This
operation is used below to define the operational semantics of
function application, where we will need to substitute the
argument term for the function parameter in the function's body.
For example, we reduce
$$(\lambda x:bool. \text{if }x\text{ then }true\text{ else }x)\;false$$
to
$$\text{if }false\text{ then }true\text{ else }false$$
by substituting $$false$$ for the parameter $$x$$ in the body of the
function.
In general, we need to be able to substitute some given term $$s$$
for occurrences of some variable $$x$$ in another term $$t$$. In
informal discussions, this is usually written $$[x:=s]t$$ and
pronounced "substitute $$x$$ with $$s$$ in $$t$$."
Here are some examples:
- $$[x:=true](\text{if }x\text{ then }x\text{ else }false)$$
yields $$\text{if }true\text{ then }true\text{ else }false$$
- $$[x:=true]x$$
yields $$true$$
- $$[x:=true](\text{if }x\text{ then }x\text{ else }y)$$
yields $$\text{if }true\text{ then }true\text{ else }y$$
- $$[x:=true]y$$
yields $$y$$
- $$[x:=true]false$$
yields $$false$$ (vacuous substitution)
- $$[x:=true](\lambda y:bool. \text{if }y\text{ then }x\text{ else }false)$$
yields $$\lambda y:bool. \text{if }y\text{ then }true\text{ else }false$$
- $$[x:=true](\lambda y:bool. x)$$
yields $$\lambda y:bool. true$$
- $$[x:=true](\lambda y:bool. y)$$
yields $$\lambda y:bool. y$$
- $$[x:=true](\lambda x:bool. x)$$
yields $$\lambda x:bool. x$$
The last example is very important: substituting $$x$$ with $$true$$ in
$$\lambda x:bool. x$$ does _not_ yield $$\lambda x:bool. true$$! The reason for
this is that the $$x$$ in the body of $$\lambda x:bool. x$$ is _bound_ by the
abstraction: it is a new, local name that just happens to be
spelled the same as some global name $$x$$.
Here is the definition, informally...
$$
\begin{aligned}
&[x:=s]x &&= s \\
&[x:=s]y &&= y \;\{\text{if }x\neq y\} \\
&[x:=s](\lambda x:A. t) &&= \lambda x:A. t \\
&[x:=s](\lambda y:A. t) &&= \lambda y:A. [x:=s]t \;\{\text{if }x\neq y\} \\
&[x:=s](t1\;t2) &&= ([x:=s]t1) ([x:=s]t2) \\
&[x:=s]true &&= true \\
&[x:=s]false &&= false \\
&[x:=s](\text{if }t1\text{ then }t2\text{ else }t3) &&=
\text{if }[x:=s]t1\text{ then }[x:=s]t2\text{ else }[x:=s]t3
\end{aligned}
$$
... and formally:
\begin{code}
[_:=_]_ : Id -> Term -> Term -> Term
[ x := v ] (var y) with x ≟ y
... | yes x=y = v
... | no x≠y = var y
[ x := v ] (app s t) = app ([ x := v ] s) ([ x := v ] t)
[ x := v ] (abs y A t) with x ≟ y
... | yes x=y = abs y A t
... | no x≠y = abs y A ([ x := v ] t)
[ x := v ] true = true
[ x := v ] false = false
[ x := v ] (if s then t else u) =
if [ x := v ] s then [ x := v ] t else [ x := v ] u
\end{code}
<div class="hidden">
\begin{code}
infix 9 [_:=_]_
\end{code}
</div>
_Technical note_: Substitution becomes trickier to define if we
consider the case where $$s$$, the term being substituted for a
variable in some other term, may itself contain free variables.
Since we are only interested here in defining the small-step relation
on closed terms (i.e., terms like $$\lambda x:bool. x$$ that include
binders for all of the variables they mention), we can avoid this
extra complexity here, but it must be dealt with when formalizing
richer languages.
#### Exercise: 3 stars (subst-correct)
The definition that we gave above defines substitution as a _function_.
Suppose, instead, we wanted to define substitution as an inductive _relation_.
We've begun the definition by providing the `data` header and
one of the constructors; your job is to fill in the rest of the constructors
and prove that the relation you've defined coincides with the function given
above.
\begin{code}
data [_:=_]_==>_ (x : Id) (s : Term) : Term -> Term -> Set where
var1 : [ x := s ] (var x) ==> s
{- FILL IN HERE -}
\end{code}
\begin{code}
postulate
subst-correct : ∀ s x t t'
→ [ x := s ] t ≡ t'
→ [ x := s ] t ==> t'
\end{code}
### Reduction
The small-step reduction relation for STLC now follows the
same pattern as the ones we have seen before. Intuitively, to
reduce a function application, we first reduce its left-hand
side (the function) until it becomes an abstraction; then we
reduce its right-hand side (the argument) until it is also a
value; and finally we substitute the argument for the bound
variable in the body of the abstraction. This last rule, written
informally as
$$
(\lambda x : A . t) v \Longrightarrow [x:=v]t
$$
is traditionally called "beta-reduction".
$$
\begin{array}{cl}
\frac{value(v)}{(\lambda x : A . t) v \Longrightarrow [x:=v]t}&(red)\\\\
\frac{s \Longrightarrow s'}{s\;t \Longrightarrow s'\;t}&(app1)\\\\
\frac{value(v)\quad t \Longrightarrow t'}{v\;t \Longrightarrow v\;t'}&(app2)
\end{array}
$$
... plus the usual rules for booleans:
$$
\begin{array}{cl}
\frac{}{(\text{if }true\text{ then }t_1\text{ else }t_2) \Longrightarrow t_1}&(iftrue)\\\\
\frac{}{(\text{if }false\text{ then }t_1\text{ else }t_2) \Longrightarrow t_2}&(iffalse)\\\\
\frac{s \Longrightarrow s'}{\text{if }s\text{ then }t_1\text{ else }t_2
\Longrightarrow \text{if }s\text{ then }t_1\text{ else }t_2}&(if)
\end{array}
$$
Formally:
\begin{code}
data _==>_ : Term → Term → Set where
red : ∀ {x A s t}
→ Value t
→ app (abs x A s) t ==> [ x := t ] s
app1 : ∀ {s s' t}
→ s ==> s'
→ app s t ==> app s' t
app2 : ∀ {s t t'}
→ Value s
→ t ==> t'
→ app s t ==> app s t'
if : ∀ {s s' t u}
→ s ==> s'
→ if s then t else u ==> if s' then t else u
iftrue : ∀ {s t}
→ if true then s else t ==> s
iffalse : ∀ {s t}
→ if false then s else t ==> t
\end{code}
<div class="hidden">
\begin{code}
infix 1 _==>_
\end{code}
</div>
\begin{code}
data Multi (R : Term → Term → Set) : Term → Term → Set where
refl : ∀ {x} -> Multi R x x
step : ∀ {x y z} -> R x y -> Multi R y z -> Multi R x z
\end{code}
\begin{code}
_==>*_ : Term → Term → Set
_==>*_ = Multi _==>_
\end{code}
<div class="hidden">
\begin{code}
{-# DISPLAY Multi _==>_ = _==>*_ #-}
\end{code}
</div>
### Examples
Example:
$$((\lambda x:bool\rightarrow bool. x) (\lambda x:bool. x)) \Longrightarrow^* (\lambda x:bool. x)$$.
\begin{code}
step-example1 : (app idBB idB) ==>* idB
step-example1 = step (red abs)
$ refl
\end{code}
Example:
$$(\lambda x:bool\rightarrow bool. x) \;((\lambda x:bool\rightarrow bool. x)\;(\lambda x:bool. x))) \Longrightarrow^* (\lambda x:bool. x)$$.
\begin{code}
step-example2 : (app idBB (app idBB idB)) ==>* idB
step-example2 = step (app2 abs (red abs))
$ step (red abs)
$ refl
\end{code}
Example:
$$((\lambda x:bool\rightarrow bool. x)\;(\lambda x:bool. \text{if }x\text{ then }false\text{ else }true))\;true\Longrightarrow^* false$$.
\begin{code}
step-example3 : (app (app idBB notB) true) ==>* false
step-example3 = step (app1 (red abs))
$ step (red true)
$ step iftrue
$ refl
\end{code}
Example:
$$((\lambda x:bool\rightarrow bool. x)\;((\lambda x:bool. \text{if }x\text{ then }false\text{ else }true)\;true))\Longrightarrow^* false$$.
\begin{code}
step-example4 : (app idBB (app notB true)) ==>* false
step-example4 = step (app2 abs (red true))
$ step (app2 abs iftrue)
$ step (red false)
$ refl
\end{code}
#### Exercise: 2 stars (step-example5)
\begin{code}
postulate
step-example5 : (app (app idBBBB idBB) idB) ==>* idB
\end{code}
## Typing
Next we consider the typing relation of the STLC.
### Contexts
_Question_: What is the type of the term "$$x\;y$$"?
_Answer_: It depends on the types of $$x$$ and $$y$$!
I.e., in order to assign a type to a term, we need to know
what assumptions we should make about the types of its free
variables.
This leads us to a three-place _typing judgment_, informally
written $$\Gamma\vdash t : A$$, where $$\Gamma$$ is a
"typing context"---a mapping from variables to their types.
Informally, we'll write $$\Gamma , x:A$$ for "extend the partial function
$$\Gamma$$ to also map $$x$$ to $$A$$." Formally, we use the function `_,_∶_`
(or "update") to add a binding to a context.
\begin{code}
Ctxt : Set
Ctxt = PartialMap Type
∅ : Ctxt
∅ = PartialMap.empty
_,_∶_ : Ctxt -> Id -> Type -> Ctxt
_,_∶_ = PartialMap.update
\end{code}
<div class="hidden">
\begin{code}
infixl 3 _,_∶_
\end{code}
</div>
### Typing Relation
$$
\begin{array}{cl}
\frac{\Gamma\;x = A}{\Gamma\vdash{x:A}}&(var)\\\\
\frac{\Gamma,x:A\vdash t:B}{\Gamma\vdash (\lambda x:A.t) : A\rightarrow B}&(abs)\\\\
\frac{\Gamma\vdash s:A\rightarrow B\quad\Gamma\vdash t:A}{\Gamma\vdash (s\;t) : B}&(app)\\\\
\frac{}{\Gamma\vdash true : bool}&(true)\\\\
\frac{}{\Gamma\vdash false : bool}&(true)\\\\
\frac{\Gamma\vdash s:bool \quad \Gamma\vdash t1:A \quad \Gamma\vdash t2:A}{\Gamma\vdash\text{if }s\text{ then }t1\text{ else }t2 : A}&(if)
\end{array}
$$
We can read the three-place relation $$\Gamma\vdash (t : A)$$ as:
"to the term $$t$$ we can assign the type $$A$$ using as types for
the free variables of $$t$$ the ones specified in the context
$$\Gamma$$."
\begin{code}
data _⊢_∶_ : Ctxt -> Term -> Type -> Set where
var : ∀ {Γ} x {A}
→ Γ x ≡ just A
→ Γ ⊢ var x ∶ A
abs : ∀ {Γ} {x} {A} {B} {s}
→ Γ , x ∶ A ⊢ s ∶ B
→ Γ ⊢ abs x A s ∶ A ⇒ B
app : ∀ {Γ} {A} {B} {s} {t}
→ Γ ⊢ s ∶ A ⇒ B
→ Γ ⊢ t ∶ A
→ Γ ⊢ app s t ∶ B
true : ∀ {Γ}
→ Γ ⊢ true ∶ bool
false : ∀ {Γ}
→ Γ ⊢ false ∶ bool
if_then_else_ : ∀ {Γ} {s} {t} {u} {A}
→ Γ ⊢ s ∶ bool
→ Γ ⊢ t ∶ A
→ Γ ⊢ u ∶ A
→ Γ ⊢ if s then t else u ∶ A
\end{code}
<div class="hidden">
\begin{code}
infix 1 _⊢_∶_
\end{code}
</div>
### Examples
\begin{code}
typing-example1 : ∅ ⊢ idB ∶ bool ⇒ bool
typing-example1 = abs (var x refl)
\end{code}
Another example:
$$\varnothing\vdash \lambda x:A. \lambda y:A\rightarrow A. y\;(y\;x) : A\rightarrow (A\rightarrow A)\rightarrow A$$.
\begin{code}
typing-example2 : ∅ ⊢
(abs x bool
(abs y (bool ⇒ bool)
(app (var y)
(app (var y) (var x)))))
∶ (bool ⇒ (bool ⇒ bool) ⇒ bool)
typing-example2 =
(abs
(abs
(app (var y refl)
(app (var y refl) (var x refl) ))))
\end{code}
#### Exercise: 2 stars (typing-example3)
Formally prove the following typing derivation holds:
$$\exists A, \varnothing\vdash \lambda x:bool\rightarrow B. \lambda y:bool\rightarrow bool. \lambda z:bool. y\;(x\;z) : A$$.
\begin{code}
postulate
typing-example3 : ∃ λ A → ∅ ⊢
(abs x (bool ⇒ bool)
(abs y (bool ⇒ bool)
(abs z bool
(app (var y) (app (var x) (var z)))))) ∶ A
\end{code}
We can also show that terms are _not_ typable. For example, let's
formally check that there is no typing derivation assigning a type
to the term $$\lambda x:bool. \lambda y:bool. x\;y$$---i.e.,
$$\nexists A, \varnothing\vdash \lambda x:bool. \lambda y:bool. x\;y : A$$.
\begin{code}
postulate
typing-nonexample1 : ∄ λ A → ∅ ⊢
(abs x bool
(abs y bool
(app (var x) (var y)))) ∶ A
\end{code}
#### Exercise: 3 stars, optional (typing-nonexample2)
Another nonexample:
$$\nexists A, \exists B, \varnothing\vdash \lambda x:A. x\;x : B$$.
\begin{code}
postulate
typing-nonexample2 : ∄ λ A → ∃ λ B → ∅ ⊢
(abs x B (app (var x) (var x))) ∶ A
\end{code}