my forest
weeknotes and more ltp
+181
-5
assets/asas.jpg
assets/asas.jpg
This is a binary file and will not be displayed.
+1
trees/loc-001B.tree
+1
trees/loc-001B.tree
+4
trees/loc-003Z.tree
+4
trees/loc-003Z.tree
···
1
+
\title{Progress on linear-temporal properties research notes}
2
+
\date{2026-04-12}
3
+
\author{liamoc}
4
+
\p{I have made significant additions to my research notes on [[ltp-0001]]. Now I have all the relevant content from [[alpern-schneider-1985]], and some of the definitions that will appear in the forthcoming journal paper from [[rayhana]] and I. This paper finally got reviews back, and we have quite a few things to do but I'm confident we'll get there.}
+6
trees/loc-0040.tree
+6
trees/loc-0040.tree
···
1
+
\title{Holbert-NG status: pluggable terms and tangled}
2
+
\author{liamoc}
3
+
\date{2026-04-12}
4
+
\p{My students [[miowu]] and [[joshbrown]] have been doing some great work on the next generation of the Holbert proof assistant. In particular, [Josh](joshbrown) has now implemented a \em{pluggable} term structure, allowing various types of terms, each with their own unification methods and structure definitions, to be combined together in judgements. [Mio](miowu) is confident she can generalise his approach to work for higher order terms as well, which is very exciting.}
5
+
\p{As part of my general desire to stop using anything that feeds the LLM bots, I am gradually beginning to migrate off of GitHub. Fortunately the Holbert-NG crew are also happy to leave GitHub, so we are going to move to [tangled](https://tangled.org/liamoc.net/holbert-ng) for the time being. }
6
+
\p{I also got the chance to do some programming work myself. Soon we should have a similar proof UI to what the original Holbert has. I think most of the architecture is in place now.}
+25
trees/loc-0041.tree
+25
trees/loc-0041.tree
···
1
+
\import{table-macros}
2
+
\def\percent{\startverb%\stopverb
3
+
}
4
+
\parent{loc-000P}
5
+
\title{Low Sunday 2026}
6
+
\tag{cmc}
7
+
\date{2026-04-12}
8
+
\author{liamoc}
9
+
\quote{
10
+
Quasi modo géniti infántes, allelúia: rationábile, sine dolo lac concupíscite, allelúia, allelúia, allelúia
11
+
}
12
+
\p{Today at [All Saints Ainslie](https://allsaintsainslie.org.au) we had small numbers (I was the only tenor) but sang well for Walford Davies' [Blessed are the pure in heart](https://www.youtube.com/watch?v=jkFUl-jq3sk): }
13
+
\quote{
14
+
\poem{
15
+
\line{Blessed are the pure in heart,}
16
+
\line{For they shall see our God.}
17
+
\line{The secret of the Lord is theirs,}
18
+
\line{Their soul is Christ's abode.\br}
19
+
\line{Still to the lowly soul}
20
+
\line{He doth himself impart,}
21
+
\line{And for his dwelling and his throne}
22
+
\line{Chooseth the pure in heart.}
23
+
}
24
+
}
25
+
\p{Unfortunately we were plagued once again with sound system gremlins today. I'm honestly sick of it, the speakers and microphones are always barely working or not working. Apparently fixing it properly would cost tens of thousands of dollars the parish doesn't have. I don't know what can be done, but it's very frustrating.}
+14
-1
trees/ltp/ltp-0001.tree
+14
-1
trees/ltp/ltp-0001.tree
···
1
1
\taxon{Research Notebook}
2
+
\import{ltp-macros}
2
3
\title{Linear-time temporal properties}
3
4
\author{liamoc}
4
5
\transclude{ltp-0002}
···
25
26
\title{Properties as a topological space}
26
27
\scope{\put\transclude/metadata{true}\transclude{ltp-0007}}
27
28
\scope{\put\transclude/metadata{true}\transclude{ltp-000I}}
29
+
\scope{\put\transclude/metadata{true}\transclude{ltp-000N}}
30
+
\transclude{ltp-000P}
31
+
\scope{\put\transclude/metadata{true}\transclude{ltp-000O}}
28
32
\scope{\put\transclude/metadata{true}\transclude{ltp-000J}}
33
+
\transclude{ltp-000Q}
34
+
\transclude{ltp-000R}
35
+
\transclude{ltp-000S}
29
36
\transclude{ltp-000M}
30
37
}
31
38
\subtree{
32
39
\title{Concerning liveness properties}
33
40
\transclude{ltp-0006}
34
41
\scope{\put\transclude/metadata{true}\transclude{ltp-000K}}
42
+
\transclude{ltp-000T}
43
+
\transclude{ltp-000U}
35
44
\scope{\put\transclude/metadata{true}\transclude{ltp-000L}}
36
-
% closure properties go here?
45
+
}
46
+
\subtree{
47
+
\title{Concerning LTL}
48
+
\transclude{ltp-000V}
49
+
\transclude{ltp-000W}
37
50
}
+1
-1
trees/ltp/ltp-0002.tree
+1
-1
trees/ltp/ltp-0002.tree
···
3
3
\title{Traces and behaviours}
4
4
\author{liamoc}
5
5
\p{Let the set of all possible \em{states} be #{\Sigma}. Note that we do not require that #{\Sigma} is finite. Then, #{\ftraces} is the set of finite sequences of states. We denote the empty sequence as #{\varepsilon}. The concatenation of two sequences #{t} and #{u} is written #{tu}. }
6
-
\p{The set of all \em{behaviours} — \em{infinite} sequences of states — is #{\itraces}. We define #{\sigma{}t = \sigma} when the sequence #{\sigma} is infinite. }
6
+
\p{The set of all \em{behaviours} — \em{infinite} sequences of states — is #{\itraces}. We define #{\sigma{}t = \sigma} when the sequence #{\sigma} is infinite. We say that #{t} is a \em{prefix} of #{u} (or #{u} is an \em{extension} of #{t}) iff there exists some #{w} such that #{tw = u}.}
7
7
\p{We shall model terminating systems, which have finite behaviours, as behaviours that infinitely repeat their final state.}
+2
-1
trees/ltp/ltp-0003.tree
+2
-1
trees/ltp/ltp-0003.tree
···
2
2
\taxon{Definition}
3
3
\import{ltp-macros}
4
4
\author{liamoc}
5
-
\p{A property, being a specification of a system, can be thought of as simply a set of behaviours, i.e. a subset of [the space #{\itraces{}}](ltp-0002). A property is \em{satisfied} by a system if all behaviours exhibited by the system are contained within the set. It is \em{violated} by a system if there exists a behaviour exhibited by the system that is not contained within the set. }
5
+
\p{A property, being a specification of a system, can be thought of as simply a set of behaviours, i.e. a subset of [the space #{\itraces{}}](ltp-0002). A property is \em{satisfied} by a system if all behaviours exhibited by the system are contained within the set. It is \em{violated} by a system if there exists a behaviour exhibited by the system that is not contained within the set.}
6
+
\p{The complement of a property, written #{\compl{P}}, is the set of all behaviours that violate the property #{P}, i.e. #{\itraces \setminus P}.}
+1
-1
trees/ltp/ltp-000F.tree
+1
-1
trees/ltp/ltp-000F.tree
···
3
3
\import{ltp-macros}
4
4
\author{liamoc}
5
5
\title{Guarantee properties are closed under union}
6
-
\p{For a (possibly infinite) collection of properties #{P_{i \in I}}, if every #{P_i} is a [guarantee property](ltp-0005) then #{\bigcup_{i \in I} P_i} is a [guarantee property](ltp-0005). }
6
+
\p{For a (possibly infinite) collection of [properties](ltp-0003) #{P_{i \in I}}, if every #{P_i} is a [guarantee property](ltp-0005) then #{\bigcup_{i \in I} P_i} is a [guarantee property](ltp-0005). }
7
7
\proofblock{ \p{Let #{ P_{i \in I}} be a (possibly infinite) family of [guarantee properties](ltp-0005). Then each #{\compl{P_i}} is a [safety property](ltp-0004) and therefore #{\bigcap_{i \in I} \compl{P_i}} is a [safety property](ltp-0004) by \ref{ltp-0008}. Its complement #{\compl{(\bigcap_{i \in I} \compl{P_i})} = \bigcup_{i \in I} P_i} is therefore a [guarantee property](ltp-0005).}}
+13
trees/ltp/ltp-000N.tree
+13
trees/ltp/ltp-000N.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Guarantee kernel distributes over finite intersection}
5
+
\meta{source}{(from [[amjad-vanglabbeek-oconnor-2026]])}
6
+
\p{The [guarantee kernel](ltp-000I) distributes over binary intersection, i.e. #{\gk{P} \cap \gk{R} = \gk{P \cap R}}}
7
+
\proofblock{
8
+
\p{Showing each direction separately:}
9
+
\ul{
10
+
\li{#{\gk{P} \cap \gk{R} \subseteq \gk{P \cap R}}: Let #{\sigma} be a [behaviour](ltp-0002) in #{\gk{P} \cap \gk{R}}. There must exist a prefix #{t} of #{\sigma} which is a [good prefix](ltp-000D) for #{P}, and a prefix #{u} of #{\sigma} which is a [good prefix](ltp-000D) for #{R}. Because both #{t} and #{u} are prefixes of #{\sigma}, either #{t} is a prefix of #{u} or #{u} is a prefix of #{t}. If #{t} is a prefix of #{u}, then #{u} must also be a [good prefix](ltp-000D) for #{P \cap R} and thus #{\sigma \in \gk{P \cap R}}. Likewise for #{t} when #{u} is a prefix of #{t}.}
11
+
\li{#{\gk{P} \cap \gk{R} \supseteq \gk{P \cap R}}: Follows from [monotonicity of guarantee kernel](ltp-000I).}
12
+
}
13
+
}
+6
trees/ltp/ltp-000O.tree
+6
trees/ltp/ltp-000O.tree
···
1
+
\taxon{Counterexample}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Guarantee kernel does not distribute over union}
5
+
\meta{source}{(from [[amjad-vanglabbeek-oconnor-2026]])}
6
+
\p{Take the [properties](ltp-0003) #{P = \{ \sigma \mid \texttt{a}\ \text{occurs infinitely often in}\ \sigma\}} and #{R = \{ \sigma \mid \texttt{a}\ \text{occurs finitely many times in}\ \sigma\}}. Both have an empty [guarantee kernel](ltp-000I), i.e. #{\gk{P} = \gk{R} = \emptyset}, however #{P \cup R = \itraces} so the [guarantee kernel](ltp-000I) of the union is #{\itraces}, not #{\emptyset}. }
+6
trees/ltp/ltp-000P.tree
+6
trees/ltp/ltp-000P.tree
···
1
+
\taxon{Counterexample}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Guarantee kernel does not distribute over infinite intersection}
5
+
\author{liamoc}
6
+
\p{Follows from \ref{ltp-000H}. As each #{P_i} is a [guarantee property](ltp-0005), the [guarantee kernel](ltp-000I) of each #{P_i} is just #{P_i}. But the [guarantee kernel](ltp-000I) of their infinite intersection #{\bigcap_{i \in \mathbb{N}} P_i} is #{\empty}.}
+16
trees/ltp/ltp-000Q.tree
+16
trees/ltp/ltp-000Q.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Safety closure distributes over finite union}
5
+
\author{liamoc}
6
+
\p{The [safety closure](ltp-000J) distributes over binary union, i.e. #{\sc{P} \cup \sc{R} = \sc{P \cup R}}}
7
+
\proofblock{
8
+
Follows from \ref{ltp-000N}: ##{
9
+
\begin{array}{lcl}
10
+
\sc{P} \cup \sc{R} &=& \compl{\gk{\compl{P}}} \cup \compl{\gk{\compl{R}}} \\
11
+
& = & \compl{(\gk{\compl{P}} \cap \gk{\compl{R}})} \\
12
+
& = & \compl{(\gk{\compl{P} \cap \compl{R}})} \\
13
+
& = & \sc{\compl{(\compl{P} \cap \compl{R})}} \\
14
+
& = & \sc{P \cup R} \end{array}
15
+
}
16
+
}
+6
trees/ltp/ltp-000R.tree
+6
trees/ltp/ltp-000R.tree
···
1
+
\taxon{Counterexample}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Safety closure does not distribute over infinite union}
5
+
\author{liamoc}
6
+
\p{Follows from \ref{ltp-000E}. As each #{P_i} is a [safety property](ltp-0004), the [safety closure](ltp-000j) of each #{P_i} is just #{P_i}. But the [safety closure](ltp-000J) of their infinite union #{\bigcup_{i \in \mathbb{N}} P_i} is #{\itraces}.}
+6
trees/ltp/ltp-000S.tree
+6
trees/ltp/ltp-000S.tree
···
1
+
\taxon{Counterexample}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Safety closure does not distribute over intersection}
5
+
\author{liamoc}
6
+
\p{Take the [properties](ltp-0003) #{P = \{ \sigma \mid \texttt{a}\ \text{occurs infinitely often in}\ \sigma\}} and #{R = \{ \sigma \mid \texttt{a}\ \text{occurs finitely many times in}\ \sigma\}}. Both have a [safety closure](ltp-000J) of #{\itraces}, i.e. #{\sc{P} = \sc{R} = \itraces}, however #{P \cap R = \emptyset} so the [safety closure](ltp-000J) of the intersection is #{\emptyset}, not #{\itraces}. }
+7
trees/ltp/ltp-000T.tree
+7
trees/ltp/ltp-000T.tree
···
1
+
\taxon{Theorem}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Liveness properties are closed under union}
5
+
\p{For a (possibly infinite) collection of [properties](ltp-0003) #{P_{i \in I}}, if every #{P_i} is a [liveness property](ltp-0006) then #{\bigcup_{i \in I} P_i} is a [liveness property](ltp-0006). }
6
+
\proofblock{
7
+
\p{Let #{P_{i \in I}} be a family of [liveness properties](ltp-0006). Because [liveness properties are dense](ltp-000K), for any #{i}, #{\sc{P_i} = \itraces}. As [safety closure is monotonic](ltp-000J), #{\itraces \subseteq \sc{\bigcup_{i \in I} P_i }}. Therefore the union is [dense](ltp-000K) #{\sc{\bigcup_{i \in I} P_i } = \itraces} and therefore a [liveness property](ltp-0006). }}
+5
trees/ltp/ltp-000U.tree
+5
trees/ltp/ltp-000U.tree
···
1
+
\taxon{Counterexample}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Liveness properties are not closed under intersection}
5
+
\p{Take the [properties](ltp-0003) #{P = \{ \sigma \mid \texttt{a}\ \text{occurs infinitely often in}\ \sigma\}} and #{R = \{ \sigma \mid \texttt{a}\ \text{occurs finitely many times in}\ \sigma\}}. Both are [liveness properties](ltp-0006), i.e. [dense](ltp-000K) (#{\sc{P} = \sc{R} = \itraces}), however #{P \cap R = \emptyset} which is not a liveness property (as #{\sc{\emptyset} = \emptyset} not #{\itraces}).}
+26
trees/ltp/ltp-000V.tree
+26
trees/ltp/ltp-000V.tree
···
1
+
\taxon{Definition}
2
+
\import{dt-macros}
3
+
\import{ltp-macros}
4
+
\title{Linear-time temporal logic}
5
+
\p{[Properties](ltp-0003) are commonly written using \em{linear-time temporal logic} (LTL), a modal logic defined over [behaviours](ltp-0002). Given atomic propositions #{\mathsf{a} : \Sigma \rightarrow \bool}, the syntax for formulae is given by: }
6
+
##{ \begin{array}{lcl}
7
+
\varphi, \psi &::=& \top \mid \bot \mid \mathsf{a} \mid \varphi \land \psi \mid \varphi \lor \psi \mid \neg \varphi \\
8
+
&\mid& \next \varphi \mid \eventually \varphi \mid \always \varphi \mid \varphi \until \psi \mid \varphi \release \psi \end{array} }
9
+
\p{To assign semantics, we compositionally map each formula to a [property](ltp-0003). Here the notation #{f^k} indicates the self-composition of #{f} #{k} times, i.e. #{f^0(x)=x} and #{f^{k+1}(x)=f^k(f(x))}. The function #{\prep}, the \em{prepend operator}, is defined as follows:}
10
+
##{\prep X = \{ s\sigma \mid s \in \Sigma \land \sigma \in X \}}
11
+
12
+
##{\begin{array}{lcl}
13
+
\sems{\top} &=& \itraces \\
14
+
\sems{\bot} &=& \emptyset \\
15
+
\sems{\mathsf{a}} &=& \{ \sigma \mid \mathsf{a}(\sigma_0) \} \\
16
+
\sems{\varphi \land \psi} &=& \sems{\varphi} \cap \sems{\psi} \\
17
+
\sems{\varphi \lor \psi} &=& \sems{\varphi} \cup \sems{\psi} \\
18
+
\sems{\neg \varphi} &=& \compl{\sems{\varphi}} \\
19
+
\sems{\next \varphi} &=& \prep\sems{\varphi} \\
20
+
\sems{\eventually \varphi} &=& \bigcup_{i \in \mathbb{N}}\prep^i\sems{\varphi} \\
21
+
\sems{\always \varphi} &=& \bigcap_{i \in \mathbb{N}}\prep^i\sems{\varphi} \\
22
+
\sems{\varphi \until \psi} &=& \bigcup_{i \in \mathbb{N}}f^k(\sems{\psi})\text{, where}\ f(X) = \prep X \cap \sems{\varphi}\\
23
+
\sems{\varphi \release \psi} &=& \bigcap_{i \in \mathbb{N}}f^k(\sems{\psi})\text{, where}\ f(X) = \prep X \cup \sems{\varphi}\\
24
+
\end{array}
25
+
}
26
+
\p{These semantics are sometimes written in terms of a satisfaction relation like #{\sigma \models \varphi}. This notation is equivalent to our #{\sigma \in \sems{\varphi}}.}
+15
trees/ltp/ltp-000W.tree
+15
trees/ltp/ltp-000W.tree
···
1
+
\import{dt-macros}
2
+
\import{ltp-macros}
3
+
\title{A minimal fragment of LTL}
4
+
\p{All of the connectives [linear-time temporal logic](ltp-000V) can be constructed from the following minimal fragment (among others:) }
5
+
##{ \begin{array}{lcl}
6
+
\varphi, \psi &::=& \top \mid \mathsf{a} \mid \varphi \land \psi \mid \neg \varphi \mid \next \varphi \mid \varphi \until \psi \end{array} }
7
+
\p{The remaining connectives can be derived by using the following identities:
8
+
\ul{
9
+
\li{#{\bot \equiv \neg \top}}
10
+
\li{#{\varphi \lor \psi \equiv \neg (\neg\varphi \land \neg\psi) }}
11
+
\li{#{\eventually \varphi \equiv \top \until \varphi}}
12
+
\li{#{\always \varphi \equiv \neg \eventually \neg \varphi}}
13
+
\li{#{\varphi \release \psi \equiv \neg (\neg \varphi \until \neg \psi)}}
14
+
}
15
+
(where #{\varphi \equiv \psi} means #{\sems{\varphi} = \sems{\psi}})}
+9
-1
trees/ltp/ltp-macros.tree
+9
-1
trees/ltp/ltp-macros.tree
···
3
3
\def\fitraces{\Sigma^\infty}
4
4
\def\compl[body]{\body^\complement}
5
5
\def\gk[body]{\underline{\body}}
6
-
\def\sc[body]{\overline{\body}}
6
+
\def\sc[body]{\overline{\body}}
7
+
\def\bool{\mathbb{B}}
8
+
\def\eventually{\mathop{\raisebox{-0.2em}{\text{\Large ◇}}}}
9
+
\def\always{\mathop{\raisebox{-0.1em}{\text{\Large □}}}}
10
+
\def\until{\mathbin{\mathcal{U}}}
11
+
\def\release{\mathbin{\mathcal{R}}}
12
+
\def\next{\mathop{\raisebox{-0.2em}{\text{\Large ○}}}}
13
+
\def\sems[body]{\llbracket\body\rrbracket}
14
+
\def\prep{\mathop{\triangleright}}
+12
trees/weeknotes/2026-W15.tree
+12
trees/weeknotes/2026-W15.tree
···
1
+
\import{table-macros}
2
+
\title{Weeknotes 2026-W15}
3
+
\author{liamoc}
4
+
\date{2026-04-12}
5
+
\p{Thankfully this is the first week of semester break, so I was actually able to do a little research work.}
6
+
\figure{
7
+
\<html:img>[loading]{lazy}[width]{480px}[src]{\route-asset{assets/asas.jpg}}%{}
8
+
\figcaption{All Saints Ainslie in evening silhouette.}
9
+
}
10
+
\transclude{loc-003Z}
11
+
\transclude{loc-0040}
12
+
\transclude{loc-0041}