Scott-continuous maps and least fixed points

TheoremScott continuity into a function space is checked pointwise#✓fully proved

Let \(\alpha\), \(\beta\), \(\gamma\) be ω-complete partial orders, and let \(g\) be a map from \(\alpha\) to the ω-complete partial order of Scott-continuous maps \(\beta \to \gamma\), ordered pointwise. If for every \(b \in \beta\) the map \(a \mapsto g(a)(b)\) is Scott-continuous, then \(g\) is Scott-continuous. Here a map is Scott-continuous when it is monotone and preserves suprema of ω-chains.

theorem ωScottContinuous_of_apply {g : α → β →𝒄 γ}
    (h : ∀ b, ωScottContinuous fun a => g a b) : ωScottContinuous g

Used by 1

Used byCurrying of Scott-continuous maps

DefinitionCurrying of Scott-continuous maps#✓fully proved

Let \(\alpha\), \(\beta\), \(\gamma\) be ω-complete partial orders and let \(f : \alpha \times \beta \to \gamma\) be a Scott-continuous map, that is, a map that is monotone and preserves suprema of ω-chains. Its currying is the Scott-continuous map from \(\alpha\) to the ω-complete partial order of Scott-continuous maps \(\beta \to \gamma\), ordered pointwise, that sends \(a\) to the map \(b \mapsto f(a, b)\).

def curry (f : α × β →𝒄 γ) : α →𝒄 (β →𝒄 γ) :=
  ofFun (fun a => ofFun (fun b => f (a, b)))
    (ωScottContinuous_of_apply fun b => show ωScottContinuous (fun a => f (a, b)) by fun_prop)

Uses 1 · Used by 1

Statement usesScott continuity into a function space is checked pointwise

Used byDenotation of PCF terms

DefinitionLeast fixed point of a Scott-continuous map#✓fully proved

Let \(D\) be an ω-complete partial order with a least element \(\bot\), and let \(f : D \to D\) be Scott-continuous, that is, monotone and preserving suprema of ω-chains. The least fixed point \(\operatorname{lfp} f\) of \(f\) is the supremum of the Kleene chain \(\bot \le f(\bot) \le f(f(\bot)) \le \cdots\), whose \(n\)-th term is the \(n\)-fold iterate \(f^n(\bot)\).

def lfp (f : D →𝒄 D) : D := ωSup (fixedPoints.iterateChain f ⊥ bot_le)

Used by 10

Used byFundamental lemma of formal approximation · Fixed-point equation for the PCF denotation of fix · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · PCF denotation of a substituted term · The least fixed point is a fixed point · The least-fixed-point operator as a Scott-continuous map · The least fixed point lies below every prefixed point · Scott continuity of the least-fixed-point operator

TheoremThe least fixed point is a fixed point#✓fully proved

Let \(D\) be an ω-complete partial order with a least element \(\bot\), and let \(f : D \to D\) be Scott-continuous, that is, monotone and preserving suprema of ω-chains. Then the least fixed point \(\operatorname{lfp} f\) of \(f\) satisfies \(f(\operatorname{lfp} f) = \operatorname{lfp} f\).

theorem lfp_eq (f : D →𝒄 D) : f (lfp f) = lfp f

Uses 1 · Used by 3

Statement usesLeast fixed point of a Scott-continuous map

Used byFixed-point equation for the PCF denotation of fix · Plugging into a PCF context is monotone in the denotation · Scott continuity of the least-fixed-point operator

TheoremThe least fixed point lies below every prefixed point#✓fully proved

Let \(D\) be an ω-complete partial order with a least element \(\bot\), let \(f : D \to D\) be Scott-continuous, that is, monotone and preserving suprema of ω-chains, and let \(\operatorname{lfp} f\) be the supremum of the Kleene chain \(\bot \le f(\bot) \le f(f(\bot)) \le \cdots\). If \(a \in D\) satisfies \(f(a) \le a\), then \(\operatorname{lfp} f \le a\).

Together with \(f(\operatorname{lfp} f) = \operatorname{lfp} f\), this makes \(\operatorname{lfp} f\) the least fixed point of \(f\).

theorem lfp_le (f : D →𝒄 D) {a : D} (h : f a ≤ a) : lfp f ≤ a

Uses 1 · Used by 2

Statement usesLeast fixed point of a Scott-continuous map

Used byPlugging into a PCF context is monotone in the denotation · Scott continuity of the least-fixed-point operator

TheoremScott continuity of the least-fixed-point operator#✓fully proved

Let \(D\) be an ω-complete partial order with a least element \(\bot\). For a Scott-continuous map \(f : D \to D\), that is, one that is monotone and preserves suprema of ω-chains, let \(\operatorname{lfp} f\) be its least fixed point. The map \(f \mapsto \operatorname{lfp} f\), from the ω-complete partial order of Scott-continuous maps \(D \to D\), ordered pointwise, to \(D\), is Scott-continuous.

theorem lfp_ωScottContinuous : ωScottContinuous (lfp : (D →𝒄 D) → D)

Uses 3 · Used by 1

Statement usesLeast fixed point of a Scott-continuous map

Proof usesThe least fixed point is a fixed point · The least fixed point lies below every prefixed point

Used byThe least-fixed-point operator as a Scott-continuous map

DefinitionThe least-fixed-point operator as a Scott-continuous map#✓fully proved

Let \(D\) be an ω-complete partial order with a least element \(\bot\). The least-fixed-point operator, sending a Scott-continuous map \(f : D \to D\) to its least fixed point \(\operatorname{lfp} f\), bundled as a Scott-continuous map from the ω-complete partial order of Scott-continuous maps \(D \to D\), ordered pointwise, to \(D\).

def lfpHom : (D →𝒄 D) →𝒄 D := ofFun lfp lfp_ωScottContinuous

Uses 2 · Used by 1

Statement usesLeast fixed point of a Scott-continuous map · Scott continuity of the least-fixed-point operator

Used byDenotation of PCF terms

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.