Caristi fixed-point theorem

In domain theory, a branch of mathematics and computer science, a Scott information system is a primitive kind of logical deductive system often used as an alternative way of presenting Scott domains.

Definition

A Scott information system, A, is an ordered triple $(T,Con,\vdash )$

• $T{\mbox{ is a set of tokens (the basic units of information)}}$
• $Con\subseteq {\mathcal {P}}_{f}(T){\mbox{ the finite subsets of T}}$
• $\vdash \subseteq (Con\setminus \lbrace \emptyset \rbrace )\times T$

satisfying

1. ${\mbox{If }}a\in X\in Con{\mbox{ then }}X\vdash a$
2. ${\mbox{If }}X\vdash Y{\mbox{ and }}Y\vdash a{\mbox{, then }}X\vdash a$
3. ${\mbox{If }}X\vdash a{\mbox{ then }}X\cup \{a\}\in Con$
4. $\forall a\in T:\{a\}\in Con$
5. ${\mbox{If }}X\in Con{\mbox{ and }}X^{\prime }\,\subseteq X{\mbox{ then }}X^{\prime }\in Con.$

Here $X\vdash Y$ means $\forall a\in Y,X\vdash a.$

Examples

Natural numbers

The return value of a partial recursive function, which either returns a natural number or goes into an infinite recursion, can be expressed as a simple Scott information system as follows:

• $T:=\mathbb {N}$
• $Con:=\{\emptyset \}\cup \{\{n\}\mid n\in \mathbb {N} \}$
• $X\vdash a{\mbox{ iff }}a\in X.$

That is, the result can either be a natural number, represented by the singleton set $\{n\}$, or "infinite recursion," represented by $\emptyset$.

Of course, the same construction can be carried out with any other set instead of $\mathbb {N}$.

Propositional calculus

The propositional calculus gives us a very simple Scott information system as follows:

• $T:=\{\phi \mid \phi {\mbox{ is satisfiable}}\}$
• $Con:=\{X\in {\mathcal {P}}_{f}(T)\mid X{\mbox{ is consistent}}\}$
• $X\vdash a{\mbox{ iff }}X\vdash a{\mbox{ in the propositional calculus}}.$

Scott domains

Let D be a Scott domain. Then we may define an information system as follows

• $T:=D^{0}$ the set of compact elements of D
• $Con:=\{X\in {\mathcal {P}}_{f}(T)\mid X{\mbox{ has an upper bound}}\}$
• $X\vdash d{\mbox{ iff }}d\sqsubseteq \bigsqcup X.$

Let ${\mathcal {I}}$ be the mapping that takes us from a Scott domain, D, to the information system defined above.

Information systems and Scott domains

Given an information system, $A=(T,Con,\vdash )$, we can build a Scott domain as follows.

• Definition: $x\subseteq T$ is a point iff
  • ${\mbox{If }}X\subseteq _{f}x{\mbox{ then }}X\in Con$
  • ${\mbox{If }}X\vdash a{\mbox{ and }}X\subseteq _{f}x{\mbox{ then }}a\in x.$

Let ${\mathcal {D}}(A)$ denote the set of points of A with the subset ordering. ${\mathcal {D}}(A)$ will be a countably based Scott domain when T is countable. In general, for any Scott domain D and information system A

• ${\mathcal {D}}({\mathcal {I}}(D))\cong D$
• ${\mathcal {I}}({\mathcal {D}}(A))\cong A$

where the second congruence is given by approximable mappings.

See also

• Scott domain
• Domain theory

References

• Glynn Winskell: "The Formal Semantics of Programming Languages: An Introduction", MIT Press, 1993 (chapter 12)