backups
This commit is contained in:
wadler
parent
94523f62b5
commit
715cfb7fcc
2 changed files with 1494 additions and 0 deletions
896
src/extra/Lists-backup.lagda
Normal file
896
src/extra/Lists-backup.lagda
Normal file
|
|
@ -0,0 +1,896 @@
|
|||
---
|
||||
title : "Lists: Lists and higher-order functions"
|
||||
layout : page
|
||||
permalink : /Lists
|
||||
---
|
||||
|
||||
This chapter discusses the list data type. It gives further examples
|
||||
of many of the techniques we have developed so far, and provides
|
||||
examples of polymorphic types and higher-order functions.
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; sym; trans; cong)
|
||||
open Eq.≡-Reasoning
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
|
||||
open import Data.Nat.Properties using
|
||||
(+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
|
||||
open import Isomorphism using (_≃_)
|
||||
open import Function using (_∘_)
|
||||
open import Level using (Level)
|
||||
\end{code}
|
||||
|
||||
We assume [extensionality][extensionality].
|
||||
\begin{code}
|
||||
postulate
|
||||
extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
|
||||
\end{code}
|
||||
|
||||
[extensionality]: Equality#extensionality
|
||||
|
||||
|
||||
## Lists
|
||||
|
||||
Lists are defined in Agda as follows.
|
||||
\begin{code}
|
||||
data List (A : Set) : Set where
|
||||
[] : List A
|
||||
_∷_ : A → List A → List A
|
||||
|
||||
infixr 5 _∷_
|
||||
\end{code}
|
||||
Let's unpack this definition. If `A` is a set, then `List A` is a set.
|
||||
The next two lines tell us that `[]` (pronounced *nil*) is a list of
|
||||
type `A` (often called the *empty* list), and that `_∷_` (pronounced
|
||||
*cons*, short for *constructor*) takes a value of type `A` and a `List
|
||||
A` and returns a `List A`. Operator `_∷_` has precedence level 5 and
|
||||
associates to the right.
|
||||
|
||||
For example,
|
||||
\begin{code}
|
||||
_ : List ℕ
|
||||
_ = 0 ∷ 1 ∷ 2 ∷ []
|
||||
\end{code}
|
||||
denotes the list of the first three natural numbers. Since `_::_`
|
||||
associates to the right, the term parses as `0 ∷ (1 ∷ (2 ∷ []))`.
|
||||
Here `0` is the first element of the list, called the *head*,
|
||||
and `1 ∷ (2 ∷ [])` is a list of the remaining elements, called the
|
||||
*tail*. Lists are a rather strange beast: they have a head and a tail,
|
||||
nothing in between, and the tail is itself another list!
|
||||
|
||||
As we've seen, parameterised types can be translated to
|
||||
indexed types. The definition above is equivalent to the following.
|
||||
\begin{code}
|
||||
data List′ : Set → Set where
|
||||
[]′ : ∀ {A : Set} → List′ A
|
||||
_∷′_ : ∀ {A : Set} → A → List′ A → List′ A
|
||||
\end{code}
|
||||
Each constructor takes the parameter as an implicit argument.
|
||||
Thus, our example list could also be written
|
||||
\begin{code}
|
||||
_ : List ℕ
|
||||
_ = _∷_ {ℕ} 0 (_∷_ {ℕ} 1 (_∷_ {ℕ} 2 ([] {ℕ})))
|
||||
\end{code}
|
||||
where here we have made the implicit parameters explicit.
|
||||
|
||||
Including the lines
|
||||
|
||||
{-# BUILTIN LIST List #-}
|
||||
|
||||
tells Agda that the type `List` corresponds to the Haskell type
|
||||
list, and the constructors `[]` and `_∷_` correspond to nil and
|
||||
cons respectively, allowing a more efficient representation of lists.
|
||||
|
||||
|
||||
## List syntax
|
||||
|
||||
We can write lists more conveniently by introducing the following definitions.
|
||||
\begin{code}
|
||||
pattern [_] z = z ∷ []
|
||||
pattern [_,_] y z = y ∷ z ∷ []
|
||||
pattern [_,_,_] x y z = x ∷ y ∷ z ∷ []
|
||||
pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
|
||||
pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ []
|
||||
pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []
|
||||
\end{code}
|
||||
This is our first use of pattern declarations. For instance,
|
||||
the third line tells us that `[ x , y , z ]` is equivalent to
|
||||
`x ∷ y ∷ z ∷ []`, and permits the former to appear either in
|
||||
a pattern on the left-hand side of an equation, or a term
|
||||
on the right-hand side of an equation.
|
||||
|
||||
|
||||
## Append
|
||||
|
||||
Our first function on lists is written `_++_` and pronounced
|
||||
*append*.
|
||||
\begin{code}
|
||||
infixr 5 _++_
|
||||
|
||||
_++_ : ∀ {A : Set} → List A → List A → List A
|
||||
[] ++ ys = ys
|
||||
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
|
||||
\end{code}
|
||||
The type `A` is an implicit argument to append, making it
|
||||
a *polymorphic* function (one that can be used at many types).
|
||||
The empty list appended to another list yields the other list.
|
||||
A non-empty list appended to another list yields a list with
|
||||
head the same as the head of the first list and
|
||||
tail the same as the tail of the first list appended to the second list.
|
||||
|
||||
Here is an example, showing how to compute the result
|
||||
of appending two lists.
|
||||
\begin{code}
|
||||
_ : [ 0 , 1 , 2 ] ++ [ 3 , 4 ] ≡ [ 0 , 1 , 2 , 3 , 4 ]
|
||||
_ =
|
||||
begin
|
||||
0 ∷ 1 ∷ 2 ∷ [] ++ 3 ∷ 4 ∷ []
|
||||
≡⟨⟩
|
||||
0 ∷ (1 ∷ 2 ∷ [] ++ 3 ∷ 4 ∷ [])
|
||||
≡⟨⟩
|
||||
0 ∷ 1 ∷ (2 ∷ [] ++ 3 ∷ 4 ∷ [])
|
||||
≡⟨⟩
|
||||
0 ∷ 1 ∷ 2 ∷ ([] ++ 3 ∷ 4 ∷ [])
|
||||
≡⟨⟩
|
||||
0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ []
|
||||
∎
|
||||
\end{code}
|
||||
Appending two lists requires time linear in the
|
||||
number of elements in the first list.
|
||||
|
||||
|
||||
## Reasoning about append
|
||||
|
||||
We can reason about lists in much the same way that we reason
|
||||
about numbers. Here is the proof that append is associative.
|
||||
\begin{code}
|
||||
++-assoc : ∀ {A : Set} (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
|
||||
++-assoc [] ys zs =
|
||||
begin
|
||||
([] ++ ys) ++ zs
|
||||
≡⟨⟩
|
||||
ys ++ zs
|
||||
≡⟨⟩
|
||||
[] ++ (ys ++ zs)
|
||||
∎
|
||||
++-assoc (x ∷ xs) ys zs =
|
||||
begin
|
||||
(x ∷ xs ++ ys) ++ zs
|
||||
≡⟨⟩
|
||||
x ∷ ((xs ++ ys) ++ zs)
|
||||
≡⟨ cong (x ∷_) (++-assoc xs ys zs) ⟩
|
||||
x ∷ (xs ++ (ys ++ zs))
|
||||
≡⟨⟩
|
||||
x ∷ xs ++ (ys ++ zs)
|
||||
∎
|
||||
\end{code}
|
||||
The proof is by induction on the first argument. The base case instantiates
|
||||
to `[]`, and follows by straightforward computation.
|
||||
The inductive case instantiates to `x ∷ xs`,
|
||||
and follows by straightforward computation combined with the
|
||||
inductive hypothesis. As usual, the inductive hypothesis is indicated by a recursive
|
||||
invocation of the proof, in this case `++-assoc xs ys zs`.
|
||||
|
||||
Agda supports a variant of the *section* notation introduced by Richard Bird.
|
||||
If `_⊕_` is an arbitrary binary operator, we
|
||||
write `(x ⊕_)` for the function which applied to `y` returns `x ⊕ y`, and
|
||||
we write `(_⊕ y)` for the function which applied to `x` also returns `x ⊕ y`.
|
||||
Applying the congruence `cong (x ∷_)` promotes the inductive hypothesis
|
||||
|
||||
xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
|
||||
|
||||
to the equality
|
||||
|
||||
x ∷ (xs ++ (ys ++ zs)) ≡ x ∷ ((xs ++ ys) ++ zs)
|
||||
|
||||
which is needed in the proof.
|
||||
|
||||
It is also easy to show that `[]` is a left and right identity for `_++_`.
|
||||
That it is a left identity is immediate from the definition.
|
||||
\begin{code}
|
||||
++-identityˡ : ∀ {A : Set} (xs : List A) → [] ++ xs ≡ xs
|
||||
++-identityˡ xs =
|
||||
begin
|
||||
[] ++ xs
|
||||
≡⟨⟩
|
||||
xs
|
||||
∎
|
||||
\end{code}
|
||||
That it is a right identity follows by simple induction.
|
||||
\begin{code}
|
||||
++-identityʳ : ∀ {A : Set} (xs : List A) → xs ++ [] ≡ xs
|
||||
++-identityʳ [] =
|
||||
begin
|
||||
[] ++ []
|
||||
≡⟨⟩
|
||||
[]
|
||||
∎
|
||||
++-identityʳ (x ∷ xs) =
|
||||
begin
|
||||
(x ∷ xs) ++ []
|
||||
≡⟨⟩
|
||||
x ∷ (xs ++ [])
|
||||
≡⟨ cong (x ∷_) (++-identityʳ xs) ⟩
|
||||
x ∷ xs
|
||||
∎
|
||||
\end{code}
|
||||
As we will see later,
|
||||
these three properties establish that `_++_` and `[]` form
|
||||
a *monoid* over lists.
|
||||
|
||||
## Length
|
||||
|
||||
Our next function finds the length of a list.
|
||||
\begin{code}
|
||||
length : ∀ {A : Set} → List A → ℕ
|
||||
length [] = zero
|
||||
length (x ∷ xs) = suc (length xs)
|
||||
\end{code}
|
||||
Again, it takes an implicit parameter `A`.
|
||||
The length of the empty list is zero.
|
||||
The length of a non-empty list
|
||||
is one greater than the length of the tail of the list.
|
||||
|
||||
Here is an example showing how to compute the length of a list.
|
||||
\begin{code}
|
||||
_ : length [ 0 , 1 , 2 ] ≡ 3
|
||||
_ =
|
||||
begin
|
||||
length (0 ∷ 1 ∷ 2 ∷ [])
|
||||
≡⟨⟩
|
||||
suc (length (1 ∷ 2 ∷ []))
|
||||
≡⟨⟩
|
||||
suc (suc (length (2 ∷ [])))
|
||||
≡⟨⟩
|
||||
suc (suc (suc (length {ℕ} [])))
|
||||
≡⟨⟩
|
||||
suc (suc (suc zero))
|
||||
∎
|
||||
\end{code}
|
||||
Computing the length of a list requires time
|
||||
linear in the number of elements in the list.
|
||||
|
||||
In the second-to-last line, we cannot write simply `length []` but
|
||||
must instead write `length {ℕ} []`. Since `[]` has no elements, Agda
|
||||
has insufficient information to infer the implicit parameter.
|
||||
|
||||
|
||||
## Reasoning about length
|
||||
|
||||
The length of one list appended to another is the
|
||||
sum of the lengths of the lists.
|
||||
\begin{code}
|
||||
length-++ : ∀ {A : Set} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
|
||||
length-++ {A} [] ys =
|
||||
begin
|
||||
length ([] ++ ys)
|
||||
≡⟨⟩
|
||||
length ys
|
||||
≡⟨⟩
|
||||
length {A} [] + length ys
|
||||
∎
|
||||
length-++ (x ∷ xs) ys =
|
||||
begin
|
||||
length ((x ∷ xs) ++ ys)
|
||||
≡⟨⟩
|
||||
suc (length (xs ++ ys))
|
||||
≡⟨ cong suc (length-++ xs ys) ⟩
|
||||
suc (length xs + length ys)
|
||||
≡⟨⟩
|
||||
length (x ∷ xs) + length ys
|
||||
∎
|
||||
\end{code}
|
||||
The proof is by induction on the first arugment. The base case instantiates
|
||||
to `[]`, and follows by straightforward computation.
|
||||
As before, Agda cannot infer the implicit type parameter to `length`,
|
||||
and it must be given explicitly.
|
||||
The inductive case instantiates to `x ∷ xs`,
|
||||
and follows by straightforward computation combined with the
|
||||
inductive hypothesis. As usual, the inductive hypothesis is indicated by a recursive
|
||||
invocation of the proof, in this case `length-++ xs ys`, and it is promoted
|
||||
by the congruence `cong suc`.
|
||||
|
||||
|
||||
## Reverse
|
||||
|
||||
Using append, it is easy to formulate a function to reverse a list.
|
||||
\begin{code}
|
||||
reverse : ∀ {A : Set} → List A → List A
|
||||
reverse [] = []
|
||||
reverse (x ∷ xs) = reverse xs ++ [ x ]
|
||||
\end{code}
|
||||
The reverse of the empty list is the empty list.
|
||||
The reverse of a non-empty list
|
||||
is the reverse of its tail appended to a unit list
|
||||
containing its head.
|
||||
|
||||
Here is an example showing how to reverse a list.
|
||||
\begin{code}
|
||||
_ : reverse [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ]
|
||||
_ =
|
||||
begin
|
||||
reverse (0 ∷ 1 ∷ 2 ∷ [])
|
||||
≡⟨⟩
|
||||
reverse (1 ∷ 2 ∷ []) ++ [ 0 ]
|
||||
≡⟨⟩
|
||||
(reverse (2 ∷ []) ++ [ 1 ]) ++ [ 0 ]
|
||||
≡⟨⟩
|
||||
((reverse [] ++ [ 2 ]) ++ [ 1 ]) ++ [ 0 ]
|
||||
≡⟨⟩
|
||||
(([] ++ [ 2 ]) ++ [ 1 ]) ++ [ 0 ]
|
||||
≡⟨⟩
|
||||
(([] ++ 2 ∷ []) ++ 1 ∷ []) ++ 0 ∷ []
|
||||
≡⟨⟩
|
||||
(2 ∷ [] ++ 1 ∷ []) ++ 0 ∷ []
|
||||
≡⟨⟩
|
||||
2 ∷ ([] ++ 1 ∷ []) ++ 0 ∷ []
|
||||
≡⟨⟩
|
||||
(2 ∷ 1 ∷ []) ++ 0 ∷ []
|
||||
≡⟨⟩
|
||||
2 ∷ (1 ∷ [] ++ 0 ∷ [])
|
||||
≡⟨⟩
|
||||
2 ∷ 1 ∷ ([] ++ 0 ∷ [])
|
||||
≡⟨⟩
|
||||
2 ∷ 1 ∷ 0 ∷ []
|
||||
≡⟨⟩
|
||||
[ 2 , 1 , 0 ]
|
||||
∎
|
||||
\end{code}
|
||||
Reversing a list in this way takes time *quadratic* in the length of
|
||||
the list. This is because reverse ends up appending lists of lengths
|
||||
`1`, `2`, up to `n - 1`, where `n` is the length of the list being
|
||||
reversed, append takes time linear in the length of the first
|
||||
list, and the sum of the numbers up to `n - 1` is `n * (n - 1) / 2`.
|
||||
(We will validate that last fact in an exercise later in this chapter.)
|
||||
|
||||
### Exercise (`reverse-++-commute`)
|
||||
|
||||
Show that the reverse of one list appended to another is the
|
||||
reverse of the second appended to the reverse of the first.
|
||||
|
||||
reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
|
||||
|
||||
### Exercise (`reverse-involutive`)
|
||||
|
||||
A function is an *involution* if when applied twice it acts
|
||||
as the identity function. Show that reverse is an involution.
|
||||
|
||||
reverse (reverse xs) ≡ xs
|
||||
|
||||
## Faster reverse
|
||||
|
||||
The definition above, while easy to reason about, is less efficient than
|
||||
one might expect since it takes time quadratic in the length of the list.
|
||||
The idea is that we generalise reverse to take an additional argument.
|
||||
\begin{code}
|
||||
shunt : ∀ {A : Set} → List A → List A → List A
|
||||
shunt [] ys = ys
|
||||
shunt (x ∷ xs) ys = shunt xs (x ∷ ys)
|
||||
\end{code}
|
||||
The definition is by recursion on the first argument. The second argument
|
||||
actually becomes *larger*, but this is not a problem because the argument
|
||||
on which we recurse becomes *smaller*.
|
||||
|
||||
Shunt is related to reverse as follows.
|
||||
\begin{code}
|
||||
shunt-reverse : ∀ {A : Set} (xs ys : List A) → shunt xs ys ≡ reverse xs ++ ys
|
||||
shunt-reverse [] ys =
|
||||
begin
|
||||
shunt [] ys
|
||||
≡⟨⟩
|
||||
ys
|
||||
≡⟨⟩
|
||||
reverse [] ++ ys
|
||||
∎
|
||||
shunt-reverse (x ∷ xs) ys =
|
||||
begin
|
||||
shunt (x ∷ xs) ys
|
||||
≡⟨⟩
|
||||
shunt xs (x ∷ ys)
|
||||
≡⟨ shunt-reverse xs (x ∷ ys) ⟩
|
||||
reverse xs ++ (x ∷ ys)
|
||||
≡⟨⟩
|
||||
reverse xs ++ ([ x ] ++ ys)
|
||||
≡⟨ sym (++-assoc (reverse xs) [ x ] ys) ⟩
|
||||
(reverse xs ++ [ x ]) ++ ys
|
||||
≡⟨⟩
|
||||
reverse (x ∷ xs) ++ ys
|
||||
∎
|
||||
\end{code}
|
||||
The proof is by induction on the first argument.
|
||||
The base case instantiates to `[]`, and follows by straightforward computation.
|
||||
The inductive case instantiates to `x ∷ xs` and follows by the inductive
|
||||
hypothesis and associativity of append. When we invoke the inductive hypothesis,
|
||||
the second argument actually becomes *larger*, but this is not a problem because
|
||||
the argument on which we induct becomes *smaller*.
|
||||
|
||||
Generalising on an auxiliary argument, which becomes larger as the argument on
|
||||
which we recurse or induct becomes smaller, is a common trick. It belongs in
|
||||
you sling of arrows, ready to slay the right problem.
|
||||
|
||||
Having defined shunt be generalisation, it is now easy to respecialise to
|
||||
give a more efficient definition of reverse.
|
||||
\begin{code}
|
||||
reverse′ : ∀ {A : Set} → List A → List A
|
||||
reverse′ xs = shunt xs []
|
||||
\end{code}
|
||||
|
||||
Given our previous lemma, it is straightforward to show
|
||||
the two definitions equivalent.
|
||||
\begin{code}
|
||||
reverses : ∀ {A : Set} (xs : List A) → reverse′ xs ≡ reverse xs
|
||||
reverses xs =
|
||||
begin
|
||||
reverse′ xs
|
||||
≡⟨⟩
|
||||
shunt xs []
|
||||
≡⟨ shunt-reverse xs [] ⟩
|
||||
reverse xs ++ []
|
||||
≡⟨ ++-identityʳ (reverse xs) ⟩
|
||||
reverse xs
|
||||
∎
|
||||
\end{code}
|
||||
|
||||
Here is an example showing fast reverse of the list `[ 0 , 1 , 2 ]`.
|
||||
\begin{code}
|
||||
_ : reverse′ [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ]
|
||||
_ =
|
||||
begin
|
||||
reverse′ (0 ∷ 1 ∷ 2 ∷ [])
|
||||
≡⟨⟩
|
||||
shunt (0 ∷ 1 ∷ 2 ∷ []) []
|
||||
≡⟨⟩
|
||||
shunt (1 ∷ 2 ∷ []) (0 ∷ [])
|
||||
≡⟨⟩
|
||||
shunt (2 ∷ []) (1 ∷ 0 ∷ [])
|
||||
≡⟨⟩
|
||||
shunt [] (2 ∷ 1 ∷ 0 ∷ [])
|
||||
≡⟨⟩
|
||||
2 ∷ 1 ∷ 0 ∷ []
|
||||
∎
|
||||
\end{code}
|
||||
Now the time to reverse a list is linear in the length of the list.
|
||||
|
||||
## Map {#Map}
|
||||
|
||||
Map applies a function to every element of a list to generate a corresponding list.
|
||||
Map is an example of a *higher-order function*, one which takes a function as an
|
||||
argument and returns a function as a result.
|
||||
\begin{code}
|
||||
map : ∀ {A B : Set} → (A → B) → List A → List B
|
||||
map f [] = []
|
||||
map f (x ∷ xs) = f x ∷ map f xs
|
||||
\end{code}
|
||||
Map of the empty list is the empty list.
|
||||
Map of a non-empty list yields a list
|
||||
with head the same as the function applied to the head of the given list,
|
||||
and tail the same as map of the function applied to the tail of the given list.
|
||||
|
||||
Here is an example showing how to use map to increment every element of a list.
|
||||
\begin{code}
|
||||
_ : map suc [ 0 , 1 , 2 ] ≡ [ 1 , 2 , 3 ]
|
||||
_ =
|
||||
begin
|
||||
map suc (0 ∷ 1 ∷ 2 ∷ [])
|
||||
≡⟨⟩
|
||||
suc 0 ∷ map suc (1 ∷ 2 ∷ [])
|
||||
≡⟨⟩
|
||||
suc 0 ∷ suc 1 ∷ map suc (2 ∷ [])
|
||||
≡⟨⟩
|
||||
suc 0 ∷ suc 1 ∷ suc 2 ∷ map suc []
|
||||
≡⟨⟩
|
||||
suc 0 ∷ suc 1 ∷ suc 2 ∷ []
|
||||
∎
|
||||
\end{code}
|
||||
Map requires time linear in the length of the list.
|
||||
|
||||
It is often convenient to exploit currying by applying
|
||||
map to a function to yield a new function, and at a later
|
||||
point applying the resulting function.
|
||||
\begin{code}
|
||||
sucs : List ℕ → List ℕ
|
||||
sucs = map suc
|
||||
|
||||
_ : sucs [ 0 , 1 , 2 ] ≡ [ 1 , 2 , 3 ]
|
||||
_ =
|
||||
begin
|
||||
sucs [ 0 , 1 , 2 ]
|
||||
≡⟨⟩
|
||||
map suc [ 0 , 1 , 2 ]
|
||||
≡⟨⟩
|
||||
[ 1 , 2 , 3 ]
|
||||
∎
|
||||
\end{code}
|
||||
|
||||
Any type that is parameterised on another type, such as lists, has a
|
||||
corresponding map, which accepts a function and returns a function
|
||||
from the type parameterised on the domain of the function to the type
|
||||
parameterised on the range of the function. Further, a type that is
|
||||
parameterised on *n* types will have a map that is parameterised on
|
||||
*n* functions.
|
||||
|
||||
|
||||
### Exercise (`map-compose`)
|
||||
|
||||
Prove that the map of a composition is equal to the composition of two maps.
|
||||
|
||||
map (f ∘ g) ≡ map f ∘ map g
|
||||
|
||||
The last step of the proof requires extensionality.
|
||||
|
||||
*Exercise* `map-++-commute`
|
||||
|
||||
Prove the following relationship between map and append.
|
||||
|
||||
map f (xs ++ ys) ≡ map f xs ++ map f ys
|
||||
|
||||
|
||||
## Fold {#Fold}
|
||||
|
||||
Fold takes an operator and a value, and uses the operator to combine
|
||||
each of the elements of the list, taking the given value as the result
|
||||
for the empty list.
|
||||
\begin{code}
|
||||
foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B
|
||||
foldr _⊗_ e [] = e
|
||||
foldr _⊗_ e (x ∷ xs) = x ⊗ foldr _⊗_ e xs
|
||||
\end{code}
|
||||
Fold of the empty list is the given value.
|
||||
Fold of a non-empty list uses the operator to combine
|
||||
the head of the list and the fold of the tail of the list.
|
||||
|
||||
Here is an example showing how to use fold to find the sum of a list.
|
||||
\begin{code}
|
||||
_ : foldr _+_ 0 [ 1 , 2 , 3 , 4 ] ≡ 10
|
||||
_ =
|
||||
begin
|
||||
foldr _+_ 0 (1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
|
||||
≡⟨⟩
|
||||
1 + foldr _+_ 0 (2 ∷ 3 ∷ 4 ∷ [])
|
||||
≡⟨⟩
|
||||
1 + (2 + foldr _+_ 0 (3 ∷ 4 ∷ []))
|
||||
≡⟨⟩
|
||||
1 + (2 + (3 + foldr _+_ 0 (4 ∷ [])))
|
||||
≡⟨⟩
|
||||
1 + (2 + (3 + (4 + foldr _+_ 0 [])))
|
||||
≡⟨⟩
|
||||
1 + (2 + (3 + (4 + 0)))
|
||||
∎
|
||||
\end{code}
|
||||
Fold requires time linear in the length of the list.
|
||||
|
||||
It is often convenient to exploit currying by applying
|
||||
fold to an operator and a value to yield a new function,
|
||||
and at a later point applying the resulting function.
|
||||
\begin{code}
|
||||
sum : List ℕ → ℕ
|
||||
sum = foldr _+_ 0
|
||||
|
||||
_ : sum [ 1 , 2 , 3 , 4 ] ≡ 10
|
||||
_ =
|
||||
begin
|
||||
sum [ 1 , 2 , 3 , 4 ]
|
||||
≡⟨⟩
|
||||
foldr _+_ 0 [ 1 , 2 , 3 , 4 ]
|
||||
≡⟨⟩
|
||||
10
|
||||
∎
|
||||
\end{code}
|
||||
|
||||
Just as the list type has two constructors, `[]` and `_∷_`,
|
||||
so the fold function takes two arguments, `e` and `_⊕_`
|
||||
(in addition to the list argument).
|
||||
In general, a data type with *n* constructors will have
|
||||
a corresponding fold function that takes *n* arguments.
|
||||
|
||||
## Exercise (`product`)
|
||||
|
||||
Use fold to define a function to find the product of a list of numbers.
|
||||
|
||||
product [ 1 , 2 , 3 , 4 ] ≡ 24
|
||||
|
||||
### Exercise (`foldr-++`)
|
||||
|
||||
Show that fold and append are related as follows.
|
||||
\begin{code}
|
||||
postulate
|
||||
foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
|
||||
foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
|
||||
\end{code}
|
||||
|
||||
|
||||
### Exercise (`map-is-foldr`)
|
||||
|
||||
Show that map can be defined using fold.
|
||||
\begin{code}
|
||||
postulate
|
||||
map-is-foldr : ∀ {A B : Set} {f : A → B} →
|
||||
map f ≡ foldr (λ x xs → f x ∷ xs) []
|
||||
\end{code}
|
||||
This requires extensionality.
|
||||
|
||||
### Exercise (`sum-downFrom`)
|
||||
|
||||
Define a function that counts down as follows.
|
||||
\begin{code}
|
||||
downFrom : ℕ → List ℕ
|
||||
downFrom zero = []
|
||||
downFrom (suc n) = n ∷ downFrom n
|
||||
\end{code}
|
||||
For example,
|
||||
\begin{code}
|
||||
_ : downFrom 3 ≡ [ 2 , 1 , 0 ]
|
||||
_ = refl
|
||||
\end{code}
|
||||
Prove that the sum of the numbers `(n - 1) + ⋯ + 0` is
|
||||
equal to `n * (n - 1) / 2`.
|
||||
\begin{code}
|
||||
postulate
|
||||
sum-downFrom : ∀ (n : ℕ) → sum (downFrom n) * 2 ≡ n * (n ∸ 1)
|
||||
\end{code}
|
||||
|
||||
|
||||
<!-- `mapIsFold` in Data.List.Properties -->
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
## Monoids
|
||||
|
||||
Typically when we use a fold the operator is associative and the
|
||||
value is a left and right identity for the value, meaning that the
|
||||
operator and the value form a *monoid*.
|
||||
|
||||
We can define a monoid as a suitable record type.
|
||||
\begin{code}
|
||||
record IsMonoid {A : Set} (_⊗_ : A → A → A) (e : A) : Set where
|
||||
field
|
||||
assoc : ∀ (x y z : A) → (x ⊗ y) ⊗ z ≡ x ⊗ (y ⊗ z)
|
||||
identityˡ : ∀ (x : A) → e ⊗ x ≡ x
|
||||
identityʳ : ∀ (x : A) → x ⊗ e ≡ x
|
||||
|
||||
open IsMonoid
|
||||
\end{code}
|
||||
|
||||
As examples, sum and zero, multiplication and one, and append and the empty
|
||||
list, are all examples of monoids.
|
||||
\begin{code}
|
||||
+-monoid : IsMonoid _+_ 0
|
||||
+-monoid =
|
||||
record
|
||||
{ assoc = +-assoc
|
||||
; identityˡ = +-identityˡ
|
||||
; identityʳ = +-identityʳ
|
||||
}
|
||||
|
||||
*-monoid : IsMonoid _*_ 1
|
||||
*-monoid =
|
||||
record
|
||||
{ assoc = *-assoc
|
||||
; identityˡ = *-identityˡ
|
||||
; identityʳ = *-identityʳ
|
||||
}
|
||||
|
||||
++-monoid : ∀ {A : Set} → IsMonoid {List A} _++_ []
|
||||
++-monoid =
|
||||
record
|
||||
{ assoc = ++-assoc
|
||||
; identityˡ = ++-identityˡ
|
||||
; identityʳ = ++-identityʳ
|
||||
}
|
||||
\end{code}
|
||||
|
||||
If `_⊕_` and `e` form a monoid, then we can re-express fold on the
|
||||
same operator and an arbitrary value.
|
||||
\begin{code}
|
||||
foldr-monoid : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
|
||||
∀ (xs : List A) (y : A) → foldr _⊗_ y xs ≡ foldr _⊗_ e xs ⊗ y
|
||||
foldr-monoid _⊗_ e ⊗-monoid [] y =
|
||||
begin
|
||||
foldr _⊗_ y []
|
||||
≡⟨⟩
|
||||
y
|
||||
≡⟨ sym (identityˡ ⊗-monoid y) ⟩
|
||||
(e ⊗ y)
|
||||
≡⟨⟩
|
||||
foldr _⊗_ e [] ⊗ y
|
||||
∎
|
||||
foldr-monoid _⊗_ e ⊗-monoid (x ∷ xs) y =
|
||||
begin
|
||||
foldr _⊗_ y (x ∷ xs)
|
||||
≡⟨⟩
|
||||
x ⊗ (foldr _⊗_ y xs)
|
||||
≡⟨ cong (x ⊗_) (foldr-monoid _⊗_ e ⊗-monoid xs y) ⟩
|
||||
x ⊗ (foldr _⊗_ e xs ⊗ y)
|
||||
≡⟨ sym (assoc ⊗-monoid x (foldr _⊗_ e xs) y) ⟩
|
||||
(x ⊗ foldr _⊗_ e xs) ⊗ y
|
||||
≡⟨⟩
|
||||
foldr _⊗_ e (x ∷ xs) ⊗ y
|
||||
∎
|
||||
\end{code}
|
||||
|
||||
As a consequence, using a previous exercise, we have the following.
|
||||
\begin{code}
|
||||
foldr-monoid-++ : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
|
||||
∀ (xs ys : List A) → foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ e xs ⊗ foldr _⊗_ e ys
|
||||
foldr-monoid-++ _⊗_ e monoid-⊗ xs ys =
|
||||
begin
|
||||
foldr _⊗_ e (xs ++ ys)
|
||||
≡⟨ foldr-++ _⊗_ e xs ys ⟩
|
||||
foldr _⊗_ (foldr _⊗_ e ys) xs
|
||||
≡⟨ foldr-monoid _⊗_ e monoid-⊗ xs (foldr _⊗_ e ys) ⟩
|
||||
foldr _⊗_ e xs ⊗ foldr _⊗_ e ys
|
||||
∎
|
||||
\end{code}
|
||||
|
||||
## All {#All}
|
||||
|
||||
We can also define predicates over lists. Two of the most important
|
||||
are `All` and `Any`.
|
||||
|
||||
Predicate `All P` holds if predicate `P` is satisfied by every element of a list.
|
||||
\begin{code}
|
||||
data All {A : Set} (P : A → Set) : List A → Set where
|
||||
[] : All P []
|
||||
_∷_ : {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs)
|
||||
\end{code}
|
||||
The type has two constructors, reusing the names of the same constructors for lists.
|
||||
The first asserts that `P` holds for ever element of the empty list.
|
||||
The second asserts that if `P` holds of the head of a list and for every
|
||||
element of the tail of a list, then `P` holds for every element of the list.
|
||||
Agda uses types to disambiguate whether the constructor is building
|
||||
a list or evidence that `All P` holds.
|
||||
|
||||
For example, `All (_≤ 2)` holds of a list where every element is less
|
||||
than or equal to two. Recall that `z≤n` proves `zero ≤ n` for any
|
||||
`n`, and that if `m≤n` proves `m ≤ n` then `s≤s m≤n` proves `suc m ≤
|
||||
suc n`, for any `m` and `n`.
|
||||
\begin{code}
|
||||
_ : All (_≤ 2) [ 0 , 1 , 2 ]
|
||||
_ = z≤n ∷ (s≤s z≤n) ∷ (s≤s (s≤s z≤n)) ∷ []
|
||||
\end{code}
|
||||
Here `_∷_` and `[]` are the constructors of `All P` rather than of `List A`.
|
||||
The three items are proofs of `0 ≤ 2`, `1 ≤ 2`, and `2 ≤ 2`, respectively.
|
||||
|
||||
## Any
|
||||
|
||||
Predicate `Any P` holds if predicate `P` is satisfied by some element of a list.
|
||||
\begin{code}
|
||||
data Any {A : Set} (P : A → Set) : List A → Set where
|
||||
here : {x : A} {xs : List A} → P x → Any P (x ∷ xs)
|
||||
there : {x : A} {xs : List A} → Any P xs → Any P (x ∷ xs)
|
||||
\end{code}
|
||||
The first constructor provides evidence that the head of the list
|
||||
satisfies `P`, while the second provides evidence that some element of
|
||||
the tail of the list satisfies `P`. For example, we can define list
|
||||
membership as follows.
|
||||
\begin{code}
|
||||
infix 4 _∈_
|
||||
|
||||
_∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set
|
||||
x ∈ xs = Any (x ≡_) xs
|
||||
|
||||
_∉_ : ∀ {A : Set} (x : A) (xs : List A) → Set
|
||||
x ∉ xs = ¬ (x ∈ xs)
|
||||
\end{code}
|
||||
For example, zero is an element of the list `[ 0 , 1 , 0 , 2 ]`. Indeed, we can demonstrate
|
||||
this fact in two different ways, corresponding to the two different
|
||||
occurrences of zero in the list, as the first element and as the third element.
|
||||
\begin{code}
|
||||
_ : 0 ∈ [ 0 , 1 , 0 , 2 ]
|
||||
_ = here refl
|
||||
|
||||
_ : 0 ∈ [ 0 , 1 , 0 , 2 ]
|
||||
_ = there (there (here refl))
|
||||
\end{code}
|
||||
Further, we can demonstrate that three is not in the list, because
|
||||
any possible proof that it is in the list leads to contradiction.
|
||||
\begin{code}
|
||||
not-in : 3 ∉ [ 0 , 1 , 0 , 2 ]
|
||||
not-in (here ())
|
||||
not-in (there (here ()))
|
||||
not-in (there (there (here ())))
|
||||
not-in (there (there (there (here ()))))
|
||||
not-in (there (there (there (there ()))))
|
||||
\end{code}
|
||||
The five occurrences of `()` attest to the fact that there is no
|
||||
possible evidence for `3 ≡ 0`, `3 ≡ 1`, `3 ≡ 0`, `3 ≡ 2`, and
|
||||
`3 ∈ []`, respectively.
|
||||
|
||||
## All and append
|
||||
|
||||
A predicate holds for every element of one list appended to another if and
|
||||
only if it holds for every element of each list. Indeed, an even stronger
|
||||
result is true, as we can show that the two types are isomorphic.
|
||||
\begin{code}
|
||||
All-++ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
|
||||
All P (xs ++ ys) ≃ (All P xs × All P ys)
|
||||
All-++ xs ys =
|
||||
record
|
||||
{ to = to xs ys
|
||||
; from = from xs ys
|
||||
; from∘to = from∘to xs ys
|
||||
; to∘from = to∘from xs ys
|
||||
}
|
||||
|
||||
where
|
||||
|
||||
to : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
|
||||
All P (xs ++ ys) → (All P xs × All P ys)
|
||||
to [] ys ∀Pys = ⟨ [] , ∀Pys ⟩
|
||||
to (x ∷ xs) ys (Px ∷ ∀Pxs++ys) with to xs ys ∀Pxs++ys
|
||||
... | ⟨ ∀Pxs , ∀Pys ⟩ = ⟨ Px ∷ ∀Pxs , ∀Pys ⟩
|
||||
|
||||
from : ∀ { A : Set} {P : A → Set} (xs ys : List A) →
|
||||
All P xs × All P ys → All P (xs ++ ys)
|
||||
from [] ys ⟨ [] , ∀Pys ⟩ = ∀Pys
|
||||
from (x ∷ xs) ys ⟨ Px ∷ ∀Pxs , ∀Pys ⟩ = Px ∷ from xs ys ⟨ ∀Pxs , ∀Pys ⟩
|
||||
|
||||
from∘to : ∀ { A : Set} {P : A → Set} (xs ys : List A) →
|
||||
∀ (u : All P (xs ++ ys)) → from xs ys (to xs ys u) ≡ u
|
||||
from∘to [] ys ∀Pys = refl
|
||||
from∘to (x ∷ xs) ys (Px ∷ ∀Pxs++ys) = cong (Px ∷_) (from∘to xs ys ∀Pxs++ys)
|
||||
|
||||
to∘from : ∀ { A : Set} {P : A → Set} (xs ys : List A) →
|
||||
∀ (v : All P xs × All P ys) → to xs ys (from xs ys v) ≡ v
|
||||
to∘from [] ys ⟨ [] , ∀Pys ⟩ = refl
|
||||
to∘from (x ∷ xs) ys ⟨ Px ∷ ∀Pxs , ∀Pys ⟩ rewrite to∘from xs ys ⟨ ∀Pxs , ∀Pys ⟩ = refl
|
||||
\end{code}
|
||||
|
||||
### Exercise (`Any-++`)
|
||||
|
||||
Prove a result similar to `All-++`, but with `Any` in place of `All`, and a suitable
|
||||
replacement for `_×_`. As a consequence, demonstrate an isomorphism relating
|
||||
`_∈_` and `_++_`.
|
||||
|
||||
### Exercise (`¬Any≃All¬`)
|
||||
|
||||
First generalise composition to arbitrary levels, using
|
||||
[universe polymorphism][unipoly].
|
||||
\begin{code}
|
||||
_∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃} → (B → C) → (A → B) → A → C
|
||||
(g ∘′ f) x = g (f x)
|
||||
\end{code}
|
||||
|
||||
[unipoly]: Equality/index.html#unipoly
|
||||
|
||||
Show that `Any` and `All` satisfy a version of De Morgan's Law.
|
||||
\begin{code}
|
||||
postulate
|
||||
¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A) → (¬_ ∘′ Any P) xs ≃ All (¬_ ∘′ P) xs
|
||||
\end{code}
|
||||
|
||||
Do we also have the following?
|
||||
|
||||
(¬_ ∘′ All P) xs ≃ Any (¬_ ∘′ P) xs
|
||||
|
||||
If so, prove; if not, explain why.
|
||||
|
||||
## Standard Library
|
||||
|
||||
Definitions similar to those in this chapter can be found in the standard library.
|
||||
\begin{code}
|
||||
import Data.List using (List; _++_; length; reverse; map; foldr; downFrom)
|
||||
import Data.List.All using (All; []; _∷_)
|
||||
import Data.List.Any using (Any; here; there)
|
||||
import Data.List.Any.Membership.Propositional using (_∈_)
|
||||
import Algebra.Structures using (IsMonoid)
|
||||
\end{code}
|
||||
The standard library version of `IsMonoid` differs from the
|
||||
one given here, in that it is also parameterised on an equivalence relation.
|
||||
|
||||
|
||||
## Unicode
|
||||
|
||||
This chapter uses the following unicode.
|
||||
|
||||
∷ U+2237 PROPORTION (\::)
|
||||
⊗ U+2297 CIRCLED TIMES (\otimes)
|
||||
∈ U+2208 ELEMENT OF (\in)
|
||||
∉ U+2209 NOT AN ELEMENT OF (\inn)
|
||||
598
src/extra/Typed-backup.lagda
Normal file
598
src/extra/Typed-backup.lagda
Normal file
|
|
@ -0,0 +1,598 @@
|
|||
---
|
||||
title : "Typed: Typed Lambda term representation"
|
||||
layout : page
|
||||
permalink : /Typed
|
||||
---
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
module Typed where
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.List using (List; []; _∷_; [_]; _++_; map; foldr; filter)
|
||||
open import Data.List.Any using (Any; here; there)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤_; _⊔_; _≟_)
|
||||
open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; 1+n≰n)
|
||||
open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
open import Data.Unit using (⊤; tt)
|
||||
open import Function using (_∘_)
|
||||
open import Function.Equality using (≡-setoid)
|
||||
open import Function.Equivalence using (_⇔_; equivalence)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Relation.Nullary.Negation using (contraposition; ¬?)
|
||||
open import Relation.Nullary.Product using (_×-dec_)
|
||||
\end{code}
|
||||
|
||||
|
||||
## Syntax
|
||||
|
||||
\begin{code}
|
||||
infixr 6 _⇒_
|
||||
infixl 5 _,_⦂_
|
||||
infix 4 _∋_⦂_
|
||||
infix 4 _⊢_⦂_
|
||||
infix 5 ƛ_⦂_⇒_
|
||||
infix 5 ƛ_
|
||||
infixl 6 _·_
|
||||
|
||||
Id : Set
|
||||
Id = ℕ
|
||||
|
||||
data Type : Set where
|
||||
o : Type
|
||||
_⇒_ : Type → Type → Type
|
||||
|
||||
data Env : Set where
|
||||
ε : Env
|
||||
_,_⦂_ : Env → Id → Type → Env
|
||||
|
||||
data Term : Set where
|
||||
⌊_⌋ : Id → Term
|
||||
ƛ_⦂_⇒_ : Id → Type → Term → Term
|
||||
_·_ : Term → Term → Term
|
||||
|
||||
data _∋_⦂_ : Env → Id → Type → Set where
|
||||
|
||||
Z : ∀ {Γ A x} →
|
||||
-----------------
|
||||
Γ , x ⦂ A ∋ x ⦂ A
|
||||
|
||||
S : ∀ {Γ A B x y} →
|
||||
x ≢ y →
|
||||
Γ ∋ y ⦂ B →
|
||||
-----------------
|
||||
Γ , x ⦂ A ∋ y ⦂ B
|
||||
|
||||
data _⊢_⦂_ : Env → Term → Type → Set where
|
||||
|
||||
⌊_⌋ : ∀ {Γ A x} →
|
||||
Γ ∋ x ⦂ A →
|
||||
---------------------
|
||||
Γ ⊢ ⌊ x ⌋ ⦂ A
|
||||
|
||||
ƛ_ : ∀ {Γ x A N B} →
|
||||
Γ , x ⦂ A ⊢ N ⦂ B →
|
||||
--------------------------
|
||||
Γ ⊢ (ƛ x ⦂ A ⇒ N) ⦂ A ⇒ B
|
||||
|
||||
_·_ : ∀ {Γ L M A B} →
|
||||
Γ ⊢ L ⦂ A ⇒ B →
|
||||
Γ ⊢ M ⦂ A →
|
||||
--------------
|
||||
Γ ⊢ L · M ⦂ B
|
||||
\end{code}
|
||||
|
||||
## Test examples
|
||||
|
||||
\begin{code}
|
||||
m n s z : Id
|
||||
m = 0
|
||||
n = 1
|
||||
s = 2
|
||||
z = 3
|
||||
|
||||
z≢s : z ≢ s
|
||||
z≢s ()
|
||||
|
||||
z≢n : z ≢ n
|
||||
z≢n ()
|
||||
|
||||
s≢n : s ≢ n
|
||||
s≢n ()
|
||||
|
||||
z≢m : z ≢ m
|
||||
z≢m ()
|
||||
|
||||
s≢m : s ≢ m
|
||||
s≢m ()
|
||||
|
||||
n≢m : n ≢ m
|
||||
n≢m ()
|
||||
|
||||
Ch : Type
|
||||
Ch = (o ⇒ o) ⇒ o ⇒ o
|
||||
|
||||
two : Term
|
||||
two = ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒ (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋))
|
||||
|
||||
⊢two : ε ⊢ two ⦂ Ch
|
||||
⊢two = ƛ ƛ ⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · ⌊ ⊢z ⌋)
|
||||
where
|
||||
⊢s = S z≢s Z
|
||||
⊢z = Z
|
||||
|
||||
four : Term
|
||||
four = ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒ ⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋)))
|
||||
|
||||
⊢four : ε ⊢ four ⦂ Ch
|
||||
⊢four = ƛ ƛ ⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · ⌊ ⊢z ⌋)))
|
||||
where
|
||||
⊢s = S z≢s Z
|
||||
⊢z = Z
|
||||
|
||||
plus : Term
|
||||
plus = ƛ m ⦂ Ch ⇒ ƛ n ⦂ Ch ⇒ ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒
|
||||
⌊ m ⌋ · ⌊ s ⌋ · (⌊ n ⌋ · ⌊ s ⌋ · ⌊ z ⌋)
|
||||
|
||||
⊢plus : ε ⊢ plus ⦂ Ch ⇒ Ch ⇒ Ch
|
||||
⊢plus = ƛ ƛ ƛ ƛ ⌊ ⊢m ⌋ · ⌊ ⊢s ⌋ · (⌊ ⊢n ⌋ · ⌊ ⊢s ⌋ · ⌊ ⊢z ⌋)
|
||||
where
|
||||
⊢z = Z
|
||||
⊢s = S z≢s Z
|
||||
⊢n = S z≢n (S s≢n Z)
|
||||
⊢m = S z≢m (S s≢m (S n≢m Z))
|
||||
|
||||
four′ : Term
|
||||
four′ = plus · two · two
|
||||
|
||||
⊢four′ : ε ⊢ four′ ⦂ Ch
|
||||
⊢four′ = ⊢plus · ⊢two · ⊢two
|
||||
\end{code}
|
||||
|
||||
|
||||
# Denotational semantics
|
||||
|
||||
\begin{code}
|
||||
⟦_⟧ᵀ : Type → Set
|
||||
⟦ o ⟧ᵀ = ℕ
|
||||
⟦ A ⇒ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
|
||||
|
||||
⟦_⟧ᴱ : Env → Set
|
||||
⟦ ε ⟧ᴱ = ⊤
|
||||
⟦ Γ , x ⦂ A ⟧ᴱ = ⟦ Γ ⟧ᴱ × ⟦ A ⟧ᵀ
|
||||
|
||||
⟦_⟧ⱽ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
|
||||
⟦ Z ⟧ⱽ ⟨ ρ , v ⟩ = v
|
||||
⟦ S _ x ⟧ⱽ ⟨ ρ , v ⟩ = ⟦ x ⟧ⱽ ρ
|
||||
|
||||
⟦_⟧ : ∀ {Γ M A} → Γ ⊢ M ⦂ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
|
||||
⟦ ⌊ x ⌋ ⟧ ρ = ⟦ x ⟧ⱽ ρ
|
||||
⟦ ƛ ⊢N ⟧ ρ = λ{ v → ⟦ ⊢N ⟧ ⟨ ρ , v ⟩ }
|
||||
⟦ ⊢L · ⊢M ⟧ ρ = (⟦ ⊢L ⟧ ρ) (⟦ ⊢M ⟧ ρ)
|
||||
|
||||
_ : ⟦ ⊢four′ ⟧ tt ≡ ⟦ ⊢four ⟧ tt
|
||||
_ = refl
|
||||
|
||||
_ : ⟦ ⊢four ⟧ tt suc zero ≡ 4
|
||||
_ = refl
|
||||
\end{code}
|
||||
|
||||
|
||||
## Erasure
|
||||
|
||||
\begin{code}
|
||||
lookup : ∀ {Γ x A} → Γ ∋ x ⦂ A → Id
|
||||
lookup {Γ , x ⦂ A} Z = x
|
||||
lookup {Γ , x ⦂ A} (S _ k) = lookup {Γ} k
|
||||
|
||||
erase : ∀ {Γ M A} → Γ ⊢ M ⦂ A → Term
|
||||
erase ⌊ k ⌋ = ⌊ lookup k ⌋
|
||||
erase (ƛ_ {x = x} {A = A} ⊢N) = ƛ x ⦂ A ⇒ erase ⊢N
|
||||
erase (⊢L · ⊢M) = erase ⊢L · erase ⊢M
|
||||
\end{code}
|
||||
|
||||
### Properties of erasure
|
||||
|
||||
\begin{code}
|
||||
lookup-lemma : ∀ {Γ x A} → (k : Γ ∋ x ⦂ A) → lookup k ≡ x
|
||||
lookup-lemma Z = refl
|
||||
lookup-lemma (S _ k) = lookup-lemma k
|
||||
|
||||
erase-lemma : ∀ {Γ M A} → (⊢M : Γ ⊢ M ⦂ A) → erase ⊢M ≡ M
|
||||
erase-lemma ⌊ k ⌋ = cong ⌊_⌋ (lookup-lemma k)
|
||||
erase-lemma (ƛ_ {x = x} {A = A} ⊢N) = cong (ƛ x ⦂ A ⇒_) (erase-lemma ⊢N)
|
||||
erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M)
|
||||
\end{code}
|
||||
|
||||
|
||||
## Substitution
|
||||
|
||||
### Lists as sets
|
||||
|
||||
\begin{code}
|
||||
infix 4 _∈_
|
||||
infix 4 _⊆_
|
||||
infixl 5 _∪_
|
||||
infixl 5 _\\_
|
||||
|
||||
_∈_ : Id → List Id → Set
|
||||
x ∈ xs = Any (x ≡_) xs
|
||||
|
||||
_⊆_ : List Id → List Id → Set
|
||||
xs ⊆ ys = ∀ {w} → w ∈ xs → w ∈ ys
|
||||
|
||||
_∪_ : List Id → List Id → List Id
|
||||
xs ∪ ys = xs ++ ys
|
||||
|
||||
_\\_ : List Id → Id → List Id
|
||||
xs \\ x = filter (¬? ∘ (x ≟_)) xs
|
||||
\end{code}
|
||||
|
||||
### Properties of sets
|
||||
|
||||
\begin{code}
|
||||
⊆∷ : ∀ {y xs ys} → xs ⊆ ys → xs ⊆ y ∷ ys
|
||||
⊆∷ xs⊆ ∈xs = there (xs⊆ ∈xs)
|
||||
|
||||
∷⊆∷ : ∀ {x xs ys} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys)
|
||||
∷⊆∷ xs⊆ (here refl) = here refl
|
||||
∷⊆∷ xs⊆ (there ∈xs) = there (xs⊆ ∈xs)
|
||||
|
||||
[_]⊆ : ∀ {x xs} → [ x ] ⊆ xs → x ∈ xs
|
||||
[_]⊆ ⊆xs = ⊆xs (here refl)
|
||||
|
||||
⊆[_] : ∀ {x xs} → x ∈ xs → [ x ] ⊆ xs
|
||||
⊆[_] x∈ (here refl) = x∈
|
||||
⊆[_] x∈ (there ())
|
||||
|
||||
bind : ∀ {x xs} → xs \\ x ⊆ xs
|
||||
bind {x} {[]} ()
|
||||
bind {x} {y ∷ ys} with x ≟ y
|
||||
... | yes refl = ⊆∷ (bind {x} {ys})
|
||||
... | no _ = ∷⊆∷ (bind {x} {ys})
|
||||
|
||||
left : ∀ {xs ys} → xs ⊆ xs ∪ ys
|
||||
left (here refl) = here refl
|
||||
left (there x∈) = there (left x∈)
|
||||
|
||||
right : ∀ {xs ys} → ys ⊆ xs ∪ ys
|
||||
right {[]} y∈ = y∈
|
||||
right {x ∷ xs} y∈ = there (right {xs} y∈)
|
||||
|
||||
prev : ∀ {z y xs} → y ≢ z → z ∈ y ∷ xs → z ∈ xs
|
||||
prev y≢z (here z≡y) = ⊥-elim (y≢z (sym z≡y))
|
||||
prev _ (there z∈) = z∈
|
||||
\end{code}
|
||||
|
||||
### Free variables
|
||||
|
||||
\begin{code}
|
||||
free : Term → List Id
|
||||
free ⌊ x ⌋ = [ x ]
|
||||
free (ƛ x ⦂ A ⇒ N) = free N \\ x
|
||||
free (L · M) = free L ∪ free M
|
||||
\end{code}
|
||||
|
||||
|
||||
### Fresh identifier
|
||||
|
||||
\begin{code}
|
||||
fresh : List Id → Id
|
||||
fresh = foldr _⊔_ 0 ∘ map suc
|
||||
|
||||
⊔-lemma : ∀ {x xs} → x ∈ xs → suc x ≤ fresh xs
|
||||
⊔-lemma {x} {.x ∷ xs} (here refl) = m≤m⊔n (suc x) (fresh xs)
|
||||
⊔-lemma {x} {y ∷ xs} (there x∈) = ≤-trans (⊔-lemma {x} {xs} x∈)
|
||||
(n≤m⊔n (suc y) (fresh xs))
|
||||
|
||||
fresh-lemma : ∀ {x xs} → x ∈ xs → fresh xs ≢ x
|
||||
fresh-lemma x∈ refl = 1+n≰n (⊔-lemma x∈)
|
||||
\end{code}
|
||||
|
||||
### Identifier maps
|
||||
|
||||
\begin{code}
|
||||
∅ : Id → Term
|
||||
∅ x = ⌊ x ⌋
|
||||
|
||||
_,_↦_ : (Id → Term) → Id → Term → (Id → Term)
|
||||
(ρ , x ↦ M) y with x ≟ y
|
||||
... | yes _ = M
|
||||
... | no _ = ρ y
|
||||
\end{code}
|
||||
|
||||
### Substitution
|
||||
|
||||
\begin{code}
|
||||
subst : List Id → (Id → Term) → Term → Term
|
||||
subst xs ρ ⌊ x ⌋ = ρ x
|
||||
subst xs ρ (ƛ x ⦂ A ⇒ N) = ƛ y ⦂ A ⇒ subst (y ∷ xs) (ρ , x ↦ ⌊ y ⌋) N
|
||||
where
|
||||
y = fresh xs
|
||||
subst xs ρ (L · M) = subst xs ρ L · subst xs ρ M
|
||||
|
||||
_[_:=_] : Term → Id → Term → Term
|
||||
N [ x := M ] = subst (free M ∪ free N) (∅ , x ↦ M) N
|
||||
\end{code}
|
||||
|
||||
|
||||
## Values
|
||||
|
||||
\begin{code}
|
||||
data Value : Term → Set where
|
||||
|
||||
Fun : ∀ {x A N} →
|
||||
--------------------
|
||||
Value (ƛ x ⦂ A ⇒ N)
|
||||
\end{code}
|
||||
|
||||
## Reduction
|
||||
|
||||
\begin{code}
|
||||
infix 4 _⟹_
|
||||
|
||||
data _⟹_ : Term → Term → Set where
|
||||
|
||||
β-⇒ : ∀ {x A N V} →
|
||||
Value V →
|
||||
----------------------------------
|
||||
(ƛ x ⦂ A ⇒ N) · V ⟹ N [ x := V ]
|
||||
|
||||
ξ-⇒₁ : ∀ {L L′ M} →
|
||||
L ⟹ L′ →
|
||||
----------------
|
||||
L · M ⟹ L′ · M
|
||||
|
||||
ξ-⇒₂ : ∀ {V M M′} →
|
||||
Value V →
|
||||
M ⟹ M′ →
|
||||
----------------
|
||||
V · M ⟹ V · M′
|
||||
\end{code}
|
||||
|
||||
## Reflexive and transitive closure
|
||||
|
||||
\begin{code}
|
||||
infix 2 _⟹*_
|
||||
infix 1 begin_
|
||||
infixr 2 _⟹⟨_⟩_
|
||||
infix 3 _∎
|
||||
|
||||
data _⟹*_ : Term → Term → Set where
|
||||
|
||||
_∎ : ∀ {M} →
|
||||
-------------
|
||||
M ⟹* M
|
||||
|
||||
_⟹⟨_⟩_ : ∀ (L : Term) {M N} →
|
||||
L ⟹ M →
|
||||
M ⟹* N →
|
||||
---------
|
||||
L ⟹* N
|
||||
|
||||
begin_ : ∀ {M N} → (M ⟹* N) → (M ⟹* N)
|
||||
begin M⟹*N = M⟹*N
|
||||
\end{code}
|
||||
|
||||
## Progress
|
||||
|
||||
\begin{code}
|
||||
data Progress (M : Term) : Set where
|
||||
step : ∀ {N} → M ⟹ N → Progress M
|
||||
done : Value M → Progress M
|
||||
|
||||
progress : ∀ {M A} → ε ⊢ M ⦂ A → Progress M
|
||||
progress ⌊ () ⌋
|
||||
progress (ƛ_ ⊢N) = done Fun
|
||||
progress (⊢L · ⊢M) with progress ⊢L
|
||||
... | step L⟹L′ = step (ξ-⇒₁ L⟹L′)
|
||||
... | done Fun with progress ⊢M
|
||||
... | step M⟹M′ = step (ξ-⇒₂ Fun M⟹M′)
|
||||
... | done valM = step (β-⇒ valM)
|
||||
\end{code}
|
||||
|
||||
|
||||
## Preservation
|
||||
|
||||
### Domain of an environment
|
||||
|
||||
\begin{code}
|
||||
dom : Env → List Id
|
||||
dom ε = []
|
||||
dom (Γ , x ⦂ A) = x ∷ dom Γ
|
||||
|
||||
dom-lemma : ∀ {Γ y B} → Γ ∋ y ⦂ B → y ∈ dom Γ
|
||||
dom-lemma Z = here refl
|
||||
dom-lemma (S x≢y ⊢y) = there (dom-lemma ⊢y)
|
||||
|
||||
f : ∀ {x y} → y ∈ [ x ] → y ≡ x
|
||||
f (here y≡x) = y≡x
|
||||
f (there ())
|
||||
|
||||
g : ∀ {w xs ys} → w ∈ xs ∪ ys → w ∈ xs ⊎ w ∈ ys
|
||||
g {_} {[]} {ys} w∈ = inj₂ w∈
|
||||
g {_} {x ∷ xs} {ys} (here px) = inj₁ (here px)
|
||||
g {_} {x ∷ xs} {ys} (there w∈) with g w∈
|
||||
... | inj₁ ∈xs = inj₁ (there ∈xs)
|
||||
... | inj₂ ∈ys = inj₂ ∈ys
|
||||
|
||||
k : ∀ {w x xs} → w ∈ xs \\ x → x ≢ w
|
||||
k {w} {x} {[]} ()
|
||||
k {w} {x} {x′ ∷ xs′} w∈ with x ≟ x′
|
||||
k {w} {x} {x′ ∷ xs′} w∈ | yes refl = k {w} {x} {xs′} w∈
|
||||
k {w} {x} {x′ ∷ xs′} (here w≡x′) | no x≢x′ = λ x≡w → x≢x′ (trans x≡w w≡x′)
|
||||
k {w} {x} {x′ ∷ xs′} (there w∈) | no x≢x′ = k {w} {x} {xs′} w∈
|
||||
|
||||
h : ∀ {x xs ys} → xs ⊆ x ∷ ys → xs \\ x ⊆ ys
|
||||
h {x} {xs} {ys} xs⊆ {w} w∈ with xs⊆ (bind w∈)
|
||||
... | here w≡x = ⊥-elim (k {w} {x} {xs} w∈ (sym w≡x))
|
||||
... | there w∈′ = w∈′
|
||||
|
||||
free-lemma : ∀ {Γ M A} → Γ ⊢ M ⦂ A → free M ⊆ dom Γ
|
||||
free-lemma ⌊ ⊢x ⌋ w∈ rewrite f w∈ = dom-lemma ⊢x
|
||||
free-lemma {Γ} (ƛ_ {x = x} {N = N} ⊢N) = h ih
|
||||
where
|
||||
ih : free N ⊆ x ∷ dom Γ
|
||||
ih = free-lemma ⊢N
|
||||
free-lemma (⊢L · ⊢M) w∈ with g w∈
|
||||
... | inj₁ ∈L = free-lemma ⊢L ∈L
|
||||
... | inj₂ ∈M = free-lemma ⊢M ∈M
|
||||
\end{code}
|
||||
|
||||
Wow! A lot of work to prove stuff that is obvious. Gulp!
|
||||
|
||||
### Renaming
|
||||
|
||||
\begin{code}
|
||||
∷drop : ∀ {v vs ys} → v ∷ vs ⊆ ys → vs ⊆ ys
|
||||
∷drop ⊆ys ∈vs = ⊆ys (there ∈vs)
|
||||
|
||||
i : ∀ {w x xs} → w ∈ xs → x ≢ w → w ∈ xs \\ x
|
||||
i {w} {x} {.w ∷ xs} (here refl) x≢w with x ≟ w
|
||||
... | yes refl = ⊥-elim (x≢w refl)
|
||||
... | no _ = here refl
|
||||
i {w} {x} {y ∷ xs} (there w∈) x≢w with x ≟ y
|
||||
... | yes refl = (i {w} {x} {xs} w∈ x≢w)
|
||||
... | no _ = there (i {w} {x} {xs} w∈ x≢w)
|
||||
|
||||
j : ∀ {x xs ys} → xs \\ x ⊆ ys → xs ⊆ x ∷ ys
|
||||
j {x} {xs} {ys} ⊆ys {w} w∈ with x ≟ w
|
||||
... | yes refl = here refl
|
||||
... | no x≢w = there (⊆ys (i w∈ x≢w))
|
||||
|
||||
⊢rename : ∀ {Γ Δ xs} → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) →
|
||||
(∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
|
||||
⊢rename ⊢σ ⊆xs (⌊ ⊢x ⌋) = ⌊ ⊢σ ∈xs ⊢x ⌋
|
||||
where
|
||||
∈xs = [_]⊆ ⊆xs
|
||||
⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N)
|
||||
= ƛ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N) -- ⊆xs : free N \\ x ⊆ xs
|
||||
where
|
||||
Γ′ = Γ , x ⦂ A
|
||||
Δ′ = Δ , x ⦂ A
|
||||
xs′ = x ∷ xs
|
||||
|
||||
⊢σ′ : ∀ {y B} → y ∈ xs′ → Γ′ ∋ y ⦂ B → Δ′ ∋ y ⦂ B
|
||||
⊢σ′ ∈xs′ Z = Z
|
||||
⊢σ′ ∈xs′ (S x≢y k) with ∈xs′
|
||||
... | here refl = ⊥-elim (x≢y refl)
|
||||
... | there ∈xs = S x≢y (⊢σ ∈xs k)
|
||||
|
||||
⊆xs′ : free N ⊆ xs′
|
||||
⊆xs′ = j ⊆xs
|
||||
⊢rename {xs = xs} ⊢σ {L · M} ⊆xs (⊢L · ⊢M) = ⊢rename ⊢σ (⊆xs ∘ left) ⊢L · ⊢rename ⊢σ (⊆xs ∘ right) ⊢M
|
||||
\end{code}
|
||||
|
||||
|
||||
### Substitution preserves types
|
||||
|
||||
\begin{code}
|
||||
⊢subst : ∀ {Γ Δ xs ρ} →
|
||||
(∀ {x} → x ∈ xs → free (ρ x) ⊆ xs) →
|
||||
(∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ⊢ ρ x ⦂ A) →
|
||||
(∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ subst xs ρ M ⦂ A)
|
||||
⊢subst Σ ⊢ρ ⊆xs ⌊ ⊢x ⌋ = ⊢ρ (⊆xs (here refl)) ⊢x
|
||||
⊢subst {Γ} {Δ} {xs} {ρ} Σ ⊢ρ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N)
|
||||
= ƛ ⊢subst {Γ′} {Δ′} {xs′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N
|
||||
where
|
||||
y = fresh xs
|
||||
Γ′ = Γ , x ⦂ A
|
||||
Δ′ = Δ , y ⦂ A
|
||||
xs′ = y ∷ xs
|
||||
ρ′ = ρ , x ↦ ⌊ y ⌋
|
||||
|
||||
Σ′ : ∀ {z} → z ∈ xs′ → free (ρ′ z) ⊆ xs′
|
||||
Σ′ (here refl) = {!!}
|
||||
Σ′ (there x∈) = {!!}
|
||||
|
||||
⊆xs′ : free N ⊆ xs′
|
||||
⊆xs′ = {!!}
|
||||
|
||||
⊢σ : ∀ {z C} → z ∈ xs → Δ ∋ z ⦂ C → Δ′ ∋ z ⦂ C
|
||||
⊢σ z∈ ⊢z = S (fresh-lemma z∈) ⊢z
|
||||
|
||||
⊢ρ′ : ∀ {z C} → z ∈ xs′ → Γ′ ∋ z ⦂ C → Δ′ ⊢ ρ′ z ⦂ C
|
||||
⊢ρ′ _ Z with x ≟ x
|
||||
... | yes _ = ⌊ Z ⌋
|
||||
... | no x≢x = ⊥-elim (x≢x refl)
|
||||
⊢ρ′ {z} z∈ (S x≢z ⊢z) with x ≟ z
|
||||
... | yes x≡z = ⊥-elim (x≢z x≡z)
|
||||
... | no _ = ⊢rename {Δ} {Δ′} {xs} ⊢σ (Σ (prev {!!} z∈)) (⊢ρ {!!} ⊢z)
|
||||
|
||||
⊢subst {xs = xs} Σ ⊢ρ {L · M} ⊆xs (⊢L · ⊢M) = ⊢subst Σ ⊢ρ L⊆xs ⊢L · ⊢subst Σ ⊢ρ M⊆xs ⊢M
|
||||
where
|
||||
L⊆xs : free L ⊆ xs
|
||||
L⊆xs = {!!}
|
||||
M⊆xs : free M ⊆ xs
|
||||
M⊆xs = {!!}
|
||||
|
||||
⊢substitution : ∀ {Γ x A N B M} →
|
||||
Γ , x ⦂ A ⊢ N ⦂ B →
|
||||
Γ ⊢ M ⦂ A →
|
||||
--------------------
|
||||
Γ ⊢ N [ x := M ] ⦂ B
|
||||
⊢substitution {Γ} {x} {A} {N} {B} {M} ⊢N ⊢M =
|
||||
⊢subst {Γ′} {Γ} {xs} {ρ} Σ ⊢ρ {N} {B} ⊆xs ⊢N
|
||||
where
|
||||
Γ′ = Γ , x ⦂ A
|
||||
xs = free M ∪ free N
|
||||
ρ = ∅ , x ↦ M
|
||||
|
||||
Σ : ∀ {x} → x ∈ xs → free (ρ x) ⊆ xs
|
||||
Σ {y} y∈ with x ≟ y
|
||||
... | no _ = ⊆[_] y∈
|
||||
... | yes _ = {!!} -- left
|
||||
|
||||
⊢ρ : ∀ {z C} → z ∈ xs → Γ′ ∋ z ⦂ C → Γ ⊢ ρ z ⦂ C
|
||||
⊢ρ {.x} z∈ Z with x ≟ x
|
||||
... | yes _ = ⊢M
|
||||
... | no x≢x = ⊥-elim (x≢x refl)
|
||||
⊢ρ {z} z∈ (S x≢z ⊢z) with x ≟ z
|
||||
... | yes x≡z = ⊥-elim (x≢z x≡z)
|
||||
... | no _ = ⌊ ⊢z ⌋
|
||||
|
||||
⊆xs : free N ⊆ xs
|
||||
⊆xs = {!!}
|
||||
\end{code}
|
||||
|
||||
Can I falsify the theorem? Consider the case where the renamed variable
|
||||
already exists in the environment.
|
||||
|
||||
(ƛ f ⦂ o ⇒ g) [ f := (ƛ z ⦂ o ⇒ z)]
|
||||
|
||||
Since I only rename to variables guaranteed not to be free in M and M is closed,
|
||||
I could accidentally rename f to g. So I must instead pick all the variables
|
||||
free in M and N.
|
||||
|
||||
In that case, could I still falsify preservation of typing? Let's say we have:
|
||||
|
||||
ε , g ⦂ A , h ⦂ B ⊢ (ƛ f ⦂ o ⇒ o ⇒ g) ⦂ (o ⇒ o) ⇒ A
|
||||
ε , g ⦂ A , h ⦂ B ⊢ (ƛ z ⦂ o ⇒ z) ⦂ o ⇒ o
|
||||
|
||||
And let's say I rename f to h. Then the result is:
|
||||
|
||||
ε , g ⦂ A , h ⦂ B ⊢ λ h ⦂ o ⇒ g
|
||||
|
||||
Then `y≢` in the body of `⊢subst` is falsified, which could be an issue!
|
||||
|
||||
### Preservation
|
||||
|
||||
\begin{code}
|
||||
{-
|
||||
preservation : ∀ {Γ M N A} → Γ ⊢ M ⦂ A → M ⟹ N → Γ ⊢ N ⦂ A
|
||||
preservation ⌊ ⊢x ⌋ ()
|
||||
preservation (ƛ ⊢N) ()
|
||||
preservation (⊢L · ⊢M) (ξ-⇒₁ L⟹L′) = preservation ⊢L L⟹L′ · ⊢M
|
||||
preservation (⊢V · ⊢M) (ξ-⇒₂ valV M⟹M′) = ⊢V · preservation ⊢M M⟹M′
|
||||
preservation ((ƛ ⊢N) · ⊢W) (β-⇒ valW) = ⊢substitution ⊢N ⊢W
|
||||
-}
|
||||
\end{code}
|
||||
|
||||
|
||||
|
||||
Loading…
Reference in a new issue