Maps (Substitutions) With Infinite Domains

Question

Finite maps model substitutions with finite domains. I either need to emulate operations on substitutions with infinite domains, or find a suitable way to represent substitutions with infinite domains. For instance, consider the restriction operation on substitutions:

• σ|_e(x_n) = if x_n ∈ FV(e) then σ(x_n) else x_n

Because the restriction operation applies to all variables in a possibly infinite set, a data type like a finite map can't "look forward" to anticipate the restriction when new bindings are added. And of course, using finite maps with infinite domains causes nontermination. Is there a way to simulate operations such as restriction using finite maps, or another representation of substitutions that would allow one to write operations like restriction over them easily? I feel I'm overlooking an obvious solution - for instance, taking advantage of lazy evaluation or functional substitutions.

edit:

For reference, here is a naive solution using finite maps. Each time the restriction operation is applied to a substitution σ and expression e, find the set FV(e) of free variables of e. For each variable x_n in the domain of σ, if x_n ∈ FV(e) then set σ'(x_n) = x_n. Return σ'. Assume that σ'(x_n) = x_n if x_n ∉ dom(σ').

edit: This is the obvious solution I overlooked.

Answer 1

Well, the most direct model of a substitution is just a function itself.

newtype Subst = Subst { apply :: Var -> Expr }

singleton :: Var -> Expr -> Subst
singleton v e = Subst (\v' -> if v == v' then e else Var v')
-- etc.

For a first pass at implementing a lanugage, this is probably what I would use as soon as finite maps broke down. It's not fast (will require O(n) time when n is the size of the domain), but it's simple. Keep it encapsulated so you can replace it later.

If you start getting hit by the O(n) time, then you could switch to a trie. data-inttrie was specifically written to behave just like a function on integers but allow efficient modifications at single points (as one would want with a substitution function). If your variables are uniquely identified by integers you could use it directly, otherwise you could emulate the style for strings or whatever you are using.

But it also seems odd to me that you would need to "look forward". I have never needed this in my language implementations; if you add a new binding to a restricted substitution, the restriction does not apply to the new bindings (if it did, the semantics would be wrong). Finite maps have done the trick for all cases when I am not doing something absurdly weird (and those don't usually pan out).