13 The lattice basis on ΣN

13 The lattice basis on Σ^N

In the next section we shall show that the properties of ≺≺ listed in Section 11 are sufficient to reconstruct the object X and its basis. To do this, however, we need some more technical information about the lattice basis on Σ^N, and about the free distributive lattice on N.

Remark 13.1 When an object X has an N-indexed basis (βⁿ,A_n) there is an embedding X↣Σ^N, given by Lemma 7.4. This structure may be summed up by the diagram,

in which {|−|} means the singleton list, the map J on the right is defined by

Jφ ≡ λξ.∃ n.φ n∧ ξ n,

and Jφ preserves ∨, ⊥ and ∃. We define E from ≺≺ using the lattice basis (B^L,A_L) on Σ^N.

Remark 13.2 These results may be seen as presentation of the algebra Σ^X. In this, N is the set of generators and DL(N) is the free (imposed) distributive lattice on them, which we construct in Proposition 13.8 below. Then there are homomorphisms

as B⁽⁻⁾ takes the imposed list operations 0, 1, + and ⋆ to the intrinsic structure ⊥, ⊤, ∨ and ∧ in Σ^{Σ^N}, whilst Σⁱ preserves the latter in Σ^X. The relation ≺≺ encodes the system of “equations” that distinguishes the particular algebra Σ^X from the generic one Σ^{Σ^N} that is freely generated by N.

This explains why n≺≺ m does not imply n≼ m in our system, whereas α≪β implies α≤β in a continuous lattice. Topologically, we already saw the point in Remarks 1.8 and 6.15: many distinct codes may in principle represent the same open or compact subobject. To put this the other way round, since equality (or containment) of open subobjects is not computable, we cannot deduce equality (or comparison) of codes from semantic coincidence of subobjects.

Remark 13.3 The triangle

illustrates the comparison between the monad that captures the imposed (0,1,+,⋆) distributive lattice structure and the one in Axiom 3.3 based on Σ⁽⁻⁾⊣Σ⁽⁻⁾. The upward maps are the units of these monads. We leave the interested student to construct the multiplication map of the DL-monad as a list program, cf. flatten in Lemma 8.6.

We are not quite justified in saying that the Σ^Σ⁽⁻⁾ monad defines the intrinsic (⊥,⊤,∨,∧) distributive lattice structure. Corollary 10.3 said that the homomorphisms are the same, but I have not been able to show that every object whose intrinsic order is that of a distributive lattice is an algebra for the monad, i.e. of the form Σ^X for some object X.

Notation 13.4 Recall from Proposition 8.8 that the basis on Σ^N is

B^L ξ ≡ ∃ℓ∈ L.∀ m∈ℓ.ξ m and A_L Φ ≡ ∀ℓ∈ L.Φ(λ m.m∈ℓ),

from which we obtain the way-below relation

A_L B^R ≡ (R⊂^♯L) ≡ ∀ℓ∈ L.∃ℓ′∈ R.(ℓ′⊂ℓ).

The list of lists R+S is given by concatenation, whilst R⋆ S and B^{R⋆ S} were defined in Lemma 8.6.

Lemma 13.5 (B^L,A_L) is a lattice basis:

B¹=⊤ B₀=⊥ B^R⋆ S=B^R∧ B^S B^R+S=B^R∨ B^S

A₀ Φ⇔⊤ A_L⊥⇔(L=0) A_R+S=A_R∧A_S. ▫

Lemma 13.6 (B^L,A_L) is a filter basis: A⊤⇔⊤ and A_L(Φ∧ Ψ) ⇔ A_L Φ ∧ A_L Ψ.

Proof

A_L(Φ∧ Ψ)	⇔	∀ℓ∈ L.(Φ∧ Ψ)(λ m.m∈ℓ)
	⇔	∀ℓ∈ L.Φ(λ m.m∈ℓ)∧ Ψ(λ m.m∈ℓ)
	⇔	(∀ℓ∈ L.Φ(λ m.m∈ℓ)) ∧ (∀ℓ∈ L.Ψ(λ m.m∈ℓ))
	⇔	A_L Φ∧ A_L Ψ ▫

The Wilker condition says that we can split the list into the two parts that satisfy the respective disjuncts.

Lemma 13.7 A_L(Φ∨ Ψ) ⇔ ∃ L₁ L₂.(L=L₁+L₂) ∧ A_L₁ Φ ∧ A_L₂ Ψ. ▫

Proposition 13.8 We write L≅ R if both R⊂^♯L and L⊂^♯R. This is an open congruence for the imposed structure on Fin(Fin N), and the free imposed distributive lattice DL(N) is its quotient (Section C 10). ▫

Remark 13.9 So far we have not used any of the structure on N itself. Since we have a lattice basis for X, by definition

β⁽⁻⁾: N → Σ^X

takes the imposed structure (0,1,+,⋆) on N to the intrinsic structure (⊥,⊤,∨,∧) on Σ^X. Associated with this imposed structure is an imposed order relation ≼, which β⁽⁻⁾ takes to ≤, but with respect to which the dual basis A₍₋₎ is contravariant.

Definition 13.10 We define ≼ from + and ⋆ as the least relation such that

0≼ n≼ n≼1 (k⋆ n)+(k⋆ m) ≼ k*(n+m)

and again we write n≅ m when both n≼ m and m≼ n.

Proposition 13.11 The relation ≅ is an open congruence on N whose quotient is an imposed distributive lattice. ▫

Notation 13.12 Returning to Fin(Fin N), L is regarded as a formal sum of products of elements of N (additive normal form). This may be “evaluated” by means of the operation

ev:Fin(Fin N)→ N.

This is defined for lists by a generalisation of Lemma 8.6. A similar construction works for Kuratowski-finite subsets instead, except that then N has actually to satisfy the equations for a distributive lattice up to equality, and not just up to ≅ (cf. Notation 4.9). The map

is the structure map of the distributive lattice, regarded as an algebra for the DL-monad.

Proposition 13.13 The map ev:Fin(Fin N)→ N is a homomorphism in the sense that ev 0=0 and ev 1=1 by construction, whilst

ev(R+S) ≅ (ev R) + (ev S) and ev(R⋆ S) ≅ (ev R) ⋆ (ev S).

Proof This is a standard piece of universal algebra, which again we leave as a student exercise. The + equation is proved by list induction, using associativity and commutativity of + up to ≅. The equation for ⋆ is more difficult, as we have to take apart the inner lists, and use distributivity. ▫

Lemma 13.14 A_L B^L ⇔ ⊤ but

A_L B^R ⇔ (R⊂^♯L)	⇔	∀ℓ∈ L.∃ℓ′∈ R.(ℓ′⊂ℓ)	⇒	(ev L≼ev R)
A_L(λξ.ξ n)	⇔	∀ℓ∈ L.n∈ℓ	⇒	(ev L≼ n)
A_L(λξ.ξ n∧ξ m)	⇔	∀ℓ∈ L.n∈ℓ∧ m∈ℓ	⇒	(ev L≼ n⋆ m)
A_L(λξ.ξ n∨ξ m)	⇔	∀ℓ∈ L.n∈ℓ∨ m∈ℓ	⇒	(ev L≼ n+m)

with equality in the cases L≡{|{|k|}|} and L≡ R.

Proof In the expansion of A_L B^R, the products in L are of longer strings than those in R. The other three results follow by putting R≡{|{|n|}|}, {|{|n,m|}|} and {|{|n|},{|m|}|}, ▫

Remark 13.15 The foregoing discussion of ≅ is the price that we pay for not requiring (N,0,1,+,⋆) to satisfy the equations for a distributive lattice in Remark 1.8. If, like [JS96], we had done so, we would have instead paid the same price to construct the basis for Σ^X. This is indexed by the free distributive lattice on N^op quâ ⋆-semilattice, i.e. with new joins but using the old ones as meets. What we have bought for this price is the flexibility of switching amongst various kinds of basis (Definition 6.6), when we needed or didn’t need them, throughout the paper.

The reason why it is unnecessary to form the quotient of N or Fin(Fin N) by the congruence ≅ is that we never deal with their elements up to equality. The things that matter are the rules

which are examples of Corollary 11.5. Indeed the relation ≼ itself is only needed to avoid the extra rules that relate + and ⋆ to ≺≺, which appear in [JS96, Lemma 7].