types, described internally, are realized externally as concrete particulars is complicated by differences in signatures and by competing processes with related signatures.
One of many ways perspectives can differ, dubbed SNAP/SPAN in Grenon and Smith 2004, is that between synchronic snapshots of continuants (or endurants) at fixed times and diachronic accounts of occurrents (or perdurants) spanning temporal stretches. A twist on SNAP/SPAN proposed by Antony Galton pulls processes away from events towards objects
objects
events processes
EXP objects processes
HIST
events
y |= ' for some y < x
to a time y earlier than x
For orientation, consider the language a+b accepted by the finite automaton A with three transitions start q0 a b
q1 q2 a over the initial state q0 and final (or accepting) state q1. A run of A is a sequence of transitions that A makes, such as q0 !a q2 !b q1, in the course of which, the finite automaton A changes its current state from q0 to q2 to q1. How does this picture fit with Galton’s proposal (†)? The automaton A coupled with its current state (initialized to q0) is an EXPprocess; a run is a HIST-event which describes change but does not itself change. Understood as accurate records of a past that is settled, HIST-events cannot change.1 As continuants, EXP-processes may change and indeed, as described by HIST-events, do.
The relationship between EXP and HIST is complicated by processes that need not run to completion; sentences (1) to (4) are from Dowty 1979 (page 133). (1) John was drawing a circle. (2) John drew a circle. (3) John was pushing a cart.
1In practice, of course, history does change, falling far short of an accurate record of the past. Revisions of HIST lie just outside the scope of the present paper. (4) John pushed a cart.
(3) implies (4), but (1) may hold without (2) holding. How
(1) can be true even if no circle was ever drawn by John
is what Dowty calls the Imperfective Paradox, for which
he appeals to inertia worlds that need not be actual.
Parsons 1990 eschews non-actual worlds, attributing the
difference between (2) and (4) to a notion of culmination over
and above holding. While the debate between intensional
and extensional accounts of the progressive continues
The moral for EXP/HIST, analyzed in terms of finite automata and their runs, is clear: any number of processes may run concurrently, not all of which may get completed.
The contrast between (3) implying (4) and (1) failing to
imply (2) has often been adopted as the litmus test for
processes versus events
abstract types
HIST-events/runs concrete particulars The complication raised by (1)-(6) above is that while EXPprocesses are typically conceived in isolation, they can be run, as HIST-events, alongside other EXP-processes that may interfere with them. What abstract types are manifested in concrete particulars can be tricky, making it tempting to focus on the concrete particulars and set aside abstract types to the extent that is possible.
Concentrating on concrete particulars, we will nevertheless avail ourselves of rudimentary forms of abstract types expressed by temporal propositions, called fluents for short. The particulars are analyzed at bounded granularities given by finite sets ⌃ of fluents. We keep the sets ⌃ finite in order to represent the runs by finite strings, enlarging ⌃ to lengthen the strings (refining the grain). The idea is familiar from the representations of a calendar year at various granularities. If the set ⌃ = {Jan, Feb, . . ., Dec} of months suggests the string of length 12, enlarging ⌃ with days d1,d2,. . .,d31 refines s⌃ to the string
Jan,d1 Jan,d2 · · · Jan,d31 Feb,d1 · · · Dec,d31 of length 366 for a leap year. We draw boxes (instead of the usual curly braces { and }) around sets qua symbols for a film strip. While it is irresistible to call the boxes SNAPshots, a change in ⌃ can cause a box to split, as Jan in s⌃ does (30 times) with the addition of d1,d2. . .,d31 Jan
Jan,d1 Jan,d2 · · · Jan,d31 SPANning 31 boxes. Similarly, a common Reichenbachian account of the progressive puts a reference time R inside the event time E,2 splitting E into 3 boxes
E
E E,R E (one before, one simultaneous, and one after R). We can also a encode runs of an automaton as strings; for example, q0 ! q2 !b q1 above as a, q2 b, q1 , leaving out the automaton’s initial state q0.
Encoding runs as strings is useful for expressing the
languages accepted by finite automata in Monadic
SecondOrder logic (MSO), one half of Bu¨chi’s theorem
9 x9 y(S(x, y) ^ Pa(x)) says a occurs before the end of the string. Confining our attention to finite models of size n 0,3 we write [n] for the set of integers from 1 to n
[n] := {1, 2, . . . , n} (with [0] = ; ) and Sn for the successor relation on [n]
Sn := {(i, i + 1) | i 2 [n] and i < n} (with S1 = S0 = ; ). A ⌃ S -model M = h[n], Sn{PaM }a2 ⌃ i interprets S as Sn and each Pa as a subset PaM of its domain [n] (for some n 0). In the terminology of Kripke semantics, h[n], Sni is a frame, while {PaM }a2 ⌃ defines the ⌃ -valuation v ✓ [n] ⇥ ⌃ such that v(i, a) () for all i 2 [n] and a 2 ⌃ . We can also view M as the finite automaton AM with initial state 1, final state n, and set of transitions {(i, S, j) | (i, j) 2 Sn} [ { (i, a, i) | a 2 ⌃ and i 2 PaM } 2See Moens and Steedman (1988), pp. 22 and 28 (footnote 3). 3We follow Libkin 2010 in allowing a model to have the empty set as its domain (universe). oav2er⌃ thseuaclhphthaabteti ⌃ 2[ {PaMS}in.For each i 2 [n], let us collect all ↵ i := {a 2 ⌃ | i 2 PaM }.
Then AM accepts the language
↵ 1⇤S↵ 2⇤S · · · S↵ n⇤ of strings s1Ss2S · · · Ssn 2 (⌃ [ { S})⇤ where si 2 ↵ i⇤ for i 2 [n]. What’s more, there is a bijection between ⌃ S models M and strings ↵ 1 · · · ↵ n over the powerset 2⌃ of ⌃ , as the equivalence
The formulas ' of Monadic Second-Order Logic (MSO) are generated through seven clauses ' ::=
S(x, y) | Pa(x) | X(x) | ' ^ ' 0 | ¬' | 9 x' | 9 X' from three disjoint infinite sets Var1, Var2 and ⇥ of firstorder variables x, y 2 Var1, second-order variables X 2 Var2, and fluents a 2 ⇥ , respectively. The vocabulary voc(' ) of ' is the finite subset of ⇥ occurring in ' voc(S(x, y)) = voc(X(x)) = ; voc(Pa(x)) = {a} voc(' ^ ' 0) = voc(' ) [ voc(' 0)
voc(¬' ) = voc(9 x' ) = voc(9 X' ) = voc(' ).
4The external/internal divide in Priorean tense logic is discussed at length in Blackburn 2006.
An MSO-sentence is understood to be an MSO-formula in which all variable occurrences are bound. We let Fin(⇥) be the set of finite subsets of ⇥ , and for every ⌃ 2 Fin(⇥) , put every MSO sentence with vocabulary contained in ⌃ into the set MSO(⌃) MSO(⌃) :=
{' | ' is an MSO-sentence and voc(' ) ✓ ⌃ }.
The notion of a ⌃ S -model M satisfying a sentence ' 2 MSO(⌃) , written M |=⌃ ' , is defined in the usual Tarskian manner. The ⌃ S -model h[n], Sn, {P M a }a2 ⌃ i is identified with the string ↵ 1 · · · ↵ n where ↵ i is {a 2 ⌃ | i 2 PaM } for each i 2 [n]. Thus, for each ⌃ 2 Fin(⇥) , ⌃ -satisfaction is a binary relation |=⌃ ✓ (2⌃ )⇤ ⇥
MSO(⌃) between (2⌃ )⇤ and MSO(⌃) . To describe how |=⌃ varies as ⌃ ranges over finite subsets of ⇥ , we define the function ⇢ ⌃ : (2⇥ )⇤ ! (2⌃ )⇤ that intersects a string in (2⇥ )⇤ componentwise with ⌃ for its ⌃ -reduct
⇢ ⌃ (↵ 1 · · · ↵ n) := (↵ 1 \ ⌃) · · · (↵ n \ ⌃) in (2⌃ )⇤ . For example, ⇢ {E}( E E,R E ) = E E E .
(2⌃ )⇤ ,
For all ⌃
2 Fin(⇥) , ' 2 MSO(⌃) and s 2 s |=⌃ ' ()
⇢ voc(' )(s) |=voc(' ) ' .
With Proposition 1, the relations {|=⌃ }⌃ 2 F in(⇥) become an
institution
Mod(⌃ 0, ⌃)( s) = ⇢ ⌃ (s) for all s 2 (2⌃ 0 )⇤ .
One may expect that for every sentence ' 2 MSO()⌃ , the set {s 2 (2⌃ )⇤ | s |=⌃ ' } is a regular language, in view of Bu¨chi’s theorem, BT, mentioned in the introduction. The problem, however, is that BT interprets ' 2 MSO(⌃) relative to strings over ⌃ , not 2⌃ as above. To establish the regularity of {s 2 (2⌃ )⇤ | s |=⌃ ' } via BT, we can translate ' 2 MSO(⌃) to ' ] 2 MSO(2⌃ ) homomorphically, treating Pa as the union of P⌃ 0 ’s for a 2 ⌃ 0 ✓ ⌃ Pa(x)] := _{P⌃ 0 (x) | ⌃ 0 ✓ ⌃ and a 2 ⌃ 0} for a 2 ⌃ .
MSO(⌃) with P⌃ 0 (x)] := ^
{Pa(x) | a 2 ⌃ 0} ^ ^{¬Pa(x) | a 2 ⌃ 2 MSO(2⌃ ) to
An advantage in interpreting MSO(⌃) relative to strings over
2⌃ is Proposition 1 above, the satisfaction condition for an
institution
A string s is understood to come with a fixed
granularity given by a signature ⌃ such that s 2 (2⌃ )⇤ . ⌃ -reducts
preserve string length. But as hinted by the discussion in the
introduction of
we should expect the length of a string to grow as we
enlarge ⌃ . To accommodate this growth, we implement
“McTaggart’s dictum that ‘there could be no time if nothing
changed”’
0 0 with ↵ 6= The restriction of bc to any finite alphabet is computable by a finite-state transducer, as are, for all ⌃ 0 2 Fin(⇥) and ⌃ ✓ ⌃ 0, the composition ⇢ ⌃ ; bc for bc⌃ bc⌃ (s) := bc(⇢ ⌃ (s)) for s 2 (2⌃ 0 )⇤ .
For example, if ⌃ is {Jan,Feb,. . .,Dec}, bc⌃ maps
Jan,d1 Jan,d2 · · · Jan,d31 Feb,d1 · · · Dec,d31 to s⌃ . Without the compression bc in bc⌃ , we are left with the map ⇢ ⌃ that leaves the ontology intact (insofar as the domain of an MSO-model is given by the string length), whilst restricting the vocabulary (for ⌃ -reducts). The institution described by Proposition 1 can be adjusted to another institution in which - the models are stutterless strings5 - the reducts ⇢ ⌃ are replaced by bc⌃ , and - the satisfaction relations |=⌃0 are given by explicitly referring to the sentence’s vocabulary s |=⌃0 ' a,tic a a,tic . The crucial point is that stutterlessness ensures the vocabulary is large enough to express the distinctions of interest (insofar as they lengthen a string).
The prefix relation on strings s prefix s0 ()
s0 = ssˆ for some sˆ lifts to maps a and a0 in IL(⇥ , bc) by universal quantification for an irreflexive relation a a0 () a 6= a0 and (8 ⌃ 2 Fin(⇥)) a(⌃) prefix a0(⌃) that is tree-like on IL(⇥ , bc) — i.e., transitive and left linear: for every a 2 IL(⇥ , bc), and all a1 a and a2 a, a1 a2 or a2 a1 or a2 = a1.
In other words, time branches at the inverse limit IL(⇥ , bc).
Working with the functions ⇢ ⌃ , we can decompose a string s 2 (2⌃ [ ⌃ 0 )⇤ as
s = ⇢ ⌃ (s) & ⇢ ⌃ 0 (s)
where superposition & forms the componentwise union of
strings of sets with the same length
(↵ 1 · · · ↵ n) & ( 1 · · · n) := (↵ 1 [
1) · · · (↵ n [
n)
inducing a relation of subsumption D
s D s0 ()
s&s0 = s
(9 s0 2 L) s D s0.
For example, a string s has length 2 iff s D +. We can reconstruct the Vendler classes described in Dowty 1979 and variants thereof by representing an event e at granularity ⌃ as a string str⌃ (e) 2 (2⌃ )+, relative to which we define e to be - ⌃ -dynamic if bc(str⌃ (e)) D - ⌃ -durative if bc(str⌃ (e)) D + + - ⌃ -telic if str⌃ (e) D ¬' + ' for some fluent ' 2 ⌃ (marking the culmination of e).
The choice of vocabulary ⌃ determines what a string can represent; it is linked in Fernando 2015 to, among other things, the event nucleus in Moens and Steedman 1988 (associating a preparatory phase, a culmination and a consequent state with an event, not all of which may be represented in a string). Up to granularity ⌃ , the string str⌃ (e) gives a completely deterministic picture of the event e. For non-determinism at ⌃ , we must look to a language (over the alphabet 2⌃ ) with more than the one string str⌃ (e).
EXP-processes as sets of strings Moving from strings ↵ 1↵ 2 · · · ↵ n to finite automata, let us recall from the introduction the deterministic automaton AM that accepts the language ↵ 1⇤S↵ 2⇤S · · · S↵ n⇤ over the alphabet ⌃ [ { S} and note that a transition in AM labeled by a 2 ⌃ does not move time forward (unlike one labeled by S). Whereas the previous section decomposes ↵ 1 · · · ↵ n through subsets of ⌃ , the present section decomposes a state also through the transitions from it, treating some of the transitions as fields that make up a record, and other transitions as specifications of types (including singletons for tokens). Take the famous example (7) of event modification/predication in Davidson 1967 (page 81). (7) Jones did it slowly, deliberately, with a knife
We associate (7) with the record (8) 2 who = hjonesi
3 6 66 how = 2 slow 6 6 6 4 3 77 7 466 dweiltihb=erahtkenifei775 7775 which we analyze presently as a minimal deterministic automaton accepting the four strings who jones, how slow, how deliberate and how with knife.
Automata can be formed from languages using a notion of
derivative connected with the Myhill-Nerode theorem
Ls := {s0 | ss0 2 L}
of strings that put after s belong to L
Ls = Ls0 .
The chain of equivalences a1a2 · · · an 2 L (from a1 · · · an to the empty/null string ✏) means that L is accepted by the deterministic automaton with - s-derivatives Ls as states - initial state L = L✏ - a-transitions from Ls to Lsa (for every symbol a) - final states Ls such that ✏ 2 Ls.
The Myhill-Nerode theorem says that a language L over a finite alphabet A is regular iff the set {Ls | s 2 A⇤ } of derivatives of L is finite. Note that Ls is non-empty precisely if s is the prefix of some string in L. Moreover, if Ls is empty then so is Lsa for every symbol a. That is, ; is a sink state that we may safely exclude from the states of the automaton above, at the cost of making the transition function partial. Let us define an A-state to be a non-empty subset q of A⇤ that is prefix-closed (i.e., for all sa 2 q, s 2 q). An A-state q can then make an a-transition to its a-derivative qa precisely if a 2 q.
Now, let us fix an infinite set Act of symbols that will play a role analogous to ⇥ in section 2 . For A 2 Fin(Act), let sen(A) be the set of formulas generated from a 2 A according to ' ::=
> | ¬' | ' ^ ' 0 | hai'
We extend hai' from a 2 A to strings s 2 A⇤ , defining h✏i' := ' and hasi' := haihsi' so that ha1 · · · ani'
= ha1i · · · hani'. and q |= hsi' ()
s 2 q and qs |= '.
Next, given a string s 2 Act⇤ and a set A 2 Fin(Act), we compute the longest prefix of s that belongs to A⇤ by the function ⇡ A : Act⇤ ! A⇤ defined by ⇡ A(✏) := ✏ and ⇡ A(as) := ⇢ a⇡ A(s) ✏ if a 2 A otherwise.
The A-restriction of a language q ✓ under ⇡ A
q A := {⇡ A(s) | s 2 q} .
If q is an Act-state, then its A-restriction, q A, is an A-state and is just the intersection q \ A⇤ with A⇤ . A-restrictions are interesting because satisfaction |= of formulas in sen(A) can be reduced to them.
Act-state q, and if, moreover, s 2 q A, then () () q |= '
q A |= ' q |= hsi'
(q A)s |= '.
For every A 2 Fin(Act), ' 2 sen(A) and Proposition 2 is proved by a routine induction on ' 2 sen(A).
There is structure lurking around Proposition 2 that is most conveniently described in category-theoretic terms. For A 2 Fin(Act), let Q(A) be the category with - A-states q as objects - pairs (q, s) such that s 2 q as morphisms from q to qs, with identities (q, ✏) and composition as concatenation (q, s) ; (qs, s0) := (q, ss0).
To turn Q into a functor from Fin(Act)op (with morphisms (A0, A) such that A ✓ A0 2 Fin(Act)) to the category Cat of small categories, we map a Fin(Act)op-morphism (A0, A) to the functor Q(A0, A) : Q(A0) ! Q(A) sending an A0-state q0 to the A-state q0 A, and the Q(A0)-morphism (q0, s0) to the Q(A)-morphism (q0 A, ⇡ A(s0)). The Grothendieck construction for Q is the category R Q where - objects are pairs (A, q) such that A 2 Fin(Act) and q is an A-state - morphisms from (A0, q0) to (A, q) are pairs
((A0, A), (q0 A, s))
of Fin(Act)op-morphisms (A0, A) and Q(A)-morphisms
(q0 A, s) such that (q0 A)s = q.
Given a small category C, let us write |C| for the set of objects of C. Thus, for A 2 Fin(Act), |Q(A)| is the set |Q(A)| = {q ✓
A⇤ | q 6= ; and q is prefix-closed} of A-states. Next, for (A, q) 2 |R Q|, let Mod(A, q) be the full subcategory of Q(A) with objects required to have q as a subset
|Mod(A, q)| := {q0 2 |Q(A)| | q ✓ q0}.
That is, |Mod(A, q)| is the set of A-states q0 such that for all
s 2 q, q0 |= hsi>. The intuition is that q is a form of record
typing over A that allows us to simplify clauses such as
q0 |= hsi'
when s 2 q ✓ q0
This comes close to the equivalence in Proposition 2, except that A-restrictions are missing. These reducts appear once we vary A, and step from Q(A) to R Q. Taking this step, we turn the categories Mod(A, q) to a functor Mod from R Q to Cat, mapping a R Q-morphism = ((A0, A), (q0 A, s)) from (A0, q0) to (A, q) to the functor
Mod( ) : Mod(A0, q0) ! Mod(A, q) sending q00 2 |Mod(A0, q0)| to the s-derivative of its Arestriction, (q00 A)s, and a Mod(A0, q0)-morphism (q00, s0) to the Mod(A, q)-morphism (q00 A, ⇡ A(s0)).
The syntactic counterpart of Q(A) is sen(A), which we turn into a functor sen matching Mod. A basic insight from Goguen and Burstall 1992 informing the present approach is the importance of a category Sign of signatures which the functor sen maps to the category Set of sets (and functions) and which Mod maps contravariantly to Cat. The definition of Mod above suggests that Signop is R Q.6 A R Qmorphism from R Q-objects (A0, q0) to (A, q) is determined uniquely by a string s 2 q0 A such that q = (q0 A)s and A ✓
A0.
(‡) Let (A, q) !s (A0, q0) abbreviate the conjunction (‡), which holds precisely if ((A0, A), (q0 A, s)) is a R Qmorphism from (A0, q0) to (A, q). Now for (A, q) 2 |R Q|, s let sen(A, q) be sen(A) (ignoring q), and when (A, q) ! (A0, q0), let
sen( ) : sen(A) ! sen(A0) send ' 2 sen(A) to h i
s ' 2 sen(A0). To see that an institution arises from restricting |= to |Mod(A, q)| ⇥ sen(A), for (A, q) 2 |R Q|, it remains to check the satisfaction condition: whenever (A, q) !s (A0, q0) and q00 2 Mod(A0, q0) and ' 2 sen(A), q00 |= hsi' () (q00 A)s |= '.
This follows from Proposition 2, as s must be in q0 A and thus also in q00 A.
Returning to sentence (7), let Act contain the finite set A := {who, jones, how, slow, deliberate, with, knife} so that if q is the A-state {who, how, how with,, ✏} then q [ { who jones, how slow, how deliberate, how with knife} is an (A, q)-model corresponding to the record (8) that (having a non-empty s-derivative for every s 2 q) has record type q. Records and types are employed extensively in Cooper 2012 as linguistic resources that, as argued in Cooper and Ranta 2008, characterize natural language. The relevance of this to EXP/HIST is expressed concisely by
EXP automata resources types
HIST ⇡ runs ⇡ uses ⇡ tokens where, in the simplest case, a token is a string, while a type is a language (to which the string may or may not belong).
4 EXP/HIST and connections Having likened EXP/HIST to modal/predicate logic in Table 1 (from the introduction), we brought out notions of granularity in sections 2 and 3 through signatures ⌃ , organized into a category Sign, from which institutionally, (i) a functor sen : Sign ! Set assigns a set sen(⌃) sentences of ⌃ (ii) a contravariant functor Mod : Signop ! Cat assigns a set |Mod(⌃) | of ⌃ -models, and 6That said, we might refine Sign, requiring of a signature (A, q) that q be a regular language. For this, it suffices to replace R Q by R R where R : Fin(Act)op ! Cat is the subfunctor of Q such that R(A) is the full subcategory of Q(A) with objects regular languages. We can make this refinement without requiring that Astates in Mod(A, q) be regular, forming Mod(A, q) from Q (not R). (iii) satisfaction relations |=⌃ relate ⌃ -models and ⌃ sentences smoothly across different signatures (made precise by the satisfaction condition).
Institutions were formed from a large set ⇥ of fluents in section 2 and a large set Act of symbols in section 3, as outlined in the table below.
signature
model sentence
⌃ 2 Fin(⇥) (2⌃ )⇤ -string
MSO⌃
EXP (A, q) where q ✓ A⇤
A-language ◆ q
Hennessy-Milner over A In HIST, a ⌃ -model is a (2⌃ )-string (where an X -string is a string over the alphabet X ), while in EXP, an (A, q)-model is an A-language that contains q (where an X -language is a set of X -strings). A comparison of Tables 1 and 2 raises the question: what has become of the clear difference between a HIST-model ↵ 1 · · · ↵ n and an EXP-model ↵ 1 · · · ↵ n, i in Table 1, consisting of a string position i 2 [n]?
A string ↵ 1 · · · ↵ n can be paired with a string position i 2 [n] within the institution built around MSO in section 2 with sentences expressive enough to capture Priorean tense logic (using second-order quantification for the transitive closure < of S). Indeed, for any 2⌃ -string ↵ 1 · · · ↵ n and set I ✓ [n] of string positions (including singletons {i} for i 2 [n]), we can encode the pair ↵ 1 · · · ↵ n, I as the 2⌃ [{ a}string ↵ 10 · · · ↵ n0, for some fluent a 2 ⇥ ⌃ , where ↵ j0 = := ⇢ ↵ j [ { a} ↵ j if j 2 I otherwise for j 2 [n]. The stutterless restriction on strings in section 2 (left out of Table 2 for simplicity) points to a conception of time as a container (containing what happens during it) that equates a stretch of time with the set of EXP-processes running over that stretch. Making a bounded granularity explicit reduces the implausibility of modeling an EXP-process as a finite automaton. But the complication discussed in the introduction relating to the Imperfective Paradox remains: (?) over any stretch of time, any number of EXP-processes may run, some interfering with others.
Competition between processes deepens the EXP/HIST
divide, moving away from the simple picture in Table 1
of EXP-processes reducible to HIST-runs. The primacy of
timelines is challenged by a causal realm that provides rules
and regulations over and above episodic instances recorded
in a timeline
If EXP is not reducible to HIST, might HIST be reducible to EXP? This depends on what EXP-processes are available for reducing HIST-strings to. For any string s, the singleton {s} is a regular language, embedding HIST-models trivially into EXP-models. But implicit in the complication (?) above is a view of the timeline as combining many separate EXP-processes, conceived largely in isolation and potentially clashing when run alongside other EXP-processes. That is, given a HIST-timeline s and an EXP-language m, we should ask not so much whether s 2 m (m being just one of the processes running in s, and thus too small to account for all of s) but rather whether there is a string s0 2 m that, for example, s subsumes (i.e., s D s0), or perhaps s D ⇤ s0 ⇤ (allowing s to extend before and/or after s0). Indeed, under (?), the string s0 2 m may not run to completion in s, suggesting a further weakening of the condition s D ⇤ s0 ⇤ . Let R be some such condition between s and s0, on the basis of which we link s and m, defining s0 R-connects (s, m) () sRs0 and s0 2 m.
We can explore different instantiations of R in HIST, by
expanding a signature ⌃ with a copy ⌃ 0 that is disjoint,
⌃ \ ⌃ 0 = ; , and forming model pairs
Proposition 3 Given two disjoint finite sets ⌃ and ⌃ 0, L ✓ (2⌃ [ ⌃ 0 )⇤ is a regular language iff there is an ✏-free finite-state transducer that computes the relation {(⇢ ⌃ (s), ⇢ ⌃ 0 (s)) | s 2 L}.
An example of a relation described by Proposition 3 is subsumption D, with the symbols renamed for disjoint copies. String pairs (s, s0) in which s D s0 pick out parts s0 of s that are of interest, often leaving some string positions empty. In the terminology of Carnap-Montague intensions, the index s provides a context for the denotation s0. The pair may fall outside subsumption D, as in the case (1) and not (2) of the Imperfective Paradox (where the event s0 of John drawing a circle may not be fully realized in the index s). The disjoint vocabularies for string pairs (s, s0) distinguish what is actual according to the index s from what the denotation s0 describes, allowing the strings to branch away from each other. Iterating the construction (and multiplying vocabularies), we can form any finite number of alternatives within HIST.
The sets of strings that serve as EXP-models in section
3 need not be finite. The strings in these sets may range
over HIST-timelines if we take Fin(⇥) to be the set Act
of symbols, finite subsets of which serve as the alphabets
A from which EXP-signatures (A, q) are formed. Implicit
in the simple membership s0 2 m in the definition of s0
R-connects (s, m) is the assumption that Act is essentially
Fin(⇥) . But different choices of Act are suitable for different
applications. To describe record types
B⇤ ) qs |= ' for every A-state q. (The arguments in section 3 carry over with this modification.) Exactly what sentences we associate with EXP is crucial if we are to relate EXP and HIST in the manner ontologies are related in, for example, Kutz, Mossakowski and Lu¨ cke 2010. The notion of s0 R-connecting (s, m) above takes a semantic approach that needs to be supplemented on the syntactic side. Much work remains to be carried out, not the least of which is an account within EXP of how to map choices of Act such as that made above for Davidson’s (7) to the HIST-timelines represented in section 2 as Fin(⇥) -strings. Are there, an anonymous referee asks, institution comorphisms between EXP and HIST? 5
Conclusion Behind the institutions above are the correspondences
HIST-event ⇡ internal mechanism external timeline ⇡ ⌃ automata string .
A HIST-timeline is where different EXP-processes, framed largely in isolation, go out to meet and be seen, as HISTevents. A finite approximability hypothesis attaches the subscript ⌃ on ⇡ , ranging over signatures that by bounding granularity, allow us to formulate the HIST-timelines as strings and the EXP-processes as finite automata. Structured as a category, the signatures provide a guide for exploring the forces that constitute the causal realm EXP, and their tortuous manifestations as events in the temporal realm HIST. Acknowledgments I am grateful to my anonymous referees for comments, and to Science Foundation Ireland’s ADAPT Centre for funding,