I spent a few days recently trying to come up with some formalism for the notion of names, namespaces and name resolution.
On the surface, it seems bigraphs might be a fruitful approach. The orthogonal treatment of locality and connectivity maps fairly well onto name structure (e.g, Module.X.foo, /foo/bar/hello.txt or foo.example.org) and redirection (e.g., symlinks or CNAMEs). Bigraph reaction rules could then model name resolution. A resolution process can move through the hierarchical name structure and across links at which point you might have some interesting properties to prove or check about a particular namespace system. Additionally, namespaces and resolution mechanism might compose in different ways and this might be worth formalising and comparing.
I didn't get much further than modelling some bits of a filesystem in BigraphER.
# filesystem
ctrl Dir = 0;
atomic ctrl File = 1;
atomic ctrl SymLink = 2;
# Query -- the thing that gets resolved.
atomic ctrl Q = 1;
# Reaction Rules
react resolve_symlink =
Q{x} | SymLink{x, y} --> Q{y} | SymLink{x, y};
# Initial State
big s0 =
Dir.
(SymLink{sym_a, file_a}
|
Q{sym_a}
|
File{file_a}
);
# Bigraphical Reactive System
begin brs
init s0;
rules = [ {resolve_symlink} ];
endResulting in these two transition states.
Bear in mind this was just a quick experiment. The first bigraph shows our query at sym_a and the second bigraph (using the resolve_symlink reduction rule) shows the query at file_a. All of this takes places within Dir. It seems that BigraphER represents the tree structure graphically with black arrows (rather than spatial containment).