In A New Approach to Abstract Syntax with Variable Binding, Pitts and Gabbay describe a "freshness" quantifier for their variant of set theory, where you can quantify over fresh names. This allows you to describe freshness conditions in a more formal way than the usual "x does not occur in M," and even reason about fresh names with formal logic. The quantification N x can be read: "for fresh x ..." This has a cool, dual universal/existential property: because the ambient universe of names is infinite, it's always true that there exists a fresh x, and because we don't care which one we choose, any proposition we prove using the freshness quantifier holds for all such fresh names.
What confused me for a while was that the quantifier just says "x is fresh;" it doesn't say "x is fresh with respect to M". But it seemed like if you take a name that's fresh at one point, but then use it in another context, you might have accidentally picked a name that conflicted with a name in the new context. In other words, I was concerned that having a local freshness condition without talking globally about all the names you're ever going to use doesn't carry enough information to avoid an incorrect choice of fresh name.
You have to dig a little deeper to see why this isn't a problem. The real meaning of the quantifier comes from the idea that the universe of names is infinite, but the construction of any particular term only involves a finite number of names. So not only can you find a fresh name at any point; but you can in fact choose any name other than the ones used in that term. So all but finitely many names are fresh. This is the more precise interpretation of N x: "for all but finitely many names x ..."
So the freshness quantifier isn't actually committing to a name. It's just saying that there's a huge set of names for which the proposition holds. Thus moving in and out of scope of particular terms doesn't affect the truth of a proposition built with the quantifier, because while the particular set of fresh names might change, the fact that that set involves all but a finite number of names does not. This allows us to abstract away from the actual choice of fresh names in a program when we're writing propositions about them.
Subscribe to:
Post Comments (Atom)
3 comments:
So, any term is finite. Okay, so that gives us an idea of the finite set of names where the proposition is not guaranteed to hold.
But what about an infinite reduction sequence? If we want to choose a name for a fresh variable at some point, isn't it possible that we'll need to ensure that all future terms in the reduction sequence don't use that name?
I haven't fully digested Pitts+Gabay, so I'm really asking an honest question, not trying to be snarky or point out a flaw in their paper.
Perhaps there's a simple inductive argument that ensures that at every point, we will always choose a new name that doesn't match any name in our past, and so all those past names are safe from, um, "unfreshness". . .
I'm pretty sure infinite reduction sequences are irrelevant. All that matters is that the name be fresh with respect to the term, which is always finite. So you're perfectly allowed to reuse a name that you used earlier in the reduction sequence, as long as it's free with respect to the current program.
Now, I wonder about infinite programs like Böhm trees. Although I don't know if they actually only use a finite number of names even though the term is itself infinite.
In a sense, they kind of punt on these questions and simply assert by fiat that there must always be some name available: one of the axioms of their set theory guarantees the existence of fresh names:
(Fresh) ∀a ∈ A . (a # x)
(A is the ambient universe of names, # means roughly "is fresh w.r.t...", and x is any set.)
...as long as it's free with respect to the current program.
s/free/fresh
Post a Comment