A locale is a structure which captures the relations between possible observations. This fact is an important insight into why topological spaces show up so often when thinking about artificial intelligence. In particular, this gives us to key to understanding why computable functions are continuous.
They are very similar to topological spaces -- the open sets of any topology form a locale. However, they have better properties than topologies in many contexts. For example, they're easier to work with when constructive math is required. See Peter Johnstone's The point of pointless topology for an overview of these benefits.
Locales model observations, and thus turn up in a very wide variety of contexts. In particular, they model affirmable observations - observations which, if true, can be affirmed by a witness. For example, "Some crows are black" is an affirmable observation, since we could affirm it by the existence of a black crow. On the other hand, "All crows are black" is not an affirmable observation. The locale is a system of affirmable observations which we call opens. [1]
Observations can have more or less information. This gives them a poset structure. We say that the more specific open refines the more generic open. To say refines , we write . A witness affirming will also affirm .
Observations can be combined to make a higher information observation. We call this combination the meet of our observations, and write it as or . Think of this as and . If incompatible observations are combined, we get the bottom element of the poset: -- representing false. We can only combine a finite number of observations -- that's because we are modeling observations that can be computably affirmed, we can't really observe something if it takes an infinite amount of time to observe it.
Observations can cover an arbitrary set of observations as specific possibilities. We call this the join of our opens, and write it as or . Think of this as or . Together with finite meets, this gives the locale a lattice structure. The top element of the poset represents true, and is the most generic observation. We can observe the join of an infinite number of opens because to affirm this join, we only need to have a witness from one of the opens in the join.
Joins and meets must be compatible with each other. In particular, they must satisfy the distributive law: . Again, this is modeling the natural logic of how combining information from observations works.
There are some ontological commitments that locales make: that the order of observations doesn't matter, and that observations don't affect the world. Quantales generalize locales to remove these commitments! Are quantales the one right way? Well, it's hard to notice what other commitments we might be implicitly making. Also, quantales are a lot harder to work with, which means we try to avoid using them if we don't need them. In general, there isn't a single right way to model something -- it depends a lot on what exactly you're trying to do with it.
Observations represent the kinds of information we can have about where something is. A point is then an exact place where something can be. In a topological space, observations correspond to sets of points, but in a locale, we can be more flexible. We also don't have to worry about points that have no possible observations that can distinguish them. [2]
If a locale has enough points so that we can define the opens as sets of points, we say the locale is spatial. Typically, the locales we are interested in will be spatial.
What is a morphism of locales? Let's think about this in terms of observations. Say we have locales and , and a computable process which takes points in to points in . [3]
For concreteness, say that is a locale representing the space in a glass slide, is a locale representing a computer monitor, and is a microscope which can look at the slide and project its view to the monitor.
An observation which we make on the monitor gives us (via the microscope) an observation on the slide. More generally, we can map opens of to opens of .
Now consider what happens if combine a set of opens on . We don't expect our computable process to effect how the observations combine. So in other words, we expect , and if is finite, .
We call a morphism satisfying these properties a continuous map. If our locales are spatial, this corresponds exactly to a continuous function between topological spaces!
Opens are generated by rational intervals.
I've found that replacing topological spaces with locales typically brings about conceptual clarity when working on something. This effect seems to be stronger the less obvious it is to make the replacement. Topological spaces bring lots of baggage with them, with all the sets and the axiom of choice. Once these have been dropped, it becomes easier to see what's actually going on, to move! Think of this as analogous to replacing Roman numerals with Arabic numerals - it's not really that you can do anything that you couldn't do before, it just becomes significantly easier to do things!
The real line always felt like such a complicated thing to drag into the laws of physics; there must be something better! In order to do physics with that something, we'd better be able to do analysis. Luckily, locales are very promising in this regard!
The example "All crows are black" is however a refutable observation, since the existence of a white crow would refute it. Refutable observations are called closeds, and are also a part of the locale structure. We incorporate them by identifying them with their negations, which are affirmative!
i.e. locales are automatically separated.
The locales don't need to be spatial for this to work, but it's easier to motivate the definition if we can reference points.