16  Morphisms as matrices

The analogy between bases for topology and bases for linear algebra in Section 6 can also be applied to morphisms. In this section we identify the abstract conditions satisfied by the relation

that was used in Definitions 1.6 and 2.3. Like ≺≺, this is a binary relation between the two overt discrete objects of codes.

As this condition is an observable property of the function, it determines an open subobject of the set of functions X→ Y, and such properties form a sub-basis of the compact–open topology. If X is locally compact then this object is the exponential Y^X in both traditional topology and locale theory, and the conditions below are those listed in [Joh82, Lemma VII 4.11]. Unfortunately, there need not be a corresponding dual basis of compact subobjects to make Y^X locally compact.

In our notation, the relation f Kⁿ⊂ U^m is A_n(Σ^fβ^m). Clearly this question can easily be generalised to A_n(Hβ^m), in which we replace f by the “second class” map H (Notation 5.13).

Notation 16.1 Let (βⁿ,A_n) and (γ^m,D_m) be ∨-bases for objects X and Y respectively. Then any first or second class morphism H:X−× Y in HS (that is, H:Σ^Y→Σ^X in S) has a matrix,

which generalises the representation of y:Y via Hψ≡ψ x as ξ≡ i y≡λ y.γ^m y in Lemmas 15.2ff.

Lemma 16.2 H is recovered from H_n^m as Hψ=∃ m n.D_mψ∧H_n^m∧βⁿ.

Proof    

Lemma 16.3 The matrix is directed in n, cf. Lemma 11.3:

Proof    These are A₀φ⇔⊤ and A_n+pφ⇔ A_nφ∧ A_pφ with φ=Hγ^m. They hold because (βⁿ,A_n) is an ∨-basis (Definition 6.6(a)).         ▫

Lemma 16.4 The matrix is monotone in m, cf. Lemma 11.6:

Proof    A_n≤ A_n′ (though we already had this from directedness) and γ^m≤γ^m′.         ▫

Lemma 16.5 The matrix is rounded, respecting ≺≺ on both sides, cf. Lemmas 11.7 & 15.2:

Proof    

Lemma 16.6 Suppose n,m:N⊢ρ(n,m):Σ satisfies the foregoing properties, i.e. 

ρ(0,k)

and define H:X−× Y by Hψ ≡ ∃ m n.D_mψ∧ρ(n,m)∧βⁿ. Then ρ(n,m) ⇔ A_n(Hγ^m).

Proof    Since ρ respects ≺≺ on the right,

Then, since ρ also respects ≺≺ on the left and A_n preserves the join, which is directed because ρ respects 0 and +,

Lemma 16.7 id_n^m  ⇔  A_n(idβ^m)  ⇔  (n≺≺ m)  ⇔  E_n^m.

Proof    The relationship with E follows from Lemma 14.5. The unit laws were given by Lemma 16.5, cf. the Karoubi completion, which splits idempotents in any category.         ▫

Lemma 16.8 K· H_n^k ⇔ ∃ m.K_m^k∧H_n^m.

Proof    

although ⇐ is actually ⇔ as we have an ∨-basis. (We draw attention to this because [I] uses the natural ∧-basis on ℝ, and therefore the weaker result about composition.)         ▫

Theorem 16.9 HS (Notation 5.13) is equivalent to the category whose

1. objects are abstract bases (N,0,1,+,⋆,≺≺) (Definition 14.1);
2. morphisms are ρ(n,m) satisfying the conditions in Lemma 16.6;
3. identity is ≺≺;
4. composition is relational.         ▫

The definition of HS in [A] was essentially taken from Hayo Thielecke’s work on “computational effects” [Thi97], which was in turn based on the Kleisli category for the monad. It was therefore motivated by more syntactic considerations than ours. From a semantic point of view, it would have been more natural to have split the idempotents. In the classical models, the category would then be the opposite of that of all continuous (but not necessarily distributive) lattices and Scott-continuous maps (cf. Example 2). In this result, we would drop the ≺≺+ and ≺≺⋆ rules from Definition 14.1 of an abstract basis.

In order to characterise first class maps, by Corollary 10.3 we have to consider preservation of the lattice connectives, cf. Lemmas 15.3ff. For this, the target object Y must have a lattice basis.

Lemma 16.10 H⊤=⊤ iff H_n¹⇔(n≺≺ 1), and H⊥=⊥ iff H_n⁰⇔(n≺≺ 0).

Proof    If H⊤=⊤ then H_n¹≡ A_n(Hγ¹)≡ A_n(H⊤) ⇔ A_n⊤ ≡ A_nβ¹≡(n≺≺1) by Notation 16.1, Definition 6.6, and Notation 11.1.

Conversely, H⊤≡ Hγ¹≡∃ n.H_n¹∧βⁿ ⇔ ∃ n.A_n⊤∧βⁿ≡ ⊤ by Definition 6.6, Lemma 16.5 and Definition 6.2.

We may substitute ⊥ and 0 for ⊤ and 1 in the same argument.         ▫

Similarly we are able on this occasion to handle ∧ and ∨ simultaneously (Remark 4.15).

Lemma 16.11 H(φ⊙ψ)=Hφ⊙ Hψ iff H_n^{s⊙ t} ⇔ ∃ m p.H_m^s∧H_p^t∧ (n≺≺ m⊙ p), both when ⊙ is ∧ or ⋆ and when it is ∨ or +.

Proof    If H(φ⊙ψ)=Hφ⊙ Hψ then

Conversely, using distributivity,

Definition 16.12 An abstract matrix is a binary relation H_n^m such that

H

0m

Theorem 16.13 S is equivalent to the category whose

1. objects are abstract lattice bases (N,0,1,+,⋆,≺≺);
2. morphisms are abstract matrices;
3. identity is ≺≺;
4. composition is relational.         ▫

Jung and Sünderhauf characterised continuous functions between stably locally compact spaces in a similar way [JS96].

Remark 16.14 We shall speculate on the possible computational applications of matrices for continuous functions in the next section, but let’s say something here about the analogy with linear algebra that we have used. Really, this has been much more useful that we had any right to expect, since neither S nor HS (the “first” and “second class” maps) is a symmetric monoidal closed category.

However, by Theorem 9.11, stably locally compact objects and the A:X−× Y for which A preserves ⊤ and ∧ do define such a category. In fact, they provide a model of linear logic with involutive negation and an “of course” operator given by the Smyth powerdomain ℘^♯ (Example 12.13):

Proposition 16.15 Let X be a stably locally compact space. The HS-maps A:Γ−× X for which A:Σ^X→Σ^Γ preserves ⊤ and ∧ correspond bijectively and naturally to S-maps Γ→℘^♯X.

Proof    Both correspond to terms Γ⊢ξ≡λ n.Aβⁿ:Σ^N that are rounded filters (∧-homomorphisms) for ≺≺_X or ideals for ≻≻_X.         ▫

Since they also preserve directed joins, such A are known as preframe homomorphisms; for more on their relationship to the Smyth powerdomain, see [Vic88, 11.2.5] and [JKM01]. For a similar investigation of join-preserving maps and the Hoare or lower powerdomain ℘^♭X in ASD, presumably we would first need to identify the “stably locally overt” objects to which the analogous construction may be applied.