{
localUrl: '../page/locale.html',
arbitalUrl: 'https://arbital.com/p/locale',
rawJsonUrl: '../raw/8vb.json',
likeableId: '4098',
likeableType: 'page',
myLikeValue: '0',
likeCount: '2',
dislikeCount: '0',
likeScore: '2',
individualLikes: [
'KevinClancy',
'8xl'
],
pageId: 'locale',
edit: '6',
editSummary: '',
prevEdit: '5',
currentEdit: '6',
wasPublished: 'true',
type: 'wiki',
title: 'Locale',
clickbait: 'Topology - but right',
textLength: '7526',
alias: 'locale',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'AdeleLopez',
editCreatedAt: '2018-11-18 20:15:32',
pageCreatorId: 'AdeleLopez',
pageCreatedAt: '2017-11-29 05:02:16',
seeDomainId: '0',
editDomainId: '122',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '0',
isEditorComment: 'false',
isApprovedComment: 'false',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '15',
text: '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. \n\nThey 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.\nSee Peter Johnstone's [The point of pointless topology](http://pointlesstopology.com/the-point-of-pointless-topology.pdf) for an overview of these benefits.\n\n#Why locales?\nLocales 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**. %%note: 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!%%\n\nObservations can have more or less information. This gives them a [3rb poset] structure. We say that the more specific open *refines* the more generic open. To say $A$ refines $B$, we write $A\\le B$. A witness affirming $A$ will also affirm $B$. \n\nObservations can be combined to make a higher information observation. We call this combination the **meet** of our observations, and write it as $\\bigwedge A_i$ or $A \\wedge B$. Think of this as $A$ *and* $B$. If incompatible observations are combined, we get the bottom element of the poset: $\\bot$ -- 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. \n\nObservations can cover an arbitrary set of observations as specific possibilities. We call this the **join** of our opens, and write it as $\\bigvee A_i$ or $A \\vee B$. Think of this as $A$ *or* $B$. Together with finite meets, this gives the locale a [46c lattice] structure. The top element of the poset $\\top$ 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.\n\nJoins and meets must be compatible with each other. In particular, they must satisfy the distributive law: $A\\wedge \\bigvee A_i = \\bigvee (A \\wedge A_i)$. Again, this is modeling the natural logic of how combining information from observations works. \n\n\n%%hidden(So are locales the one right way to model observations?): 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.%%\n\n## Points\nObservations 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. %%note: i.e. locales are automatically $T_0$ separated. %% \n\nIf 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.\n\n%%todo:\n## Category perspective\nA poset can be considered as a category, the elements are the objects, and the order relation defines the morphisms: $A \\le B$ implies there's a morphism $A \\rightarrow B$. The meet is then the product, and the join is the coproduct! Initial object of course is $\\bot$, and final object is $\\top$. Morphisms can also be interpreted as logical implication!\n \n\nLocales themselves can be the object of a category. In fact, they are the objects of multiple important categories!\n%%\n\n## Morphisms\n\nWhat is a morphism of locales? Let's think about this in terms of observations. Say we have locales $A$ and $B$, and a computable process $f$ which takes points in $A$ to points in $B$. %%note: 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.%%\n\nFor concreteness, say that $A$ is a locale representing the space in a glass slide, $B$ is a locale representing a computer monitor, and $f$ is a microscope which can look at the slide and project its view to the monitor. \n\nAn observation which we make on the monitor gives us (via $f$ the microscope) an observation on the slide. More generally, we can map opens of $B$ to opens of $A$.\n\nNow consider what happens if combine a set $S$ of opens on $B$. We don't expect our computable process to effect how the observations combine. So in other words, we expect $f(\\vee S) = \\vee f(S)$, and if $S$ is finite, $f(\\wedge S) = \\wedge f(S)$. \n\nWe call a morphism $f:A\\rightarrow B$ satisfying these properties a _continuous map_. If our locales are spatial, this corresponds exactly to a continuous function between topological spaces!\n\n# Examples\n\n## The locale of real numbers\n\nOpens are generated by rational intervals. \n\n## More examples\n\n - The 3D space that we live in\n - The open sets of any topology\n - Logical propositions \n\n#Important concepts\n- Sublocale\n- Separation\n - Regularity is the most natural separation axiom, not Hausdorff (which *can* be defined for locales)\n- Compactness\n- Fundamental groupoid\n - Much intuitively clearer to define and use!\n\n#How do we use them?\n##Conceptual clarity\n\nI'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! \n\n##Constructive analysis\nThe 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!\n\n- Heine-Borel\n- Constructive Tychonoff!\n\n\n\n\n#References\n\n 1. Topology via Logic by Stephen Vickers\n 2. Stone Spaces by Peter Johnstone\n 3. [Locale - nLab](https://ncatlab.org/nlab/show/locale)',
metaText: '',
isTextLoaded: 'true',
isSubscribedToDiscussion: 'false',
isSubscribedToUser: 'false',
isSubscribedAsMaintainer: 'false',
discussionSubscriberCount: '1',
maintainerCount: '1',
userSubscriberCount: '0',
lastVisit: '',
hasDraft: 'false',
votes: [],
voteSummary: 'null',
muVoteSummary: '0',
voteScaling: '0',
currentUserVote: '-2',
voteCount: '0',
lockedVoteType: '',
maxEditEver: '0',
redLinkCount: '0',
lockedBy: '',
lockedUntil: '',
nextPageId: '',
prevPageId: '',
usedAsMastery: 'false',
proposalEditNum: '0',
permissions: {
edit: {
has: 'false',
reason: 'You don't have domain permission to edit this page'
},
proposeEdit: {
has: 'true',
reason: ''
},
delete: {
has: 'false',
reason: 'You don't have domain permission to delete this page'
},
comment: {
has: 'false',
reason: 'You can't comment in this domain because you are not a member'
},
proposeComment: {
has: 'true',
reason: ''
}
},
summaries: {},
creatorIds: [
'AdeleLopez'
],
childIds: [],
parentIds: [],
commentIds: [],
questionIds: [],
tagIds: [],
relatedIds: [],
markIds: [],
explanations: [],
learnMore: [],
requirements: [],
subjects: [],
lenses: [],
lensParentId: '',
pathPages: [],
learnMoreTaughtMap: {},
learnMoreCoveredMap: {},
learnMoreRequiredMap: {},
editHistory: {},
domainSubmissions: {},
answers: [],
answerCount: '0',
commentCount: '0',
newCommentCount: '0',
linkedMarkCount: '0',
changeLogs: [
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '23128',
pageId: 'locale',
userId: 'AdeleLopez',
edit: '6',
type: 'newEdit',
createdAt: '2018-11-18 20:15:32',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '23127',
pageId: 'locale',
userId: 'AdeleLopez',
edit: '5',
type: 'newEdit',
createdAt: '2018-11-18 19:32:53',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '23126',
pageId: 'locale',
userId: 'AdeleLopez',
edit: '4',
type: 'newEdit',
createdAt: '2018-11-18 19:26:03',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '23125',
pageId: 'locale',
userId: 'AdeleLopez',
edit: '0',
type: 'newAlias',
createdAt: '2018-11-18 19:24:30',
auxPageId: '',
oldSettingsValue: '8vb',
newSettingsValue: 'locale'
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '23124',
pageId: 'locale',
userId: 'AdeleLopez',
edit: '3',
type: 'newEdit',
createdAt: '2018-11-18 19:17:49',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '22901',
pageId: 'locale',
userId: 'AdeleLopez',
edit: '2',
type: 'newEdit',
createdAt: '2017-11-29 05:17:40',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '22900',
pageId: 'locale',
userId: 'AdeleLopez',
edit: '1',
type: 'newEdit',
createdAt: '2017-11-29 05:02:16',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'false',
hasParents: 'false',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}