31 lines
1.1 KiB
Markdown
31 lines
1.1 KiB
Markdown
Here's my formal definition of substitution. Since I wasn't in class last week, I'm not sure what notational conventions are being used, so I'll define my grammar first.
|
|
|
|
```ebnf
|
|
n, m :: Nat
|
|
a, b, c :: Term ::= n | λ b | b a
|
|
r :: Nat -> Nat
|
|
```
|
|
|
|
I'm using simultaneous renamings r mapping from indices to indices. Lifting a renaming means weakening by 1, so the new mapping refers to the previous entry in the old mapping, and increments what it maps to, defined below.
|
|
|
|
```haskell
|
|
lift :: (Nat → Nat) → Nat → Nat
|
|
lift r n = if n == 0 then 0 else (r (n - 1)) + 1
|
|
```
|
|
|
|
Applying a renaming requires lifting it when going under a binder.
|
|
|
|
```haskell
|
|
rename :: (Nat → Nat) → Term → Term
|
|
rename r n = r n
|
|
rename r (b a) = (rename r b) (rename r a)
|
|
rename r (λ b) = λ (rename (lift r) b)
|
|
```
|
|
|
|
I denote substitution as `b{c/n}`, replacing the index `n` by `c` inside of `b`. Renaming by incrementing `1` is used when going under a binder so that the `c`'s zeroth indices don't get captured.
|
|
|
|
```haskell
|
|
n{c/m} = if n == m then c else n
|
|
(b a){c/m} = b{c/m} a{c/m}
|
|
(λ b){c/m} = let c' = rename (+ 1) c in λ (b{c'/m})
|
|
``` |