Stlc theory #454
Stlc theory #454
Conversation
|
|
||
| Here is why it's called capture-avoiding: if our lambda binds the | ||
| variable name again, we don't substitute inside. In other words, the | ||
| substituion `(λ y. y) y [y := k]`{.Agda} yields `(λ y. y) k`{.Agda}, |
There was a problem hiding this comment.
| substituion `(λ y. y) y [y := k]`{.Agda} yields `(λ y. y) k`{.Agda}, | |
| substitution `(λ y. y) y [y := k]`{.Agda} yields `(λ y. y) k`{.Agda}, |
|
|
||
| ```agda | ||
| data Value : Expr → Type where | ||
| v-var : ∀ n → Value (` n) |
There was a problem hiding this comment.
Do we really want to consider open terms here? Typically, we either define values as closed terms, or include neutrals.
There was a problem hiding this comment.
I was following off PLFA here - they appear to define them as general terms, with no closed requirement. It does seem reasonable to constrain them, though.
There was a problem hiding this comment.
As far as I can tell values do not contain variables in PLFA. (They may still contain open terms like λ x. y)
|
|
||
| ```agda | ||
| `λ x f [ n := e ] with x ≡? n | ||
| ... | yes _ = `λ x f |
There was a problem hiding this comment.
What happens when e contains x as a free variable? If we are treating the Nats as nominal vars, then we have accidentally performed a capture!
For instance, λ x (` y) [ y := x ] ≡ λ x (` x), yet λ a (` y) [ y := x ] ≡ λ a (` x), so substitution is no longer stable under alpha-equivalence. To fix this, you need to rename x to a variable that is not free in e when doing the substitution.
| `U : Expr | ||
| ``` | ||
|
|
||
| <details><summary>Some application lemmas, for convinience.</summary> |
There was a problem hiding this comment.
| <details><summary>Some application lemmas, for convinience.</summary> | |
| <details><summary>Some application lemmas, for convenience.</summary> |
| Here is why it's called capture-avoiding: if our lambda binds the | ||
| variable name again, we don't substitute inside. In other words, the | ||
| substituion `(λ y. y) y [y := k]`{.Agda} yields `(λ y. y) k`{.Agda}, |
There was a problem hiding this comment.
That's not actually what "capture-avoiding" refers to; see Reed's comment. The capture-avoiding part is α-renaming the λ-term we're substituting into so that its binder does not capture any of the free variables in the substitute.
| Preservation states that if a well typed expression $x$ steps to another $x'$, | ||
| they have the same type (i.e., stepping preserves type.) | ||
|
|
||
| The first step in proving these is showing that a "proper" substituion |
There was a problem hiding this comment.
| The first step in proving these is showing that a "proper" substituion | |
| The first step in proving these is showing that a "proper" substitution |
| Γ ⊢ bd [ n := s ] ⦂ typ | ||
| ``` | ||
|
|
||
| In the case of variables, we use weakening for the substituion itself, |
There was a problem hiding this comment.
| In the case of variables, we use weakening for the substituion itself, | |
| In the case of variables, we use weakening for the substitution itself, |
|
I'm going to not push anything up here for a little bit while I work on the substitution problem; I feel like it's going to be quite messy while I figure it all out. |
Description
Added a very simple STLC, alongside several properties. Still WIP.
Checklist
Before submitting a merge request, please check the items below:
support/sort-imports.hs(ornix run --experimental-features nix-command -f . sort-imports).