Outline of a Formal Theory of Processes and Events, and Why GIScience Needs One

All the theorems listed below have been proved, but there is no space here to include the proofs. These may be obtained from the author on request. We define a many-sorted first-order language with identity, with sorts \(\mathcal P\) (Processes), \(\mathcal E\) (Event types), and \(\mathcal T\) (Time instants). We could have introduced an additional sort for time intervals, but instead we will refer to an interval by means of a pair of instants, representing its beginning and end points. The primitive predicates are: Active, of type \(\mathcal{P}\times \mathcal{T}\), where Active( P,  t) means that P is on-going at t. Occurs, of type \(\mathcal{E}\times \mathcal{T}\times \mathcal{T}\), where \(Occurs(E,t_1,t_2)\) means that an event of type E occurs on the interval \([t_1,t_2]\). \(<\), of type \(\mathcal{T}\times \mathcal{T}\), where \(t_1<t_2\) means that \(t_1\) precedes \(t_2\). We assume the ordering \(<\) is irreflexive, transitive, linear, and dense; also, in one place, we assume that the order is continuous (a second-order property). The only axioms we assert here are that the start of an event precedes its end and that processes are active on open intervals: \(\mathbf{(AxOcc).}\quad Occurs(E,t_1,t_2)\rightarrow t_1<t_2\) \(\mathbf{(AxAct).}\quad Active(P,t)\rightarrow \exists t_1t_2(t_1<t<t_2\wedge \forall t'(t_1<t'<t_2\rightarrow Active(P,t')))\) We define a number of additional predicates, as follows: An event-type is discrete if distinct occurrences cannot overlap: A process is locally finite if it neither always has been, nor always will be, active: Subtype: The relation \({\sqsubseteq }\subset (\mathcal{E}\times \mathcal{E})\cup (\mathcal{P}\times \mathcal{P})\) is defined by Equality for event-types and processes: For \(X\in \mathcal{E}\cup \mathcal{P}\), Chunking: The function \(chunk: \mathcal{P}\rightarrow \mathcal{E}\) is defined contextually, via an occurrence condition for the event-type chunk( P), as follows: ¹² Dechunking: The function \(dechunk: \mathcal{E}\rightarrow \mathcal{P}\) is defined contextually, via an activity condition for the process dechunk( E), as follows: ¹³ Using these axioms and definitions we can prove: Discrete( chunk( P)). \(Discrete(E)\rightarrow LocFin(dechunk(E))\). The converse of Theorem 2 does not hold: if E has only two occurrences, which overlap, then dechunk( E) is locally finite but E is not discrete. The next two theorems show that for discrete events and locally finite processes, chunk and dechunk are mutually inverse. \(Discrete(E)\rightarrow chunk(dechunk(E))=E\). \(LocFin(P)\rightarrow dechunk(chunk(P))=P\). Note that even if P is not locally finite we have \(dechunk(chunk(P))\sqsubseteq P\), which holds for any process P. We define two different flavours of sequential composition operator, which we call weak and strong. Other definitions are possible. Weak Sequential Composition: The next theorem establishes the associativity of weak sequential composition: \(E_1;(E_2;E_3)=(E_1;E_2);E_3.\) As a result of this theorem, we can drop the parentheses and write \(E_1;E_2;E_3\). As noted in the main text, under Weak Sequential Composition \(E_1;E_2\) is not discrete. Strong Sequential Composition: The next theorem establishes that the strong sequential composition of two discrete events is discrete. \(Discrete(E_1)\wedge Discrete(E_2)\rightarrow Discrete(E_1\hat{;}E_2)\). As noted in the main text, the operator \(\hat{;}\) is not associative. For repetition, we want to define a process rep( E) which is active during a period in which E repeatedly occurs. The simplest case is where E occurs twice. This can be expressed as an occurrence of the event E;  E (but not \(E\hat{;}E\), since \(E\hat{;}E\) cannot occur). We define: This would mean that two occurrences of E suffice for this process to be active. Normally we would expect a larger number (think of our bursts of machine-gun fire). We could arbitrarily decide for some n that we require \(rep(E)=dechunk(E;E;\cdots ;E)\), where the right-hand side contains n copies of ‘ E’. While it would clearly not be feasible to fix an n which will always give satisfactory results, the important thing is that as we increase n we obtain a sequence of processes each of which is special case of the previous one. This is shown by the following theorem: \(dechunk(E;E;E)\sqsubseteq dechunk(E;E).\) As well as the indeterminacy as to how many repetitions of E are required before we say that the process rep( E) is active, there is an indeterminacy as to how far apart the individual occurrences of E must be in time. Resolution of both these indeterminacies must depend on the nature of the specific event-type in question and the context in which it is considered.

1 2 3 4 5 6 7 8 9 10 11 12 13