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,⊢)$

• $T\text{ is a set of tokens (the basic units of information)}$
• $Con\subseteq {𝒫}_f(T)\text{ the finite subsets of T}$
• $⊢\subseteq (Con\setminus \{\mathrm{\varnothing }\})\times T$

satisfying

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

Here $X⊢Y$ means $\mathrm{\forall }a\in Y,X⊢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:=\{\mathrm{\varnothing }\}\cup \{\{n\}\mid n\in \mathbb{N}\}$
• $X⊢a\text{ 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 $\mathrm{\varnothing }$.

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:=\{\varphi \mid \varphi \text{ is satisfiable}\}$
• $Con:=\{X\in {𝒫}_f(T)\mid X\text{ is consistent}\}$
• $X⊢a\text{ iff }X⊢a\text{ 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 {𝒫}_f(T)\mid X\text{ has an upper bound}\}$
• $X⊢d\text{ iff }d⊑⨆X.$

Let $ℐ$ 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,⊢)$, we can build a Scott domain as follows.

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

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

• $𝒟(ℐ(D))\cong 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)