# Alfred's Fixed Points
## A bit of formal order theory using Clojure and the LaTTe proof assistant

Frederic Peschanski - LIP6 - Sorbonne Université

This document is copyright (C) 2019 Frederic Peschanski - Creative Commons [CC-BY-SA 4.0](https://creativecommons.org/licenses/by-sa/4.0/)
# Introduction
A **fixed point** of a function $f$ is simply a point $x$ such that $f(x)=x$.
A function may have many, one or zero fixed point(s).
All the points in the domain of an *identity* function are fixed points, i.e. for any $x$,$f(x)=x$. In Clojure the `identity` function has thus *all* fixed points:
```clojure id=845a5f4e-20b3-483e-9da4-bada9ddc6d19
(identity 42) ; a simple (and fundamental) fixed point
```
```clojure id=229ece38-e63b-42f7-87e3-3284f608411b
(identity {:firstname "Alfred"
:lastname "Tarksi"
:born 1901}) ; a more complex fixed point
```
The unary minus function on integers has only one fixed point : the equation $-x=x$ is only true when $x$ is $0$.
And the `inc` (increment) function on integers has no fixed point at all, there is no $x$ such that $x=x+1$.
We might wonder whether finding fixed point of function, or at least proving their existence using a so-called fixed point theorem would be useful. In fact, this question is central in (abstract) mathematics, which makes [fixed point theory](https://fixedpointtheoryandapplications.springeropen.com/) an important branch of study with dedicated journals ([this one](https://fixedpointtheoryandapplications.springeropen.com) and [this one](http://jfpt.scik.org/) at least) and [conferences](https://waset.org/fixed-point-theory-conference-in-may-2020-in-sydney).
Quoting [this page](https://fixedpointtheoryandapplications.springeropen.com/): *The existence of a fixed point is therefore of paramount importance in several areas of mathematics and other sciences*
In computer science, fixed point theorems are used in various areas, e.g. when reasoning about programs or verifying properties (e.g. by abstract interpretation or model checking), also in game theory (e.g. Nash equilibrium *is* a fixed point theorem).
One elementary albeit pervasively useful fixed point theorem is the famous **Knaster–Tarski theorem**. The statement of this theorem on [Wikipedia](https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem) is as follows:
*Let L be a [complete lattice](https://en.wikipedia.org/wiki/Complete_lattice) and let f : L → L be an [order-preserving function](https://en.wikipedia.org/wiki/Order-preserving_function). Then the [set](https://en.wikipedia.org/wiki/Set_(mathematics)) of [fixed points](https://en.wikipedia.org/wiki/Fixed_point_(mathematics)) of f in L is also a complete lattice.*
This is a very short but also very dense formulation !
A little bit below in the article, we can read :
*Since complete lattices cannot be [empty](https://en.wikipedia.org/wiki/Empty_set) (they must contain supremum of empty set), the theorem in particular guarantees the existence of at least one fixed point of f, and even the existence of a least (or greatest) fixed point. In many practical cases, this is the most important implication of the theorem.*
In this notebook our objective is to *dissect* this particular implication of the theorem, and establish (almost) all the foundations so that it can be stated formally (albeit less concisely). Ultimately, our goal is to obtain a formal proof of the theorem, mechanized in the LaTTe proof assistant... and of course in a *reproducible* *way* thanks to nextjournal!
**Intended audience**
* you should be familiar with functional programming languages, possibly with Clojure (but in fact we will not write *classical* Clojure code)
* an illustration of what you can do using a proof assistant such as LaTTe, and perhaps the feeling that it's not so remote from "normal" mathematics
* a glimpse of the Lisp superpowers (Clojure inside !)
If you're curious about how this is done "inside", then the following talk might prove useful : [Live Coding Mathematic Your First Clojure Proof (Euroclojure 2016)](https://youtu.be/5YTCY7wm0Nw)
(note that LaTTe evolved a little bit since the talk)
# Basic order theory in LaTTe
LaTTe is a proof assistant developed in the realm of the Clojure programming environment. It is better to know a little bit of Clojure to completely grasp what's following, but the formal statements we make are often not so far from "classical" mathematics (in Lisp forms) so this is not even a strong requirement.
We rely on a few libraries, especially [latte-prelude](https://github.com/latte-central/latte-prelude) (the basic library with propositions, quantifiers, etc.) and [latte-sets](https://github.com/latte-central/latte-sets) (typed set theory).
```clojure id=edef5d95-e18a-4060-8220-499f2357c8fa
(ns fixed-points.alfred-fixpoints
(:refer-clojure :exclude [and or not set =])
(:require [clojure.repl :refer [source doc]]
[latte.core
:as latte
:refer [definition defthm deflemma
proof assume have pose qed
type-of forall]]
[latte-sets.core :as sets :refer [set elem set-equal forall-in]]
[latte-sets.rel :as rel :refer [rel]]
[latte-prelude.equal :as eq :refer [equal]]
[latte-prelude.prop :as p :refer [not and and* or]]
[latte-prelude.quant :as q :refer [exists]]))
```
In the [latte-sets.rel](https://latte-central.github.io/latte-sets/latte-sets.rel.html) namespace is defined the notion of a **relation**.
```clojure id=953d507f-93cc-4933-94a2-b3197f95e59c
(source rel)
```
For given types `T` and `U`, the type `(rel T U)` means a relation between type `T` and type `U`. In classical set theory, this would be a set of pairs in the Cartesian product$T \times U$ but in type theory it's in fact a more like a "function" of two arguments. If `R` is a relation of type `(rel T U)`, in order to express that `x` of type `T` and `y` of type `U` are related in `R`, we simply write `(R x y)`. If they are *not* related, then we would simply write `(not (R x y))` instead. Personally, I find these more "natural" than e.g. $(x,y)\in R$ or $(x,y)\notin R$.
## Ordering relations
In order theory we are interested in **ordering relations** (or simply *orders*), which are *endo* relations (between a type `T` and itself) satisfying three properties.
First, an ordering relation must be **reflexive**. In day to day mathematics we would write: $\forall x\in T,~(x,x)\in R$ or $x~R~x$ but in LaTTe it's defined as follows.
```clojure id=4dbefa7e-35d5-4399-bf4e-d5aa39fea9e1
(definition reflexive
[?T :type, R (rel T T)]
(forall [x T] (R x x)))
```
The question mark in `?T :type` means that `T` is an *implicit type parameter*. To state the reflexivity property, we do not want to write `(reflexive T R)` (for a relation `R` of type `(rel T T)`) but simply `(reflexive R)`. The support of such implicit type parameters is a recent addition to LaTTe, maybe not 100% finalized but we will take advantage of it to avoid a lot of boilerplate code.
The second property is that of **transitivity**, which is stated as follows:
```clojure id=64e4a46f-dc20-4ed8-9ba1-58e74bdf9e5b
(definition transitive
[?T :type, R (rel T T)]
(forall [x y z T]
(==> (R x y)
(R y z)
(R x z))))
```
In the traditional notation, we would write$\forall x,y,z \in T. x~R~y \land y~R~z \implies x~R~z$
In type theory, an implication `(==> H1 H2 ... Hn G)` must be understood as the statement that from the hypotheses `H1`, `H2`, ..., `Hn` we can deduce the `G`(oal).
The final property of an ordering relation is that of **antisymmetry**.
```clojure id=1ea7a426-7a24-4134-88d5-8cd41b0f6bf5
(definition antisymmetric
[?T :type, R (rel T T)]
(forall [x y T]
(==> (R x y)
(R y x)
(equal x y))))
```
Ultimately here is the definition of an ordering relation :
```clojure id=3a554fd2-3c4b-42ce-a6fb-639989bd57bb
(definition order
[?T :type, R (rel T T)]
(and* (reflexive R)
(transitive R)
(antisymmetric R)))
```
## The identity relation
In all the article we will mostly remain in the abstract, so we will not take example of specific relations (e.g. involving natural numbers). However one basic relation can be demonstrated an ordering : the **identity relation** on type `T`.
```clojure id=b06757c2-e684-4af6-bf59-e43e40039e12
(definition ridentity
[T :type]
(lambda [x T] (lambda [y T] (equal x y))))
```
We can check that `(ridentity T)` is a relation.
```clojure id=15a3e8fb-7a76-4fee-b717-1442f91cac88
(type-of [T :type]
(ridentity T))
```
The returned type is `(==> T T ✳)` which is the same as `(==> T T :type)` and thus `(rel T T)`.
Let's first demonstrate, as a lemma, that `(ridentity T)` is reflexive.
```clojure id=f1194b86-62c8-49a2-bb0c-e78bfd9fb56e
(defthm rid-refl
[T :type]
(reflexive (ridentity T)))
```
```clojure id=c8591439-a584-4d82-beed-7934b759cf6a
(proof 'rid-refl
"First, we take an arbitrary `x` o type `T`."
(assume [x T]
"A basic fact is that `x` is equal to itself."
(have (equal x x) :by (eq/eq-refl x))
"Said differently, `x` is related to itself in the identity..."
(have ** ((ridentity T) x x) :by ****))
"Given our assumption that `x` is arbitray, we reached our goal."
(qed ****))
```
Since it's our first proof in LaTTe in this document (which is not a LaTTe tutorial), let's add some comment. First, beyond the lispy syntax this formal proof is not so far from a "standard" mathematical proof. To "demonstrate" this, let's translate it removing all LaTTe-specific comments, writing the identity relation as $rid_T$.
**Proof** of Theorem `rid-refl`
First we take an arbitrary $x$ of type `T`. A basic fact (step `****` in the LaTTe proof) is that `x` is equal to itself, which is by reflexivity of equality (i.e. $\forall x\in T,~x=x$). Said differently (step `****` in the proof), `x` is related to itself in the identity, i.e. $x~rid_T~x$. Given our assumption that $x$ is arbitrary, we reached our goal (QED).
There is a certain distance between an informal (textbook-like) mathematical proof and what we have to write in LaTTe. But this distance is often not as huge as we might think. This is because we can introduce abstractions and proof methods, which is exactly what we are doing in this document, in the realm of order theory.
From now on, we will not "translate" the proofs and only rely on LaTTe to explain things, rather than the conventional and highly informal mathematical notation.
Let's now prove that the identity relation is transitive.
```clojure id=8fca69b5-2314-4d77-9763-8dbb68836bab
(defthm rid-trans
[T :type]
(transitive (ridentity T)))
```
```clojure id=cb246b57-4d93-49ec-908e-314f03077ba5
(proof 'rid-trans
"First we make a local definition."
(pose R := (ridentity T))
"Now we make the assumptions of `transitive`."
(assume [x T y T z T
Hxy (R x y)
Hyz (R y z)]
"We have to prove that `x` and `z` are also related in `R`."
"We first relate our assumptions to equality."
(have **** (equal x y) :by Hxy)
(have **** (equal y z) :by Hyz)
"And by transitivity of equality we obtain the following:"
(have (equal x z) :by (eq/eq-trans **** ****))
"Which can be restated as follows:"
(have (R x z) :by ))
"Since `x`, `y` and `z` were taken arbitrarily, we reach our goal."
(qed ))
```
And finally antisymmetry.
```clojure id=11211e8e-e47f-4ea6-8e06-c0747c864447
(deflemma rid-antisym
[T :type]
(antisymmetric (ridentity T)))
```
The proof is trivial.
```clojure id=e6ca90ce-8fa2-440d-a1d2-69ea549d0d1c
(proof 'rid-antisym
(pose R := (ridentity T))
(assume [x T y T
Hxy (R x y)
Hyx (R y x)]
(have **** (equal x y) :by Hxy))
(qed ))
```
Hence identity is an ordering relation.
```clojure id=3d52fd0f-c1d1-4418-8d58-a9fc82d9dea9
(defthm rid-order
[T :type]
(order (ridentity T)))
```
```clojure id=270d9621-104b-46fc-97a3-e90493235b8c
(proof 'rid-order
(qed (p/and-intro* (rid-refl T)
(rid-trans T)
(rid-antisym T))))
```
## The inverse relation
For any relation $R$ an inverse relation $R^{-1}$ is such that $x~R~y$ iff $y~R^{-1}~x$. In LaTTe this can be defined as follows:
```clojure id=f1b46312-dbc9-4a88-ab2b-c3b79be582c7
(definition rinverse
[?T :type, R (rel T T)]
(lambda [x T] (lambda [y T] (R y x))))
```
Many results about an ordering relation can be propagated, by a so-called *principle of duality*, to its inverse (and *vice versa*). This is an important source of what are called *free theorems*.
One important fact is that the inverse of an ordering relation is itself an ordering relation.
```clojure id=3195912e-5347-493a-8e21-20b6449c8b1e
(defthm rinv-order
[?T :type, R (rel T T)]
(==> (order R)
(order (rinverse R))))
```
The proof is a little bit long because we need to handle the three properties of orders individually, but it's not difficult at all (and it could be decomposed in lemmas as we did previously, but it would not really help readability here).
```clojure id=f43fed4e-5dda-4e40-9804-fefd6adb127b
(proof 'rinv-order-thm
(pose iR != (rinverse R))
(assume [HR (order R)]
"First part: reflexivity"
(have (reflexive R) :by (p/and-elim* 1 HR))
"This is the same as the following."
(have iR-refl (reflexive iR) :by )
"Second part: transitivity"
(have R-trans (transitive R) :by (p/and-elim* 2 HR))
"The assumptions for transitivity of `iR`."
(assume [x T y T z T
Hxy (iR x y)
Hyz (iR y z)]
"The two hypotheses can be rewritten in terms of `R`."
(have (R y x) :by Hxy)
(have (R z y) :by Hyz)
"And we can exploit the fact that `R` is transitive."
(have (R z x) :by (R-trans z y x ))
"Which is the same as the following:"
(have (iR x z) :by ))
(have iR-trans (transitive iR) :by )
"Third part: antisymmetry"
(have R-anti (antisymmetric R) :by (p/and-elim* 3 HR))
"Under the assumptions for antisymmetry of `iR`."
(assume [x T y T
Hxy (iR x y)
Hyx (iR y x)]
"We simply exploit the fact that e.g. `(iR x y)` is `(R y x)`."
(have **~~ (equal x y) :by (R-anti x y Hyx Hxy)))
(have iR-anti (antisymmetric iR) :by ~~~~)
"Thus the inverse is an ordering relation."
(have iR-order (order iR) :by (p/and-intro* iR-refl iR-trans iR-anti)))
(qed iR-order))
```
# Bounds
Now that we now what is an ordering relation, we can begin to discuss supplementary properties can be associated with it.
## Lower and upper bounds
Among important extra properties of ordering relations, **lower and upper bounds** play a fundamental role.
```clojure id=e807b676-f720-4f90-8914-1d2b77319c20
(definition lower-bound
"`l` is a lower bound for `X` in the ordering relation `R`."
[?T :type, R (rel T T), S (set T), l T]
(forall-in [e S] (R l e)))
```
In informal mathematics we would write something like $\forall e\in S,~l~R~e$. Note that the notion is defined for an arbitrary (*endo*) relation, not prescriptively an ordering one. The upper bound is symmetric.
```clojure id=07a4f9c7-c57c-4673-a380-b43680c35218
(definition upper-bound
"`u` is an upper bound for set `S` in the ordering relation `R`."
[?T :type, R (rel T T), S (set T), u T]
(forall-in [e S] (R e u)))
```
The two notions are of course dual, as illustrated by the following theorem.
```clojure id=2af61192-a432-4dfb-906d-95f2cd2245d4
(defthm low-up-dual
[?T :type, R (rel T T), S (set T), x T]
(==> (lower-bound R S x)
(upper-bound (rinverse R) S x)))
```
```clojure id=49d9ad26-f949-4e02-ae89-af7228d8fecc
(proof 'low-up-dual-thm
(pose iR := (rinverse R))
"The hypothesis is that `x` is a lower bound."
(assume [Hlow (lower-bound R S x)]
"Now we take an arbitrary element `e` of the set `S`."
(assume [e T
He (elem e S)]
"By hypothesis `x` is lower than `e` in `R`."
(have ~~~~ (R x e) :by (Hlow e He))
"Hence it is greated in `iR`."
(have ~~** (iR e x) :by ****))
"And we're done."
(have up (upper-bound iR S x) :by ****))
(qed up))
```
**Exercise** : prove similarly the theorem `up-low-dual` that states exactly the converse, that an upper bound in `R` is a lower bound in its inverse.
## Least and greatest elements
Lower and upper bounds of a given set may (and are often) not be elements of this set. If on the contrary they were, we would need the stronger notions of **least and greatest elements**.
```clojure id=94a463cd-230d-46f4-ad49-fc084d8e9995
(definition least-element
[?T :type, R (rel T T), S (set T), l T]
(and (elem l S)
(lower-bound R S l)))
```
```clojure id=a2a1a89e-24d5-44ed-b6d2-845060c7973b
(definition greatest-element
[?T :type, R (rel T T), S (set T), u T]
(and (elem u S)
(upper-bound R S u)))
```
**Exercise** : define and prove a theorem stating that the least and greatest elements are dual notions.
## Greatest lower bound (glb) and Least upper bound (lub)
Some ordering relations admit special bounds :
* the **greatest lower bound** (nicknamed **glb**), which is the greatest among all possible lower bounds
* the **least upper bound** (nicknamed **lub**), which is the least among all possible upper bounds
The LaTTe definitions follow.
```clojure id=477b61be-9d41-4125-a947-6ba9776959d7
(definition glb
"The greatest lower bound `l` of a subset `S` relation `R`."
[?T :type, R (rel T T), S (set T), l T]
(and (lower-bound R S l)
(forall [x T]
(==> (lower-bound R S x)
(R x l)))))
```
```clojure id=be60f997-4b4f-4bdb-b53d-429b03556aae
(definition lub
"The least upper bound `u` of a subset `S` in relation `R`."
[?T :type, R (rel T T), S (set T), u T]
(and (upper-bound R S u)
(forall [x T]
(==> (upper-bound R S x)
(R u x)))))
```
Of course, the two notions are dual.
```clojure id=0991272e-322b-4b7e-ad96-8dc9f564021d
(defthm glb-lub-dual
[?T :type, R (rel T T)]
(forall [S (set T)]
(forall [l T]
(==> (glb R S l)
(lub (rinverse R) S l)))))
```
```clojure id=650b9647-4d71-4f09-b696-024b870d677d
(proof 'glb-lub-dual-thm
(pose iR := (rinverse R))
"First let's state the main hypotheses."
(assume [S (set T)
l T
Hl (glb R S l)]
"From now on the inverse will be noted `R'`."
"A `glb` is a lower bound..."
(have (lower-bound R S l) :by (p/and-elim-left Hl))
"... and thus is is an upper bound for the inverse,
which is the least part of the [[lub]] conjunction we need."
(have **** (upper-bound iR S l) :by ((low-up-dual R S l) ))
"Now let's assume we have `u` an upper bound in `R'`."
(assume [u T
Hu (upper-bound iR S u)]
"We trivially have that `l` is lower than `u` in `iR'`
(since it is greater in `R`)."
(have **** (iR l u) :by ((p/and-elim-right Hl) u Hu)))
"Thus we have the right part of the [[lub]] conjunction."
(have _ :by (p/and-intro **** ****)))
"Hence we can conclude"
(qed ))
```
**Exercise** : prove similarly the theorem `lub-glb-dual` that states exactly the converse, that a least upper bound in `R` is a greatest lower bound in its inverse.
An important property of the lub and the glb is that, if they exist in a relation `R`, then they are unique. First let's see how LaTTe defines the notion of uniqueness:
```clojure id=c158fdd0-92d4-4beb-a453-a4976314f75f
(source q/unique)
```
This means uniqueness is *existence* of some element (of type `T`) satisfying some property P `(ex P)` and *"singleness"* `(single P)`. Let's begin with the latter:
```clojure id=2453c35e-e912-4ef2-b833-e8e6143f8a5a
(source q/single)
```
So for the greatest lower bound we want to prove the following :
```clojure id=b4098ff2-9a48-4263-8bf7-d1d662280c2e
(deflemma glb-single
"Singleness of greateast lower bounds."
[?T :type, R (rel T T), X (set T)]
(==> (antisymmetric R)
(q/single (lambda [l T] (glb R X l)))))
```
Note that our only assumption is that the relation is antisymmetric, we do not need all the other ordering properties (reflexivity, transitivity).
```clojure id=857778fe-4417-440c-8554-00a8c4ee6b39
(proof 'glb-single-lemma
(pose P := (lambda [l T] (glb R X l)))
"These are all our assumptions:"
(assume [Hanti (antisymmetric R)
l1 T, l2 T
H1 (P l1) H2 (P l2)]
"We much show that l1 is equal to l2."
"First, these are two lower bounds for `R`."
(have **** (lower-bound R X l1) :by (p/and-elim-left H1))
(have **** (lower-bound R X l2) :by (p/and-elim-left H2))
"Now let's apply the *greatest* constraints."
"First, `l1` is greater than `l2`."
(have (R l2 l1) :by ((p/and-elim-right H1) l2 ****))
"Second, `l2` is greater than `l1`."
(have (R l1 l2) :by ((p/and-elim-right H2) l1 ****))
"Thus, by antisymmetry (our hypothesis `H`) `l1` and `l2` must be equal."
(have (equal l1 l2) :by (Hanti l1 l2 )))
"And this is enough to conclude"
(qed ))
```
We may thus conclude our theorem since
```clojure id=a703d0be-f2ad-4930-9a45-d9205336dd0a
(defthm glb-unique
"Unicity of greatest lower bounds."
[?T :type, R (rel T T), X (set T)]
(==> (antisymmetric R)
(exists [l T] (glb R X l))
(q/unique (lambda [l T] (glb R X l)))))
```
```clojure id=bda3860e-b323-4b4e-9b87-26348132dce7
(proof 'glb-unique-thm
(assume [Hanti _, Hex _]
(have _ :by (p/and-intro Hex ((glb-single R X) Hanti))))
(qed ))
```
**Exercise** : state and prove a similar theorem `lub-unique` for least upper bound. Use the direct approach as above first. Then propose an alternative proof exploiting duality.
# Complete Lattices
The **complete lattices** are particularly well-behaved ordering relation wrt. the least upper and greatest lower bounds. They are defined by the fact that all their subsets have `glb`'s and `lub`'s. However, as we'll see, it is enough to have "only" `glb`'s or `lub`'s for the definition to hold. Because the least fixed points are somewhat more common in practice we take the `glb` road (but this is somewhat an arbitrary choice, as we will make clear later on).
```clojure id=b3fceec9-5986-43c7-a167-1f62b7a601e4
(definition complete-lattice
"The definition of a relation `R` on `T` being a complete lattice."
[?T :type, R (rel T T)]
(and (order R)
(forall [X (set T)]
(exists [l T] (glb R X l)))))
```
To emphasis the fact the choosing glb's instead of lub's in the definition is vacuous, we state the following property :
```clojure id=310302f5-a1fa-49d7-8bcb-02bd0a61b612
(defthm all-glb-all-lub
[?T :type, R (rel T T)]
(==> (antisymmetric R)
(forall [X (set T)]
(exists [l T] (glb R X l)))
(forall [X (set T)]
(exists [u T] (lub R X u)))))
```
This says that if an antisymmetric relation has all `glb'`s then is also has all` lub`'s. The proof is a little bit more technical, but there is no trick we only have to dig into the definitions.
```clojure id=e52f8cde-66d4-4175-b5b5-65d20d0ccacd
(proof 'all-glb-all-lub-thm
"First we introduce our two assumptions."
(assume [H1 _ H2 _]
"Now let's assume an arbitrary set `X`."
(assume [X (set T)]
"We define `Y` the set of upper bounds of `X`."
(pose Y := (lambda [u T] (upper-bound R X u)))
"By hypothesis there is a unique greatest lower bound for `Y`."
(have (exists [l T] (glb R Y l)) :by (H2 Y))
(have glbY-unique _ :by ((glb-unique R Y) H1 ))
"Let's call this `glbY`."
(pose glbY := (q/the (lambda [l T] (glb R Y l)) glbY-unique))
"And we keep the fact that it is indeed *the* greatest lower bound."
(have **** (glb R Y glbY) :by (q/the-prop (lambda [l T] (glb R Y l)) glbY-unique))
"Our objective now is to show that `glbY` is *also* an upper bound for the set `X`."
"For this we assume an arbitrary element `x` of the set `X`."
(assume [x T
Hx (elem x X)]
"In the first step we'll show that `x` is a lower bound for `Y`."
(assume [y T
Hy (elem y Y)]
(have (upper-bound R X y) :by Hy)
(have (R x y) :by ( x Hx)))
(have (lower-bound R Y x) :by )
"Hence since `glbY` is *greatest* we can show that `(R x glbY)`."
(have (forall [z T]
(==> (lower-bound R Y z)
(R z glbY))) :by (p/and-elim-right ****))
(have (==> (lower-bound R Y x)
(R x glbY)) :by ( x))
(have (R x glbY) :by ( )))
"Thus `glbY` is an upper bound for `X`."
(have (upper-bound R X glbY) :by )
"The second step consists in showing that `glbY` is the *least* upper bound."
(assume [x T
Hx (upper-bound R X x)]
"Taking an arbitrary upper bound `x`, we can show `(R glbY x)` since
as a `glbY` is a lower bound for `Y` and the assumed `x` is by hypothesis a member of `Y`. "
(have (elem x Y) :by Hx)
(have (lower-bound R Y glbY) :by (p/and-elim-left ****))
(have (R glbY x) :by ( x )))
(have (forall [x T]
(==> (upper-bound R X x)
(R glbY x))) :by )
"Hence we have our main result which is that `glbY` is a `lub` for `X`."
(have (lub R X glbY) :by (p/and-intro ))
"Hence we've just shown that there exists a lub for `X`, namely `glbY`."
(have (exists [l T] (lub R X l))
:by ((q/ex-intro (lambda [l T] (lub R X l)) glbY) ))))
(qed ))
```
Let's try an alternative definition for complete lattices.
```clojure id=2ac7b269-f779-445b-9af1-75eb5f6565cf
(definition complete-lattice-alt
[?T :type, R (rel T T)]
(and (order R)
(forall [X (set T)]
(exists [l T] (lub R X l)))))
```
And thanks to the `all-glb-all-lub` theorem we have the following :
```clojure id=52cb6485-d989-48fa-b809-ac28726f9017
(defthm complete-lattice-glb-lub
[?T :type, R (rel T T)]
(==> (complete-lattice R)
(complete-lattice-alt R)))
```
And the proof is trivial.
```clojure id=6fd18f7d-9e21-4f74-8f8b-bfd345e7d896
(proof 'complete-lattice-glb-lub-thm
(assume [H _]
"Let's dig out the antisymmetric property"
(have **** (antisymmetric R)
:by (p/and-elim* 3 (p/and-elim-left H)))
"As well as the *all glb's* property"
(pose glb-prop := (p/and-elim-right H))
(have **** (forall [X (set T)]
(exists [l T] (lub R X l)))
:by ((all-glb-all-lub R) **** glb-prop))
"and we're done"
(have (complete-lattice-alt R)
:by (p/and-intro (p/and-elim-left H) ****)))
(qed ))
```
**Exercise** : prove the converse, i.e. that `(complete-lattice-alt R)` implies `(complete-lattice R)`. This can be done by exploiting duality.
**Exercise** : prove that if R is a complete lattice, then (rinverse R) is also a complete lattice.
# Monotonic functions
A (total) function from a domain `T` to a codomain `U` can be represented in LaTTe as a value of type `(==> T U)`. In order theory, most functions of concerns are *endo functions* of type `(==> T T)`, and given an ordering relation `R` (with elements in `T`) the important requirement is how such a function behaves wrt. `R`. The most interesting property one can expect from such a function is that of *monotonicity*. The definition of a **monotonic function** is as follows:
```clojure id=a536539a-0e2e-47c2-aae4-cc5af1de26d3
(definition monotonic
"The endo function `f` on `T` is monotonic wrt. `R`."
[?T :type, R (rel T T), f (==> T T)]
(forall [x y T]
(==> (R x y) (R (f x) (f y)))))
```
A monotonic (or *monotone*) function is thus a function that "respects" a given ordering, it is said *order-preserving*. As an example if we take the real numbers, then addition is monotonous. Suppose the function $f_K(x) = x + K $ then $\forall x,y \in \mathbb{R},~x \leq y \implies f_K(x) \leq f_K(y)$. The function $g(x)=x^2$ is however non-monotonous (e.g. $-2 \leq 1$ but $g(-2)=4 \nleq 1=g(1)$).
To familiarize a little bit with the definition, let's prove the following theorem.
```clojure id=1f9b705a-7007-474c-9a94-a258147a96cb
(defthm inv-monotonic
[?T :type, R (rel T T), f (==> T T)]
(==> (monotonic R f)
(monotonic (rinverse R) f)))
```
The proof is left uncommented, given its simplicity.
```clojure id=e5002408-dca9-44d5-a76b-c40942bccf89
(proof 'inv-monotonic-thm
(pose R' := (rinverse R))
(assume [H (monotonic R f)]
(assume [x T
y T
H' (R' x y)]
(have **** (R y x) :by H')
(have **** (R (f y) (f x)) :by ((H y x) ****))
(have (R' (f x) (f y)) :by ****))
(have (monotonic R' f) :by ))
(qed ))
```
# Fixed points
We are not far from being able to state Alfred's fixed point theorem.
The final building block of the definition is that of a **fixed point**.
```clojure id=9c7ec112-f60a-49c1-8ed9-ee4c42aaa4d5
(definition fixed-point
"A fixed point `x` of an endo function `f` on `T`."
[?T :type, f (==> T T), x T]
(equal x (f x)))
```
There are derived notions of *pre-and-post fixed points*.
```clojure id=ca7fde66-0525-4e3e-bb66-56ec893a5c53
(definition pre-fixed-point
[?T :type, R (rel T T), f (==> T T), x T]
(R x (f x)))
```
```clojure id=8d4e44c7-27f6-4bc8-80a9-343b9e08ef4d
(definition post-fixed-point
[?T :type, R (rel T T), f (==> T T), x T]
(R (f x) x))
```
Or course, if an element `x` is both a pre and a post fixed point, then it is indeed a fixed point (by antisymmetry).
```clojure id=925764de-f7c1-42d6-b359-6a55f7c6202a
(defthm pre-post-fixed-point
[?T :type, R (rel T T), f (==> T T), x T]
(==> (antisymmetric R)
(pre-fixed-point R f x)
(post-fixed-point R f x)
(fixed-point f x)))
```
```clojure id=3aeaaa53-ca96-4fda-aaff-2eb40c560287
(proof 'pre-post-fixed-point-thm
(assume [H1 (antisymmetric R)
H2 (pre-fixed-point R f x)
H3 (post-fixed-point R f x)]
(have **** (fixed-point f x)
:by (H1 x (f x) H2 H3)))
(qed ))
```
Also, a fixed point is by definition also a post fixed point, which we state as follows:
```clojure id=acc4da8f-bd9a-4283-b910-786fa3c58d18
(defthm fixed-point-post
[?T :type, R (rel T T), f (==> T T), x T]
(==> (reflexive R)
(fixed-point f x)
(post-fixed-point R f x)))
```
The proof is straightforward.
```clojure id=05669fe3-c9ac-40d6-8014-fa5cd804196a
(proof 'fixed-point-post-thm
(pose P := (lambda [y T] (R y x)))
(assume [H1 (reflexive R)
H2 (fixed-point f x)]
"Reflexivity means `(R x x)` hence `(P x)`."
(have (P x) :by (H1 x))
"Since `(equal x (f x))` we can substitute in `(P x)` we just obtained."
(have **** (P (f x)) :by (eq/eq-subst P H2 ****)))
"And we're done"
(qed ****))
```
**Exercise** : show that a fixed point is also a pre fixed point.
# The least fixed point theorem
We are now at the core of Alfred's fixed point theorem. A function can have zero, one or many fixed points. In the latter case, similarly to bounds, we would like to know if some fixed points is *less than* (resp. *greater than*) all the other ones. The notion of a **least fixed point** is defined as follows:
```clojure id=127b5fce-d7b9-4e94-9ec4-7b7dfd9a19cd
(definition lfp
"The least fixed point of a function `f` wrt. a relation `R`."
[?T :type, R (rel T T), f (==> T T), mu T]
(and (fixed-point f mu)
(forall [y T]
(==> (fixed-point f y)
(R mu y)))))
```
So a least fixed point is an element `mu` such that `(fixed-point f mu)`, and moreover for any other fixed point `(fixed-point f y)` then `mu` is less than `y` in `R`, i.e. `(R mu y)`.
Now we can state the core result of the least fixed point theorem.
```clojure id=dbd484e2-b1c5-4fce-af89-ad5610a06549
(defthm lfp-theorem
"The least fixed-point theorem."
[?T :type, R (rel T T), f (==> T T)]
(==> (complete-lattice R)
(monotonic R f)
(q/unique (lambda [mu T] (lfp R f mu)))))
```
The theorem states that given a complete lattice `R` and a monotonic function `f`, then there exists a unique least fixed point `mu` of `f` in `R`. To demonstrate this theorem we have to proceed in two steps.
* first we have to show the existence of a least fixed point `mu`.
This is stated as follows:
```clojure id=90897c9c-48d3-4a16-bfe4-3f1998bd9dc4
(deflemma lfp-ex
"The least fixed-point theorem, existential part."
[?T :type, R (rel T T), f (==> T T)]
(==> (complete-lattice R)
(monotonic R f)
(exists [mu T] (lfp R f mu))))
```
This is the most tricky part of the demonstration, and this is where much of the "mathematical creativity" is required... There's some artistic beauty in the proof that follows.
```clojure id=fbd4ed1d-1845-40fb-a2c6-2e786844352a
(proof 'lfp-ex-lemma
(assume [H1 _ H2 _]
"We first define the set of post-fixed points of `F`.
This is in fact where most of the creativity of the proof
is concentrated. The artistic creativity is all here!"
(pose Y := (lambda [y T] (post-fixed-point R f y)))
"This set has a glb since `R` is a complete lattice."
(have glbY-ex (exists [l T] (glb R Y l))
:by ((p/and-elim-right H1) Y))
(pose glbY-unique := ((glb-unique R Y)
(p/and-elim-right (p/and-elim-left H1))
glbY-ex))
"We name it `glbY`."
(pose glbY := (q/the (lambda [l T] (glb R Y l)) glbY-unique))
"And we recall the main property."
(have **** (glb R Y glbY)
:by (q/the-prop (lambda [l T] (glb R Y l)) glbY-unique))
"In the first part we will show that `glbY` is a fixed point of `f`."
"For this, we take an arbitrary elment `y` of `Y`
(hence an arbitrary post-fixed point)."
(assume [y T
Hy (elem y Y)]
"It is greater than a lower bound, e.g. `glbY`."
(have (R glbY y) :by ((p/and-elim-left ) y Hy))
"And thus by monotonicity:"
(have (R (f glbY) (f y)) :by (H2 glbY y ))
"And it is also a post-fixed point, hence :"
(have (R (f y) y) :by Hy)
"Now, by transitivity:"
(have (R (f glbY) y) :by
((p/and-elim-right (p/and-elim-left (p/and-elim-left H1)))
(f glbY) (f y) y ))
"Thus `(f glbY)` is a lower bound of `Y`.")
(have **** (lower-bound R Y (f glbY)) :by )
"Moreover, because `glbY` is a greatest lower bound."
(have (R (f glbY) glbY) :by ((p/and-elim-right ****) (f glbY) ****))
"And since `f` is monotonous."
(have (R (f (f glbY)) (f glbY)) :by (H2 (f glbY) glbY ))
(have (elem (f glbY) Y) :by )
"Now `glbY` is still a lower bound, thus:"
(have (R glbY (f glbY)) :by ((p/and-elim-left ****) (f glbY) ))
"Thus `glbY` is a fixed point of `f`, since it is both a pre and a post-fixed point."
(have (fixed-point f glbY)
:by ((pre-post-fixed-point R f glbY)
(p/and-elim-right (p/and-elim-left H1))
))
"For the second part, we need to show that `glbY` is the *least* fixed point."
(assume [z T
Hz (fixed-point f z)]
"A fixed point `z` is also a post-fixed point."
(have (post-fixed-point R f z)
:by ((fixed-point-post R f z)
(p/and-elim* 1 (p/and-elim-left H1))
Hz))
"Hence `z` is a member of the set `Y`..."
(have (elem z Y) :by )
"... which `glbY` (our fixed point) is a (greatest) lower bound, hence the following:"
(have (R glbY z) :by ((p/and-elim-left ) z )))
"hence we have the *least* property."
(have (forall [z T]
(==> (fixed-point f z)
(R glbY z))) :by )
"Now we obtained the `lfp` property for `glbY`."
(have (lfp R f glbY)
:by (p/and-intro ))
"Which leads to the existential conclusion."
(have _ :by ((q/ex-intro (lambda [mu T] (lfp R f mu)) glbY) )))
(qed ))
```
**Remark** : this proof is a little bit "CPU intensive". One way to largely accelerate the process would be to decompose it in a few auxiliary lemmas. Alternatively, we may wait for a future optimized version of the LaTTe kernel.
* The second part is to show *"singleness"*, i.e. that two least fixed points are unavoidably *"the same"*.
```clojure id=e924ce6d-79a4-4b02-9e32-aa96de760ae8
(deflemma lfp-single
[?T :type, R (rel T T), f (==> T T)]
(==> (antisymmetric R)
(q/single (lambda [mu T] (lfp R f mu)))))
```
Note that the only property we need is that of antisymmetry.
Unlike the previous one, this proof doesn't require much creativity. We just have to follow the definition.
```clojure id=b8663102-5580-4f8a-bdb9-84e08bc6b98c
(proof 'lfp-single-lemma
(assume [H (antisymmetric R)]
"We consider two least fixed point `mu1` and `mu2`."
(assume [mu1 T
mu2 T
Hmu1 (lfp R f mu1)
Hmu2 (lfp R f mu2)]
"They are by definition of `lfp` interrelated in `R`."
(have (R mu1 mu2) :by ((p/and-elim-right Hmu1) mu2 (p/and-elim-left Hmu2)))
(have **** (R mu2 mu1) :by ((p/and-elim-right Hmu2) mu1 (p/and-elim-left Hmu1)))
"Hence by antisymmetry they are equal."
(have (equal mu1 mu2) :by (H mu1 mu2 **** ****))))
(qed ))
```
Hence we have a complete proof for the least fixed point theorem.
```clojure id=1f396c3a-e2af-4591-a948-998893719d4b
(proof 'lfp-theorem-thm
(assume [H1 _ H2 _]
(have **** _ :by (p/and-intro
;; existence
((lfp-ex R f) H1 H2)
;; unicity
((lfp-single R f) (p/and-elim* 3 (p/and-elim-left H1))))))
(qed ))
```
**Exercise** : state prove the dual *greatest fixed point theorem* stated below.
```clojure id=4b1cd0e4-5f27-49ba-beb4-0a416fbb3f18
(definition gfp
"The greatest fixed point of a function `f` wrt. a relation `R`."
[?T :type, R (rel T T), f (==> T T), nu T]
(and (fixed-point f nu)
(forall [y T]
(==> (fixed-point f y)
(R y nu)))))
```
```clojure id=95daf70d-036e-40dc-a61e-f819ab8a42e6
(defthm gfp-theorem
"The greatest fixed-point theorem."
[?T :type, R (rel T T), f (==> T T)]
(==> (complete-lattice R)
(monotonic R f)
(q/unique (lambda [nu T] (gfp R f nu)))))
```
**Hint** : The simplest, shortest and most interesting way to demonstrate this theorem is to exploit the duality of the notion.
# Conclusion
We started with an informal mathematical statement, which can be (re)formulated as follows :
Given a complete lattice `R` and a function f monotonic on `R`, then `f` has a least fixed point `mu` in `R`. The exercises (if done correctly) should lead to the dual fact that `f` also has a greatest fixed point `nu` in `R`.
In this (next)article, we defined formally all the involved notions using the LaTTe proof assistant. This comprises:
* the notion of a **complete lattice**, cf. `complete-lattice`
* the notion of a **monotonic**, or order-preserving function, cf. `monotonic`
* the notion of a **fixed point**, cf. `fixed-point`
These, in turn, require a few other definitions : ordering relations, least upper bounds, etc.
Our assessment of this little exercise is first that order theory can be fully formalized, and with some care the abstraction level of the involved definitions, statements and proofs *almost* matches the classical practice of *pencil&paper mathematics*.
Last but not least, the presentation of formal mathematical developments as nextjournal articles appear to the author as *optimal*: this really is [Live Coding (abstract) Mathematics](https://www.youtube.com/watch?v=5YTCY7wm0Nw)!
**
## This notebook was exported from https://nextjournal.com/a/LegmU4hjhHwdfwbWXdSLR?change-id=CkdpwUUcasfvVc5TzBzqYe

```edn nextjournal-metadata
{:article
{:settings {:subtitle? true, :authors? true, :numbered? true},
:nodes
{"05669fe3-c9ac-40d6-8014-fa5cd804196a"
{:compute-ref #uuid "47b2913a-84e8-465d-8b47-9dc63edcc6a8",
:exec-duration 51,
:id "05669fe3-c9ac-40d6-8014-fa5cd804196a",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"07a4f9c7-c57c-4673-a380-b43680c35218"
{:compute-ref #uuid "3854cf91-6ed1-4ba5-8ab8-fa8618f5ce12",
:exec-duration 161,
:id "07a4f9c7-c57c-4673-a380-b43680c35218",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"0991272e-322b-4b7e-ad96-8dc9f564021d"
{:compute-ref #uuid "2acadd7b-38f1-4611-a469-f729f20a4e11",
:exec-duration 150,
:id "0991272e-322b-4b7e-ad96-8dc9f564021d",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"11211e8e-e47f-4ea6-8e06-c0747c864447"
{:compute-ref #uuid "a8b59bb6-60eb-4605-a860-f280956342f0",
:exec-duration 47,
:id "11211e8e-e47f-4ea6-8e06-c0747c864447",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"127b5fce-d7b9-4e94-9ec4-7b7dfd9a19cd"
{:compute-ref #uuid "5240574e-84c2-420a-a702-46c2fd8a07d6",
:exec-duration 66,
:id "127b5fce-d7b9-4e94-9ec4-7b7dfd9a19cd",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"15a3e8fb-7a76-4fee-b717-1442f91cac88"
{:compute-ref #uuid "8a42b9df-c6ba-4f06-9692-c62213b07518",
:exec-duration 54,
:id "15a3e8fb-7a76-4fee-b717-1442f91cac88",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"1ea7a426-7a24-4134-88d5-8cd41b0f6bf5"
{:compute-ref #uuid "cdbe3b47-3917-4990-afe8-35eeb98f7119",
:exec-duration 193,
:id "1ea7a426-7a24-4134-88d5-8cd41b0f6bf5",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"1f396c3a-e2af-4591-a948-998893719d4b"
{:compute-ref #uuid "607e64d2-cdcc-4691-b348-f659012dcf9a",
:exec-duration 832,
:id "1f396c3a-e2af-4591-a948-998893719d4b",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"1f9b705a-7007-474c-9a94-a258147a96cb"
{:compute-ref #uuid "cbcad4a9-e1c9-40ce-b049-1ea20bf02fe7",
:exec-duration 123,
:id "1f9b705a-7007-474c-9a94-a258147a96cb",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"229ece38-e63b-42f7-87e3-3284f608411b"
{:compute-ref #uuid "4f29431e-5312-4ec2-b85b-88335b781ebd",
:exec-duration 67,
:id "229ece38-e63b-42f7-87e3-3284f608411b",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"2453c35e-e912-4ef2-b833-e8e6143f8a5a"
{:compute-ref #uuid "1c817fc6-fa66-4305-8a08-c0c5e42db6e8",
:exec-duration 528,
:id "2453c35e-e912-4ef2-b833-e8e6143f8a5a",
:kind "code",
:output-log-lines {:stdout 7},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"270d9621-104b-46fc-97a3-e90493235b8c"
{:compute-ref #uuid "0e9e22c3-264e-402f-8129-27dac6c7adc7",
:exec-duration 119,
:id "270d9621-104b-46fc-97a3-e90493235b8c",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"2ac7b269-f779-445b-9af1-75eb5f6565cf"
{:compute-ref #uuid "451d096f-3f64-40e7-a01b-5e5d314dc61b",
:exec-duration 106,
:id "2ac7b269-f779-445b-9af1-75eb5f6565cf",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"2af61192-a432-4dfb-906d-95f2cd2245d4"
{:compute-ref #uuid "bec8523e-20d6-4e56-8f1b-f65e28b0adcf",
:exec-duration 122,
:id "2af61192-a432-4dfb-906d-95f2cd2245d4",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"310302f5-a1fa-49d7-8bcb-02bd0a61b612"
{:compute-ref #uuid "ac289d0a-033f-48f5-9cf3-b16e762e83bb",
:exec-duration 172,
:id "310302f5-a1fa-49d7-8bcb-02bd0a61b612",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"3195912e-5347-493a-8e21-20b6449c8b1e"
{:compute-ref #uuid "ac351ff1-adb8-4a3a-8d72-685328adcd40",
:exec-duration 78,
:id "3195912e-5347-493a-8e21-20b6449c8b1e",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"3a554fd2-3c4b-42ce-a6fb-639989bd57bb"
{:compute-ref #uuid "5fc619cb-3aee-4122-bd8f-2e52b5db1a56",
:exec-duration 162,
:id "3a554fd2-3c4b-42ce-a6fb-639989bd57bb",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"3a85690b-683a-4fd9-9821-8b902ce0a2ff"
{:environment
[:environment
{:article/nextjournal.id
#uuid "02be3b0e-091b-40f2-b9b8-a05b08da9d06",
:change/nextjournal.id
#uuid "5d8e16f7-d074-41a2-9a19-28a22da6ac26",
:node/id "c0a6243c-909e-45be-adc6-d6330fbb59d2"}],
:id "3a85690b-683a-4fd9-9821-8b902ce0a2ff",
:kind "runtime",
:language "clojure",
:type :nextjournal},
"3aeaaa53-ca96-4fda-aaff-2eb40c560287"
{:compute-ref #uuid "8520f00d-0427-4fb6-b1f5-328c1ac9af84",
:exec-duration 47,
:id "3aeaaa53-ca96-4fda-aaff-2eb40c560287",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"3d52fd0f-c1d1-4418-8d58-a9fc82d9dea9"
{:compute-ref #uuid "2227c688-30fe-4bb3-ad70-dcbb2ccd686b",
:exec-duration 69,
:id "3d52fd0f-c1d1-4418-8d58-a9fc82d9dea9",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"477b61be-9d41-4125-a947-6ba9776959d7"
{:compute-ref #uuid "cfcf0d0f-d962-4f72-b546-dca7c155a7b2",
:exec-duration 199,
:id "477b61be-9d41-4125-a947-6ba9776959d7",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"49d9ad26-f949-4e02-ae89-af7228d8fecc"
{:compute-ref #uuid "dfefba03-1832-4272-8579-25e4028f3f53",
:exec-duration 85,
:id "49d9ad26-f949-4e02-ae89-af7228d8fecc",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"4b1cd0e4-5f27-49ba-beb4-0a416fbb3f18"
{:compute-ref #uuid "0a00ec98-56bc-4dc4-9431-a147c3e7e02d",
:exec-duration 73,
:id "4b1cd0e4-5f27-49ba-beb4-0a416fbb3f18",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"4dbefa7e-35d5-4399-bf4e-d5aa39fea9e1"
{:compute-ref #uuid "99d994af-84d7-48ea-b59d-b70315506f8a",
:exec-duration 83,
:id "4dbefa7e-35d5-4399-bf4e-d5aa39fea9e1",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"52cb6485-d989-48fa-b809-ac28726f9017"
{:compute-ref #uuid "ce3d5e27-8e94-4082-b738-9d9820205169",
:exec-duration 88,
:id "52cb6485-d989-48fa-b809-ac28726f9017",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"64e4a46f-dc20-4ed8-9ba1-58e74bdf9e5b"
{:compute-ref #uuid "1b36a0c6-2fad-47fa-8eed-7e21603b7214",
:exec-duration 114,
:id "64e4a46f-dc20-4ed8-9ba1-58e74bdf9e5b",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"650b9647-4d71-4f09-b696-024b870d677d"
{:compute-ref #uuid "9d0ea58e-0e31-4a84-b4d9-8a98df8491a2",
:exec-duration 349,
:id "650b9647-4d71-4f09-b696-024b870d677d",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"6fd18f7d-9e21-4f74-8f8b-bfd345e7d896"
{:compute-ref #uuid "23103aec-31d1-44a2-9c3d-7f3be95f9a9f",
:exec-duration 396,
:id "6fd18f7d-9e21-4f74-8f8b-bfd345e7d896",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"845a5f4e-20b3-483e-9da4-bada9ddc6d19"
{:compute-ref #uuid "2e24881a-bfb0-406e-9328-ebcb7419c904",
:exec-duration 60,
:id "845a5f4e-20b3-483e-9da4-bada9ddc6d19",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"857778fe-4417-440c-8554-00a8c4ee6b39"
{:compute-ref #uuid "5e768a1d-a707-4775-9c54-8e9f940e3f37",
:exec-duration 243,
:id "857778fe-4417-440c-8554-00a8c4ee6b39",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"8d4e44c7-27f6-4bc8-80a9-343b9e08ef4d"
{:compute-ref #uuid "41c6ac33-9984-479d-b545-d4e50c112cfa",
:exec-duration 54,
:id "8d4e44c7-27f6-4bc8-80a9-343b9e08ef4d",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"8fca69b5-2314-4d77-9763-8dbb68836bab"
{:compute-ref #uuid "55055d7e-3ba0-4618-8e55-dd86a25d6fbd",
:exec-duration 48,
:id "8fca69b5-2314-4d77-9763-8dbb68836bab",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"90897c9c-48d3-4a16-bfe4-3f1998bd9dc4"
{:compute-ref #uuid "388d0913-5319-4984-bab6-07641a54f8d9",
:exec-duration 96,
:id "90897c9c-48d3-4a16-bfe4-3f1998bd9dc4",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"925764de-f7c1-42d6-b359-6a55f7c6202a"
{:compute-ref #uuid "9dc06e59-39b8-4a8a-a0de-136f46923182",
:exec-duration 98,
:id "925764de-f7c1-42d6-b359-6a55f7c6202a",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"94a463cd-230d-46f4-ad49-fc084d8e9995"
{:compute-ref #uuid "c3981d26-2a66-47d6-8e1d-4bdd0b365df6",
:exec-duration 163,
:id "94a463cd-230d-46f4-ad49-fc084d8e9995",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"953d507f-93cc-4933-94a2-b3197f95e59c"
{:compute-ref #uuid "43e88ebc-ce9c-408b-84d5-b102d5bae8d1",
:exec-duration 692,
:id "953d507f-93cc-4933-94a2-b3197f95e59c",
:kind "code",
:output-log-lines {:stdout 4},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"95daf70d-036e-40dc-a61e-f819ab8a42e6"
{:compute-ref #uuid "e4920ced-a4a6-43e9-b6f9-5312ad324150",
:exec-duration 81,
:id "95daf70d-036e-40dc-a61e-f819ab8a42e6",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"9c7ec112-f60a-49c1-8ed9-ee4c42aaa4d5"
{:compute-ref #uuid "45fd1b1e-8693-410b-9c8d-2c812e5d47be",
:exec-duration 70,
:id "9c7ec112-f60a-49c1-8ed9-ee4c42aaa4d5",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"a2a1a89e-24d5-44ed-b6d2-845060c7973b"
{:compute-ref #uuid "3e4ffab9-1d5f-4444-a701-1ab1d6769da8",
:exec-duration 159,
:id "a2a1a89e-24d5-44ed-b6d2-845060c7973b",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"a536539a-0e2e-47c2-aae4-cc5af1de26d3"
{:compute-ref #uuid "82491518-853f-48cb-9792-72b30be74e7d",
:exec-duration 126,
:id "a536539a-0e2e-47c2-aae4-cc5af1de26d3",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"a703d0be-f2ad-4930-9a45-d9205336dd0a"
{:compute-ref #uuid "4606ef2e-2a6d-4dda-8a72-eb37d43f3ca6",
:exec-duration 128,
:id "a703d0be-f2ad-4930-9a45-d9205336dd0a",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"acc4da8f-bd9a-4283-b910-786fa3c58d18"
{:compute-ref #uuid "5e1381ba-a1c6-43f9-998e-13f38624e314",
:exec-duration 51,
:id "acc4da8f-bd9a-4283-b910-786fa3c58d18",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"b06757c2-e684-4af6-bf59-e43e40039e12"
{:compute-ref #uuid "98c083c3-bcd4-4ed8-8be5-5f431036f2ee",
:exec-duration 47,
:id "b06757c2-e684-4af6-bf59-e43e40039e12",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"b3fceec9-5986-43c7-a167-1f62b7a601e4"
{:compute-ref #uuid "5703a6c4-552e-4c59-a367-98c1044a0b72",
:exec-duration 145,
:id "b3fceec9-5986-43c7-a167-1f62b7a601e4",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"b4098ff2-9a48-4263-8bf7-d1d662280c2e"
{:compute-ref #uuid "c1c73e3d-a30f-42e4-8b55-dd7ae2b0bd92",
:exec-duration 59,
:id "b4098ff2-9a48-4263-8bf7-d1d662280c2e",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"b8663102-5580-4f8a-bdb9-84e08bc6b98c"
{:compute-ref #uuid "b108f3f2-b109-4f2e-9979-d7be8d994723",
:exec-duration 143,
:id "b8663102-5580-4f8a-bdb9-84e08bc6b98c",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"bda3860e-b323-4b4e-9b87-26348132dce7"
{:compute-ref #uuid "657e42d1-67a3-4c4d-b978-7763e9639af6",
:exec-duration 400,
:id "bda3860e-b323-4b4e-9b87-26348132dce7",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"be60f997-4b4f-4bdb-b53d-429b03556aae"
{:compute-ref #uuid "56a6f527-6dbe-4711-ab58-e143d6e87354",
:exec-duration 124,
:id "be60f997-4b4f-4bdb-b53d-429b03556aae",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"c158fdd0-92d4-4beb-a453-a4976314f75f"
{:compute-ref #uuid "3ab7d4a9-e0ea-4223-9a18-dcaef1d1b0a0",
:exec-duration 469,
:id "c158fdd0-92d4-4beb-a453-a4976314f75f",
:kind "code",
:output-log-lines {:stdout 5},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"c8591439-a584-4d82-beed-7934b759cf6a"
{:compute-ref #uuid "e845c99d-8017-41a5-88ba-d83dad40ab3f",
:exec-duration 90,
:id "c8591439-a584-4d82-beed-7934b759cf6a",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"ca7fde66-0525-4e3e-bb66-56ec893a5c53"
{:compute-ref #uuid "b3ee777c-7c59-4f2c-8119-59f1e2f18c21",
:exec-duration 48,
:id "ca7fde66-0525-4e3e-bb66-56ec893a5c53",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"cb246b57-4d93-49ec-908e-314f03077ba5"
{:compute-ref #uuid "fe213951-5700-4ae4-a5cf-904d6907fec0",
:exec-duration 136,
:id "cb246b57-4d93-49ec-908e-314f03077ba5",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"dbd484e2-b1c5-4fce-af89-ad5610a06549"
{:compute-ref #uuid "5a368dbc-6ea3-4c52-b462-a920f5b2e9f2",
:exec-duration 156,
:id "dbd484e2-b1c5-4fce-af89-ad5610a06549",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"e5002408-dca9-44d5-a76b-c40942bccf89"
{:compute-ref #uuid "b496ab90-be12-4561-a242-351598bc9c1d",
:exec-duration 121,
:id "e5002408-dca9-44d5-a76b-c40942bccf89",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"e52f8cde-66d4-4175-b5b5-65d20d0ccacd"
{:compute-ref #uuid "7dd1ff42-17d5-4f72-adf5-10a401488b84",
:exec-duration 2157,
:id "e52f8cde-66d4-4175-b5b5-65d20d0ccacd",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"e6ca90ce-8fa2-440d-a1d2-69ea549d0d1c"
{:compute-ref #uuid "a37235ff-e3a6-4057-ab8d-221fcf0a16e0",
:exec-duration 49,
:id "e6ca90ce-8fa2-440d-a1d2-69ea549d0d1c",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"e807b676-f720-4f90-8914-1d2b77319c20"
{:compute-ref #uuid "537ad61d-a9cb-4e09-a5db-06c5cdda02d3",
:exec-duration 106,
:id "e807b676-f720-4f90-8914-1d2b77319c20",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"e924ce6d-79a4-4b02-9e32-aa96de760ae8"
{:compute-ref #uuid "775db9ae-9883-4256-8885-3cf4b70a05bb",
:exec-duration 148,
:id "e924ce6d-79a4-4b02-9e32-aa96de760ae8",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"edef5d95-e18a-4060-8220-499f2357c8fa"
{:compute-ref #uuid "d9eb1231-db7b-4b67-bc46-926d452e4d9e",
:exec-duration 129,
:id "edef5d95-e18a-4060-8220-499f2357c8fa",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"f1194b86-62c8-49a2-bb0c-e78bfd9fb56e"
{:compute-ref #uuid "c8d418dc-63f8-4ec3-bd79-90c012daa085",
:exec-duration 97,
:id "f1194b86-62c8-49a2-bb0c-e78bfd9fb56e",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"f1b46312-dbc9-4a88-ab2b-c3b79be582c7"
{:compute-ref #uuid "c774f52f-0b5c-41ce-ab9b-c0bd9c021048",
:exec-duration 109,
:id "f1b46312-dbc9-4a88-ab2b-c3b79be582c7",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"f43fed4e-5dda-4e40-9804-fefd6adb127b"
{:compute-ref #uuid "06adc0a8-6c9f-4198-8160-b9c485810336",
:exec-duration 567,
:id "f43fed4e-5dda-4e40-9804-fefd6adb127b",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]},
"fbd4ed1d-1845-40fb-a2c6-2e786844352a"
{:compute-ref #uuid "fed387c3-8270-4c8d-8767-fc0ce154beb0",
:exec-duration 13054,
:id "fbd4ed1d-1845-40fb-a2c6-2e786844352a",
:kind "code",
:output-log-lines {},
:refs (),
:runtime [:runtime "3a85690b-683a-4fd9-9821-8b902ce0a2ff"]}},
:nextjournal/id #uuid "02be5b31-a0a6-4ba3-a466-c2169b4a470a",
:article/change
{:nextjournal/id #uuid "5f2c33d9-0618-4488-8573-d73edfc6af93"}}}
```