General area

Applied mathematics: the formulation and study of mathematical structures to model interesting or puzzling phenomena in a useful and/or enlightening way. Need not be ‘grand’. My particular eccentricity: constructive mathematics, that is implementable in principle.

Phenomena: master/slave  layering, call/return  levels of abstraction, instruction/results, stimulus/response, … angels/demons

Aspects related to well−foundedness. The limitation imposed on us by working in a given formal (mechanisable) system.

Trinity of coalgebras

dynamical systems A set and a function on it: (∃A : Set)A → A. transition systems A set and a function from it to (indexed)

families of its elements: (∃A : Set)A → \underbrace{(∃B : Set)B → A}_{F am(B)}.

Typical element, ϕ = (A, λa. (B(a), λb. c(a, b))). interactive systems A set and a function from it to families of

families of its elements:

(∃A : Set)A → \underbrace{(∃B : Set)B → \underbrace{(∃C : Set)C → A}_{F am(A)}}_{F am(F am(A))}.

Typical element, Φ = (A, λa. (B(a), λb. (C(a, b), λc. d(a, b, c)))).

Main structures

Duples (‘Ab’s)  \begin{matrix}A : Set, \\ b : (a : A) → A \end{matrix}
Triples (‘ABc’s)  \begin{matrix}A : Set, \\ B : (∀a : A) Set, \\ c : (∀a : A, b : B(a)) A \end{matrix}

Quadruples (‘ABCd’s) A : Set, B : (∀a : A) Set, C : (∀a : A, b : B(a)) Set, d : (∀a : A, b : B(a), c : C(a, b)) A

Notation: \begin{matrix}a′ & =^{Δ} b(a) , \\ a[b] & =^{Δ} c(a, b) , \\ a[b/c] & =^{Δ} d(a, b, c) \end{matrix}

Interactive system interpretation

a : A  a state
b : B(a)  an input legal (for user) in state a
c : C(a, b) an output legal (for machine) in response to b
a[b/c] : A the next state after interaction b, c.

[figure: b : B(a); a ↦ d(a, b, c); c : C(a, b)]

Rule set interpretation

a : A  a formula
b : B(a)  an inference (step) yielding a
c : C(a, b) the name of a sub−proof (premise) required by b
a[b/c] : A the formula to be proved by sub−proof c

…  c … d(a, b, c)  b a

Topological interpretation

a : A  a basic open neighbourhood
b : B(a)  index of a (basic) covering of neighbourhood a
c : C(a, b) index of an element of covering b
a[b/c] : A the neighbourhood indexed by c
Cov(a) = { { a[b/c] | c : C(a, b) } | b : B(a) }

With some other structure (‘stability’, etc), a presentation of a locale.

Inductive constructions

• W : (∀A : Set, B : (∀a : A) Set) Set

W = Σ_{a:A}W^{B(a)}

Per Martin−Löf. “Wellorderings”.

• T : (∀ A : Set, B : (∀a : A) Set, C : (∀a : A, b : B(a)) Set, d : (∀a : A, b : B(a), c : C(a, b)) A, a : A ) Set

T (a) = (∃b : B(a))(∀c : C(a, b)) T (a[b/c])

Dan Synek and Kent Petersson. “General trees”.

Two predicate transformers

∘(P (a : A) : Set) =^{Δ} λa. (∃b : B(a))(∀c : C(a, b)) P (a[b/c])
•(P (a : A) : Set) =^{Δ} λa. (∀b : B(a)) (∃c : C(a, b))P (a[b/c])

\begin{matrix}Bar & =^{Δ} & μP : & ^{∘}P ⊆ P \\ P os & =^{Δ} & νP : & P ⊆ ^{•}P \end{matrix}

Composition

Give ρ_{1}, ρ_{2}, define ρ_{1} ;_{∘} ρ_{2} such that (ρ_{1} ;_{∘} ρ_{2})^{∘} = ρ_{1}^{∘} ^{∘} ρ_{2}^{∘}

;_{∘} \{ \begin{matrix}B(a) & =^{Δ} \underbrace{(∃b : B_{1}(a))(∀c : C_{1}(a, b)) B_{2}(a[b/c]_{1})}_{ρ_{1}^{∘}(B_{2},a)} \\ C(a, (b, f)) & =^{Δ} (∃c : C_{1}(a, b))C_{2}(a[b/c]_{1}, f(c)) \\ a[(b, f)/(c_{1}, c_{2})] & =^{Δ} a[b/c_{1}]_{1}[f(c_{1})/c_{2}]_{2} \end{matrix}

Bar

Constructor: \frac{x : ^{∘}Bar(a)}{bar(x) : Bar(a)}

Recursor: BarRec : \begin{matrix}(∀ \begin{matrix}G : (∀a : A, x : Bar(a)) Set \\ g : \begin{matrix}(∀ \begin{matrix}a : A, b : B(a), \\ f : (∀c : C(a, b)) Bar(a[b/c]), \\ h : (∀c : C(a, b)) G(a[b/c], f(c))) \end{matrix} \\ ) G(a, bar(b, f)) \end{matrix} \\ a : A, x : Bar(a) \end{matrix} \\ ) G(a, x) \end{matrix}

Equation: ([G, g]) =^{Δ} BarRec(G, g)

([G, g])(a, bar(b, f)) = g(a, b, f, λc.([G, g])(a, f(c)))

Bar’

Constructor: \frac{x : ^{∘}Bar(a)}{bar(x) : Bar(a)}

Recursor:

BarRec : (∀ G : (∀a : A, x : Bar(a)) Set g : (∀ \begin{matrix}a : A, \\ (b, λc. (f(c), h(c))) : \begin{matrix}let & G′(a) =^{Δ} (∃t : Bar(a))G(a, t) \\ in & ^{∘}G′(a) \end{matrix} \end{matrix} ) G(a, bar(b, f)) a : A, x : Bar(a) ) G(a, x)

Equation: ([G, g]) =^{Δ} BarRec(G, g)

([G, g])(a, bar(b, f)) = g(a, b, f, λc.([G, g])(a, f(c)))

Pos

Coconstructor: \frac{x : P os(a)}{pos(x) : ^{•}P os(a)}

Corecursor:

MkP os : \begin{matrix}(∀ \begin{matrix}G : (∀a : A) Set, \\ f : (∀a : A, x : P os(a), b : B(a)) C(a, b), \\ g : (∀a : A, x : P os(a), b : B(a)) G(a[b/f(a, x, b)], \\ a : A, x : G(a) \end{matrix} \\ ) P os(a) \end{matrix}

Coequation: [(G, f, g)] =^{Δ} MkP os(G, f, g)

pos([(G, f, g)](a, x)) = λb. \begin{matrix}let & \begin{matrix}c = f(a, x, b) : C(a, b), \\ x′ = g(a, x, b) : G(a[b/c]) \end{matrix} \\ in & (c, [(G, f, g)](a[b/c], x′)) \end{matrix}

Pos’

Coconstructor: \frac{x : P os(a)}{pos(x) : ^{•}P os(a)}

Corecursor:

MkP os : \begin{matrix}(∀ \begin{matrix}G : (∀a : A) Set, \\ λa, x, b. (f(a, x, b), h(a, x, b)) : (∀a : A, x : G(a))^{•}G(a) \\ a : A, x : G(a) \end{matrix} \\ ) P os(a) \end{matrix}

Coequation: [(G, f, g)] =^{Δ} MkP os(G, f, g)

pos([(G, f, g)](a, x)) = λb. \begin{matrix}let & \begin{matrix}c = f(a, x, b) : C(a, b), \\ x′ = g(a, x, b) : G(a[b/c]) \end{matrix} \\ in & (c, [(G, f, g)](a[b/c], x′)) \end{matrix}

Trees in summer

B^{∗}(a : A) : Set

B^{∗}(a : A) = { leaf }

∪ \{ fork(b, f) | \begin{matrix}b : B(a), \\ f : (∀c : C(a, b)) B^{∗}(a[b/c]) \} \end{matrix}

C^{∗}(a : A, bt : B^{∗}(a)) : Set

C^{∗}(a, leaf)  = { nil }
C^{∗}(a, fork(b, f)) = \{ cons(c, cs) | \begin{matrix}c : C(a : A, b : B(a)) \\ cs : C^{∗}(a[b/c], f(c)) \} \end{matrix}

d^{∗}(a : A, bt : B^{∗}(a), cs : C^{∗}(a, bt)) : A

d^{∗}(a, leaf, nil) = a

d^{∗}(a, fork(b, f), cons(c, cs)) = d^{∗}(a[b/c], f(c), cs)

A strange kind of ‘dual’: ΣΠ ↦ ΠΣ

B_{∗}(a : A) : Set

B_{∗}(a : A) = { fael }

∪ \{ krof(f, g) | \begin{matrix}f : (∀b : B(a)) C(a, b), \\ g : (∀b : B(a)) B_{∗}(a[b/f(b)]) \} \end{matrix}

C_{∗}(a : A, ct : B_{∗}(a)) : Set

C_{∗}(a, fael)  = { lin }
C_{∗}(a, krof(f, g)) = \{ snoc(b, bs) | \begin{matrix}b : B(a) \\ bs : C_{∗}(a[b/f(b)], g(b)) \} \end{matrix}

d_{∗}(a : A, ct : B_{∗}(a), bs : C_{∗}(a, ct)) : A

d_{∗}(a, fael, lin)  = a
d_{∗}(a, krof(f, g), snoc(b, bs)) = d_{∗}(a[b/f(b)], g(b), bs)

What are these things?

• – bt : B^{∗}(a) is a prescription or program for the user to deal with (feed stimuli to) a machine. Eventually the user leafs, or drives machine into deadlock.

– cs : C^{∗}(a, b) is a trace of machine responses that leads to a state in which the user leafs. (Machine escapes deadlock.)

• – tb : B_{∗}(a) is a prescription or program for the machine to deal with (respond to stimuli from) a user. Eventually the machine faels, or drives user into deadlock.

– sc : C_{∗}(a, tb) is a trace of user commands that leads to a state where the machine faels. (User escapes deadlock.)

Two Relation transformers

•∘R(a_{v}, a) =^{Δ}

(∀b_{v} : B_{v}(a_{v})) \underbrace{(∃bt : B^{∗}(a_{v}))(∀cs : C^{∗}(a, bt))}_{Callbacks} \begin{matrix}(∃c_{v} : C_{v}(a_{v}, b_{v})) \\ R(a_{v}[b_{v}/c_{v}], a[bt/cs]^{∗}) \end{matrix}

Typical element: λb_{v}. (bt(b_{v}), λcs. (c_{v}(b_{v}, cs), r(b_{v}, cs)))

∘•R(a_{v}, a) =^{Δ}

(∃b_{v} : B_{v}(a_{v})) \underbrace{(∀bt : B^{∗}(a)) (∃cs : C^{∗}(a, bt))}_{Callbacks} \begin{matrix}(∀c_{v} : C_{v}(a_{v}, b_{v})) \\ R(a_{v}[b_{v}/c_{v}], a[bt/cs]^{∗}) \end{matrix}

Typical element: (b_{v}, λbt. (cs(bt), λc_{v}. r(bt, c_{v})))

What follows is detritus

20

What’s an triple?

A triple is a binary relation (directed graph) on A: • b : B(a) is a token of something’s relationship with a.

• c(a, b) : A is that thing (a[b]). Reflexive and transitive closure (free category on a graph): B^{∗}(a : A) : Set

B^{∗}(a) = { nil } ∪ { cons(b, bt) | b : B(a), bt : B^{∗}(c(a, b)) }

c^{∗}(a : A, b : B^{∗}(a)) : A

\begin{aligned}c^{∗}(a, nil) & = & a \\ c^{∗}(a, cons(b, bt)) & = & c^{∗}(c(a, b), bt) \end{aligned}

In what sense is ^{∗} a closure operation?

Triples. Form reflexive and transitive closure using nil : B(a) and cons(b : B(a), bs : B^{∗}(a[b])) : B^{∗}(a). Then define concatenation

(bs : B^{∗}(a)) ⌢ (bs′ : B^{∗}(a[bs]^{∗})) : B^{∗}(a)

by induction on bs. This is (like) a monoid (multiplication).

Quadruples. Form … closure using given leaf : B^{∗}(a), and fork(b : B(a), f : (∀c : C(a, b)) B^{∗}(a[b/c])) : B^{∗}(a). Then define tree−forest composition

(bt : B^{∗}(a)) ⋆ (f : (∀cs : C^{∗}(a, bt)) B^{∗}(a[bt/cs]^{∗})) : B^{∗}(a)

by induction on bt. This is (like) a monad (bind).

What’s a morphism?

\begin{aligned}α & : & A & ⟶ & A′ \\ β(a : A) & : & B(a) & ⟶ & B′(α(a)) \\ γ(a : A, b : B(a)) & : & C(a, b) & ⟵ & C′(α(a), β(a, b)) \end{aligned}

α(a[b/γ(a, b, c′)]) = α(a)[β(a, b)/c′]

Triples and quadruples are coalgebras

F am(X : Type) =^{Δ} (∃I : Set)I → X : Type

Typical element: (I, λi. x(i))

T r =^{Δ} (∃A : Set)S → \underbrace{(∃B : Set)B → A}_{F am(A)}
=^{Δ} (∃A : Set)A → F am(A)

Typical element: (A, λa. (B(a), λb. c(a, b)))

Qu =^{Δ} (∃S : Set)S → F am(F am(S))
=^{Δ} (∃A : Set)A → (∃B : Set)B → (∃C : Set)C → A

Typical element: (A, λa. (B(a), λb. (C(a, b), λc. a[b/c])))