Rule sets and games

Peter Hancock

Never. May 9, 1999

Contents

1 Introduction 2 1.1 Structure, ish . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 Notions of powerset 3

3 Notions of identity 5

4 One way to model rule sets 6

5 Predicate transformers 8 5.1 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 5.2 Winning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

6 Programming with rule sets 11 6.1 Sequential composition . . . . . . . . . . . . . . . . . . . . . . 11 6.2 Alternative composition . . . . . . . . . . . . . . . . . . . . . 11 6.3 Some basic rule structures . . . . . . . . . . . . . . . . . . . . 12

6.3.1 Skip, update . . . . . . . . . . . . . . . . . . . . . . . . 12 6.3.2 Magic, assume . . . . . . . . . . . . . . . . . . . . . . . 13 6.3.3 Abort, assert . . . . . . . . . . . . . . . . . . . . . . . 13 6.3.4 Guarding . . . . . . . . . . . . . . . . . . . . . . . . . 13

6.4 Other forms of composition . . . . . . . . . . . . . . . . . . . 14 6.5 Representing closure . . . . . . . . . . . . . . . . . . . . . . . 15

7 Relation transformers 15 8 Implementations and bugs 16

8.1 Bugs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

9 The mother of all closure operations 18

10 General perspective on rule sets 19

11 Related notions 21

1 Introduction

Aczel’s rule sets were introduced in [1]. A rule set is a set S of statements, together with a structure of the form:

Φ : S → P(P(S))

where P(X ) is the powerset of X . This structure assigns to a statement s ∈ S the set of those sets of statements from which s may be inferred in one step.

It should be pointed out immediately that this is not exactly Aczel’s formulation, which is:

Φ : P(P(S) × S)

The two are nevertheless equivalent, by the isomorphism

between  P(X × Y ) and Y → P(X )
which sends R ⊆ X × Y to λy. { x : X | R(x, y) } : Y → P(X )

Note that the same isomorphism (applied to the transposed relation R^{T} ⊆ Y × X ) yields yet another formulation:

Φ : P(S) → P(S)

As shown in Dybjer’s paper [4], rule sets play a fundamental rôle with respect to principles of inductive definition. He puts them to use in constructing realisability interpretations of systems of dependent types with strong universe principles .

We obtain a variety of notions of rule set by interpreting and restricting the notion of powerset in various ways. In these notes, I have interpreted ‘subset of S’ as ‘indexed family of S’s. For variations on that theme, it seems fruitful to replace Aczel’s formulation by the one given first.

The notion of rule set seems also to have many applications. By the isomorphism last mentioned, rule sets represent monotone predicate transformers of the kind used in formal program development [Dijkstra, Morgan]. This suggests a way to bring this approach to program development within the reach of type systems supporting sufficiently strong principles of inductive definition. An obstacle here is that the classical theory exploits the fully impredicative notion of the complete lattice of subsets of a set in order to deal with iteration and recursion.

The problem arises of how to formulate the notion of rule set in a constructive setting, leanly enough that one can actually ‘program’ with rule sets, as a fundamental, pervasive data type.

1.1 Structure, ish

(Out of date. Degenerated.) The first few sections of these notes concern the notions of powerset and identity in type theory. Then comes my favourite formulation of the notion of rule system, and an indication the kinds of situation in which the notion is applicable.

We define two predicate transformers associated with a rule set. We show how various operators on predicate transformers, particularly inductive closure, may be represented by operators on rule sets. We take a look at the notion of a morphism between rule sets, which is a kind of inference−by−inference translation of potentially proofs, related to simulation between states in a labelled transition system. It is not entirely clear how to deal with potentially infinite structures in type theory. Can one really define composition between morphisms without some form of corecursion?

These ideas can be seen in quite a general perspective, as indicated in the final section. It seems worthwhile to investigate connections with the work mentioned there.

2 Notions of powerset

If one reflects on the kinds of set expression that occur in nature, that is in the application of set theory to problems in real life (where one is not interested in set theory for its own sake), there seem to be two. I shall call there parametric and separative.

parametric { p(i) | i : I } p : I → S
separative { s : S | P(s) } P a predicate on S

In a set expression of parametric form, we have a function p defined on an index set I , which gives a generic element p(i) of the set expressed in terms of the parameter i : I . For example, a parabola with vertex at the origin and focus at (1, 0) is the set of points { (t^{2}, 2t) | t : R } indexed by the set R of real numbers.

In a set expression of separative (form, we pick out the elements of the set from a given set S with a predicate P, or propositional (i.e. proposition valued) function, defined on S. Instead of ‘proposition’, one may say ‘truth value’. Here I shall take a proposition to be the set of its proofs, in line with the Curry−Howard correspondence. So a predicate defined on S is a function defined on S whose values are sets.

These two forms of set expression correspond to the so called covariant (parametric) and contravariant (separative) powerset functors, which may be written as follows:

Fam(X )  = ( Σ I : Set ) I → X
Fam(f : X → Y ) = λ(I , p). (I , f ^{∘} p) : Fam(X ) → Fam(Y )
Pred(X )  = X → Set
Pred(f : X → Y ) = λP. P ^{∘} f : Pred(Y ) → Pred(X )

In order to type the operators Fam and Pred, some questions of size remain. Letting Type denote the (large) category of sets and functions between them, in the following I shall suppose that the functors Fam and Pred are both to be typed as follows. This accords with the analysis of the notions in predicative type theory.

Fam, Pred : Type → Type

Both these notions may be relativised to a ‘universe’ of sets U = (A, B) : Fam(Set). (For example, the countable family of finite sets.) An (A, B)−predicate is then simply a function into A, while an (A, B)−family is a family in which the index sets are restricted to have the form B(a) for a : A. (This seems most useful when the family U is closed under ( Σ ) , contains the empty set, contains a standard singleton, and is closed under binary disjoint union.)

3 Notions of identity

I wish to abstain from assuming that for an arbitrary type a there is canonical equivalence relation, which maps a pair of objects to a set; that is to say, I do not use any form of schematic identity type. There are a number of equivalence relations which percolate in a more or less obvious way through the usual type forming operators. [ These rarely coincide with the naturally interesting equalities: between convergent sequences of rationals, or tree−sets, for examples.] But this percolation is far short of having a single ‘god−given’ universal equality construction. It is not clear to me under what conception of inductive definitions (or indeed of judgement) one can introduce the least reflexive relation I_{S}(s, s′) on a set S, since the constructors of a set are then introduced under a judgemental constraint (i.e. hypothesis) that s and s′ are equal, and it is not clear how equational constraints can be interpreted in a context. Because of these misgivings, I am particularly interested in constructions which can be defined with no reference to ‘equality’ on a set, most particularly in constructions of equivalence relations.

The relation between the two kinds of powerset hinges on how we interpret equality. Let S be some fixed (small or large) set.

• If { s : S | P(s) } is a separative subset of a small set S, then we may define a parametric subset

{ fst(sp) | sp : ( Σ s : S ) P(s) }

Note however that this does not work if S is large.

• If we have an equivalence relation ‘=’ on the set S, we can define for each s a singleton predicate.

{ } : S → Pred(S)
{s } =^{Δ} λs′. s′ = s

This is enough, by the next point, to interpret families as predicates.

• Both predicates and families are closed under unions (of small families).

⋃_{i:I} P(i)  = λs. ( Σ i : I ) P(i, s)
⋃_{i:I} (J (i), λj . p(i, j )) = λs. (( Σ i : I ) J (i), λ(i, j ). p(i, j ))

• Predicates are closed under intersections (of small families of predi-

cates).

⋂_{i:I} P(i) = λs. ( ∏ i : I ) P(i, s)

This does not seem to hold for families, even for finite intersections, as the notion of intersection requires a notion of equality.

• We can say that a family is included in a predicate.

{ p(i) | i : I } ⊆ { s : S | P(s) }

=^{Δ} ( ∏ i : I ) P(p(i))

• We can say a family intersects with (i.e. has nonempty intersection with) a predicate.

{ } ≠ { p(i) | i : I } ∩ { s : S | P(s) }

=^{Δ} ( Σ i : I ) P(p(i))

• To say that a predicate is included in a family requires equality.

{ s : S | P(s) } ⊆ { p(i) | i : I }
=^{Δ} ( ∏ s : S ) P(s) ⇒ ( Σ i : I ) p(i) = s

• Families of S’s live in the slice category (Set/S) over S, while predicates of S’s live in the functor category Set^{S}. (Saunders MacLane, Ieke Moerdijk, Sheaves in Geometry and Logic, A First Introduction to Topos Theory, Springer−Verlag, 1992, pp. 28−29. )

4 One way to model rule sets

Let us model rule sets with structures of the form:

(S, Φ) : ( Σ S : Set ) S → Fam^{2}(S)

I call the function Φ a rule structure

The elements of the set S are to be thought of as statements. Then the structure Φ assigns to a statement s a family of families of statements − exactly those families of statements from which s may be immediately inferred. This is depicted in the following picture, in which a white circle represents a statement, the black circles linked to it represent the inferences with that statement as conclusion, and the white circles linked to an inference represent the statements of the premises of that inference.

[figure: …; …; …; …; …; …; statement (conclusion); inference; statement (premises)]

The pictorial device of ‘white’ and ‘black’ nodes is stolen from Samson Abramsky’s ‘Semantics of Interaction: an Introduction to Game Semantics’ [page 4, Semantics and Logics of Computation, ed. A. Pitts and P. Dybjer], where it is used to depict game trees. The connection between inferential systems and games, or more generally dialectical/interactive processes of some kind was made by Lorenzen [Ein dialogisches Konstruktivitätskriterium, in Infinitistic methods, Proceedings of the symposium on Foundations of Mathematics, Pergamon, 1961, pp 193−200], but it is arguably implicit in Gentzen’s first proof of the consistency of Peano arithmetic [Coquand??]. It is explained in Aczel’s chapter [op cit]. See also Coquand, Computational content of classical logic [??].

If S is a set, then an element of S → Fam^{2}(S) has the form:

Φ = λs. (R(s), λr. (P(s, r), λp. s[r/p]))

where

R : S → Set
P : ( ∏ s : S ) R(s) → Set
λs r p. s[r/p] : ( ∏ s : S, r : R(s) ) P(s, r) → S

The structure (S, R, P, λs r p. s[r/p]) was already identified by Petersson and Synek [??], who arrived at it when looking for a abstract type−theoretical formulation of the grammatical notion of context−free production system. The structure is extremely rich in applications, as indicated by the table in figure 1.

We may re−express the general form of a rule structure

Φ = λs. (R(s), λr. (P(s, r), λp. s[r/p]))

making use of the Pred notation.

R : Pred(S)
λ(s, r). (P(s, r), λp. s[r/p]) : (( Σ s : S ) R(s)) → Fam(S)

S  R(s)  P(s, r)  s[r/p]
sort  constructor destructor component sort
statement  inference  premise  premise formula
neighbourhood partition  part  new neighbourhood
game  attack  defence  new state
interrogation question  answer  new state
interface  call  return  new state
universe  observation reading  new state
knowledge  experience result  new state
dialogue  thesis  antithesis synthesis

Figure 1: Interpretations of the structure.

It can be seen as a predicate of states, and a function from states satisfying the predicate to families of states (cf. realisability models). Note that the family may depend of the proof that R holds. However, the extension of the family may be independent of the proof.

5 Predicate transformers

If S is a set, then an element of S → Fam^{2}(S) has the form:

Φ = λs. (R(s), λr. (P(s, r), λp. s[r/p]))

Here, R(s) is the set of inferences which have statement s : S as their conclusion, P(s, r) is the set of premises of inference r : R(s). I shall use the notation s[r/p] for the statement to be proved by the p−th premise.

Any such structure Φ determines a pair of predicate transformers Φ^{∘}, Φ^{•} as follows:

Φ^{∘}, Φ^{•}  : Pred(S) → Pred(S)
Φ^{∘}(X , s) =^{Δ} ( Σ r : R(s) ) ( ∏ p : P(s, r) ) X (s[r/p])
Φ^{•}(X , s) =^{Δ} ( ∏ r : R(s) ) ( Σ p : P(s, r) ) X (s[r/p])

It is obvious that both the predicate transformers Φ^{∘} and Φ^{•} determined by a rule structure Φ are monotone, as the input predicate occurs only positively in their defining expressions.

Note that any predicate transformer of • form also has ∘ form, because of the following isomorphism.

( ∏ r : R(s) ) ( Σ p : P(s, r) ) X (s[r/p])

≅ ( Σ f : ( ∏ r : R(s) ) P(s, r) ) ( ∏ r : R(s) ) X (s[r/f (r)])

Given a rule structure Φ we define Φ^{⊥} by:

R^{⊥}(s)  =^{Δ} ( ∏ r : R(s) ) P(s, r)
P^{⊥}(s, )  =^{Δ} R(s)
s[λr. p(r)/r] =^{Δ} s[r/p(r)]

Then (Φ^{⊥})^{∘} = Φ^{•}, by the axiom of choice.

5.1 Discussion

Intuitively, to demonstrate that Φ^{∘}(X ) holds of a statement we must exhibit an inference of that statement and show that all premises of the inference satisfy X . (If there is an inference of s with no premises, then Φ^{∘}(X , s) holds for any predicate X , even the empty predicate.) On the other hand, to demonstrate that Φ^{•}(X ) holds of a statement we must show that any inference of that statement has a premise which satisfies X . (If there is no inference with conclusion s, then Φ^{•}(X , s) for any predicate X .) By the classical de Morgan rules, the two operators are dual in the sense that ∁^{∘} Φ^{∘} = Φ^{•} ^{∘} ∁ and vice versa, where ∁ is the complementation operator on predicates.

We may think of a rule structure Φ as representing the rules of a game, in which the state of the game is a goal statement, the defendant chooses an inference which justifies the goal (if there are any − there may be no way of justifying the goal), and the adversary chooses one of the premises of that inference (if there are any − the inference may have been an axiom). We may think of the opponent as a ‘doubting’ Thomas.

We may think of a rule structure as representing an abstract non−deterministic program. The state of an executing program determines the set of instructions which are enabled in that state (there may be several ‘program counters’, pointing at several possible ‘instructions’, which may have guards as with semaphore operations). The computer (control unit, instruction scheduler, angel) picks one of these (if any) to be executed. This choice determines a set of possible next states, and the environment (execution unit, demon) picks one of these (if there are any to pick from). Then Φ^{∘}(X ) is the condition that the computer can pick an instruction from which there is no escape except in a state satisfying X . This is a closed−ness condition. Also Φ^{•}(X ) is the condition that whatever instruction the computer picks, the environment can pick a next state satisfying X − a kind of ‘ubiquity’ or density condition.

What is the weakest precondition operator (which sends a predicate X to the condition that the computer can not just avoid ∁X , but actually ensure X in the next state)? It is something close to the predicate transformer X ↦ Φ^{∘}(X ) ∩ Φ^{•}(X ), which equals X ↦ Φ^{∘}(X ) ∩ Φ^{•}(True). I have no real answer at the moment.

The predicate Φ^{∘}(False) (False and True are the predicates with constant values N_{0} and N_{1} respectively) means in programming terms that the computer can issue a command to which there is no response. This ‘aborts’ the computation, and surely the environment is supposed to avoid such hazardous states. It is a ‘bug’ in the environment: the system can ‘break’ the environment. In game terms, white can beat black; in inferential terms, the statement is directly provable. Φ^{∘}(False) is the complement of Φ^{•}(True), which means that black can respond to any command.

On the other hand, Φ^{•}(False) means in programming terms that the environment has terminated successfully, as there can be no further instructions. In game terms, black has beaten white. Φ^{•}(False) is the complement of Φ^{∘}(True), which means that white can move.

Note that there are (non−constructively) really three possibilities: white beats black, black beats white, or black wins without ever beating white. The constant endeavour of black is to avoid situations in which white can win, and to keep responding to instructions.

The intersection Φ^{•}(True) ∩ Φ^{∘}(True) means that the game is not yet won by either party. The intersection Φ^{•}(False) ∩ Φ^{∘}(False) is empty.

5.2 Winning

What exactly counts as a behaviour of the system in which Black wins? There is actually a nice pun here, which connects with the so−called ‘weakest invariant’ predicate transformer [Lamport, win and sin: predicate transformers for concurrency, ??]. This section had some brief remarks on the connection with Lamport’s approach to specification.

6 Programming with rule sets

The general message of this section is that all kinds of familiar program constructs are apparently reflected by rule sets.

6.1 Sequential composition

Suppose that:

Φ_{1}, Φ_{2} : S → Fam^{2}(S)
Φ_{1}  = λs. (R_{1}(s), λr. (P_{1}(s, r), λp. s[r/p]))
Φ_{2}  = λs. (R_{2}(s), λr. (P_{2}(s, r), λp. s[r/p]))

Then we can find Φ = Φ_{1} _{ ˆ∘} Φ_{2} : S → Fam^{2}(S) (a kind of sequential composition) such that

(Φ_{1} _{ ˆ∘} Φ_{2})^{∘} = (Φ_{1})^{∘} ^{∘} (Φ_{2})^{∘}

The required components of Φ are

R(s)  =^{Δ} (Φ_{1})^{∘}(R_{2}, s)
P(s, (r_{1}, λp_{1}. r_{2}(p_{1})))  =^{Δ} ( Σ p_{1} : P_{1}(s, r_{1}) ) P_{2}(s[r_{1}/p_{1}], r_{2}(p_{1}))
s[(r_{1}, λp_{1}. r_{2}(p_{1}))/(p_{1}, p_{2})] =^{Δ} s[r_{1}/p_{2}][r_{2}(p_{1})/p_{2}]

A dual construction _{ ˆ•} can be given, such that

(Φ_{1} _{ ˆ•} Φ_{2})^{•} = (Φ_{1})^{•} ^{∘} (Φ_{2})^{•}

In this case, the components of the rule structure^{•}−representing composition are as follows.

R(s)  =^{Δ} (Φ_{1})^{•}(R_{2}, s)
P(s, λr_{1}. (p_{1}(r_{1}), r_{2}(r_{1})))  =^{Δ} ( Σ r_{1} : R_{1}(s) ) P_{2}(s[r_{1}/p_{1}(r_{1})], r_{2}(r_{1}))
s[λr_{1}. (p_{1}(r_{1}), r_{2}(r_{1}))/(r_{1}, p_{2})] =^{Δ} s[r_{1}/p_{1}(r_{1})][r_{2}(r_{1})/p_{2}]

6.2 Alternative composition

The join or alternative composition Φ = (Φ_{1} ⊔Φ_{2}) of two rule structures over the same set S is defined as follows:

R  =^{Δ} R_{1} ∪ R_{2}
P(s, inl(r_{1})) =^{Δ} P_{1}(s, r), P(s, inr(r_{2})) =^{Δ} P_{2}(s, r_{2})
s[inl(r_{1})/p_{1}] =^{Δ} s[r_{1}/p_{1}], s[inr(r_{2})/p_{2}] =^{Δ} s[r_{2}/p_{2}]

In the gametheoretical metaphor, the player who goes first chooses in which of the two games the transition occurs. Clearly this binary construction can be generalised to take the join of a small family of rule structures. We have:

(Φ_{1} ⊔ Φ_{2})^{∘}(X ) = (Φ_{1})^{∘}(X ) ∪ (Φ_{2})^{∘}(X )
(Φ_{1} ⊔ Φ_{2})^{•}(X ) = (Φ_{1})^{•}(X ) ∩ (Φ_{2})^{•}(X )

Dually, we may consider a game built of two games, in which the player who goes first offers a choice of two moves to his opponent. Let us call this Φ = (Φ_{1} ⊓ Φ_{2}).

R  =^{Δ} R_{1} ∩ R_{2},
P(s, (r_{1}, r_{2}))  =^{Δ} P_{1}(s, r_{1}) + P(s, r_{2}),
s[(r_{1}, r_{2})/inl(p_{1})] =^{Δ} s[r_{1}/p_{1}],
s[(r_{1}, r_{2})/inr(p_{2})] =^{Δ} s[r_{2}/p_{2}]

Clearly this binary construction can be generalised to take the meet of a small family of rule structures. We have:

(Φ_{1} ⊓ Φ_{2})^{∘}(X ) = (Φ_{1})^{∘}(X ) ∩ (Φ_{2})^{∘}(X )
(Φ_{1} ⊓ Φ_{2})^{•}(X ) = (Φ_{1})^{•}(X ) ∪ (Φ_{2})^{•}(X )

6.3 Some basic rule structures

Refinement calculus. Ralph Back and von Wright [3].

6.3.1 Skip, update

As a representation of the identity predicate transformer, that is to say as a ‘no−op’ instruction (which should be a unit for sequential composition), we may take the following rule structure SKIP:

SKIP :  R(s) = N_{1},  P(s, n_{0}) = N_{1},  s[n_{0}/n_{0}] = s

We have SKIP^{∘}(X ) = X and SKIP^{•}(X ) = X .

More generally, if f : S → S is a state transformer then we can update the state deterministically.

UPDATE(f ) :  R(s) = N_{1},  P(s, n_{0}) = N_{1},  s[n_{0}/n_{0}] = f (s)

In particular SKIP = UPDATE(id).

6.3.2 Magic, assume

The magic command brings about the impossible. Unfortunately, it can never be issued.

MAGIC :  R(s) = N_{0}

Then MAGIC^{∘}(X ) = False, MAGIC^{•}(X ) = True.

More generally, for F a state predicate, we have the assumption command ASSUME(F ). This can be issued only when F holds.

ASSUME(F ) :  R(s) = F (s),  P(s, f ) = N_{1}  s[f /n_{0}] = s

Then

ASSUME(F )^{∘}(X , s) = F (s) × X (s)
ASSUME(F )^{•}(X , s) = F (s) → X (s)

In particular, MAGIC = ASSUME(False).

6.3.3 Abort, assert

The abort command can always be issued, but never executed.

ABORT :  R(s) = N_{1},  P(s, n_{0}) = N_{0}

We have ABORT^{∘}(X ) = True and ABORT^{•}(X ) = False.

More generally, for F a state predicate, we have the ‘assertion’ command ASSERT (F ). This can be executed (control will reach the next statement) only if F .

ASSERT (F ) :  R(s) = N_{1},  P(s, n_{0}) = F (s),  s[n_{0}/p] = s

Then

ASSERT (F )^{∘}(X , s) = F (s) → X (s)
ASSERT (F )^{•}(X , s) = F (s) × X (s)

In particular, ABORT = ASSERT (False).

6.3.4 Guarding

We can also consider ‘guarding’ a given rule structure. If G is a state predicate, let Φ = G → Φ′ where:

R  =^{Δ} G ∩ R′
P(s, (g, r)) =^{Δ} P′(s, r)
s[(g, r)/p] =^{Δ} s[r/p]

6.4 Other forms of composition

Sequential composition and union are homogeneous operators taking rule structures over a given state set S to a rule structure over the same set. Two other kinds of composition that are representable as operators on rule sets are simultaneous composition (in which the state set is the Cartesian product of the state sets of the component games, and transitions occur in all coordinates simultaneously), and interleaving composition (in which the states are finite multi−sets of states in the component games, and transitions occur in just one isolated component per cycle, leaving all others states in the multi−sets unchanged). Both these constructions alter the state space (by Cartesian products, and by multi−sets), so they are really constructions on rule sets, not just rule structures on a set. Note that the components do not communicate in any way.

Let us use two lines Φ_{1}∥Φ_{2} for simultaneous (synchronised?) composition and three Φ_{1}∥∥Φ_{2} for interleaving. For synchronising two rule sets, let (S, Φ) = (S_{1}, Φ_{1})∥(S_{2}, Φ_{2})

S  =^{Δ} S_{1} × S_{2}
R((s_{1}, s_{2}))  =^{Δ} R_{1}(s_{1}) × R_{2}(s_{2})
P((s_{1}, s_{2}), (r_{1}, r_{2}))  =^{Δ} P_{1}(s_{1}, r_{1}) × P_{2}(s_{2}, r_{2})
(s_{1}, s_{2})[(r_{1}, r_{2})/(p_{1}, p_{2})] =^{Δ} (s_{1}[r_{1}/p_{1}], s_{2}[r_{2}/p_{2}])

This binary operation has an extension to families.

For interleaving two rule sets, let (S, Φ) = (S_{1}, Φ_{1})∥∥(S_{2}, Φ_{2}).

S  =^{Δ} S_{1} × S_{2}
R((s_{1}, s_{2}))  =^{Δ} R_{1}(s_{1}) + R_{2}(s_{2})
P((s_{1}, s_{2}), inl(r_{1})) =^{Δ} P_{1}(s_{1}, r_{1})
P((s_{1}, s_{2}), inl(r_{2})) =^{Δ} P_{2}(s_{2}, r_{2})
(s_{1}, s_{2})[inl(r_{1})/p_{1}] =^{Δ} (s_{1}[r_{1}/p_{1}], s_{2})
(s_{1}, s_{2})[inr(r_{2})/p_{2}] =^{Δ} (s_{1}, s_{2}[r_{2}/p_{2}])

This binary operation can be extended to countable families of states. The cardinality restriction is necessary because we must have a decidable equality between the parameters to define the next state.

6.5 Representing closure

Given a monotone predicate transformer θ, we define its closure θ^{∗} inductively as follows:

θ^{∗}  : Pred(S) → Pred(S)
θ^{∗}(X ) =^{Δ} X ∪ θ(θ^{∗}(X ))

It can be checked that θ^{∗} is a closure operator, in the sense that X ⊆ θ^{∗}X and (θ^{∗})^{2}X ⊆ θ^{∗}X .

For any Φ, we can find Φ^{∘∘}, Φ^{••} such that:

\begin{aligned}(Φ^{∘∘})^{∘} & = & (Φ^{∘})^{∗} \\ (Φ^{••})^{∘} & = & (Φ^{•})^{∗} \end{aligned}

These are defined as follows.

Φ^{∘∘} : S → Fam^{2}(S)

R^{∘∘}  = (Φ^{∘})^{∗}(True)
P^{∘∘}(s, inl(n_{0}))  = N_{1}
P^{∘∘}(s, inr(r, λp. e(p)))  = ( Σ p : P(s, r) ) P^{∘∘}(s[r/p], e(p))
s[inl(n_{0})/n_{0}]  = s
s[inr(r, λp. e(p))/(p, ps)] = s[r/p][e(p)/ps]

Φ^{••} : S → Fam^{2}(S)

R^{••}  = (Φ^{•})^{∗}(True)
P^{••}(s, inl(n_{0}))  = N_{1}
P^{••}(s, inr(λr. (p(r), m(r)))) = ( Σ r : R(s) ) P^{••}(s[r/p(r)], m(r))
s[inl(n_{0})/n_{0}]  = s
s[inr(λr. (p(r), m(r)))/(r, rs)] = s[r/p(r)][m(r)/rs]

7 Relation transformers

Any rule structure Φ on a set S determines a pair of operators on S → Pred(S) (≃ Pred(S^{2}), the type of binary relations on S) which I write Φ^{•∘}, Φ^{∘•}. The definitions are as follows:

Φ^{•∘}, Φ^{∘•}  : (S → Pred(S)) → S → Pred(S)
Φ^{•∘}(X , s_{a}) =^{Δ} ⋃_{r:R(s_{a})}(Φ^{••})^{∘}(⋂_{p:P(s_{a},r)} X (s_{a}[r/p]))
Φ^{∘•}(X , s_{a}) =^{Δ} ⋂_{r:R(s_{a})}(Φ^{∘∘})^{∘}(⋃_{p:P(s_{a},r)} X (s_{a}[r/p]))

It is obvious that both relation transformers Φ^{•∘} and Φ^{∘•} determined by a rule structure Φ are monotone, as the input relation occurs only positively in their defining expressions.

8 Implementations and bugs

The predicament of a programmer is usually as follows: she has to write a program (a collection of procedures) to present at inferface A a certain abstract behaviour, using only lower level resources made available at interface C by the efforts of other programmers. The ‘added value’ she provides is a certain increase in abstraction. How can it be modelled mathematically?

In the setting of rule sets, we need a relation s_{a} ⪯ s_{c} (s_{a} is within s_{c}) between the states of a rule system. (There could actually be two rule sets; this does not seem especially interesting.) The work of the programmer results in something that ‘lives’ in this relation. A proof that s_{a} ⪯ s_{c} can be thought of as an implementation of the abstract state s_{a} using the concrete state s_{c}. The relation should be the greatest solution of

s_{a} ⪯ s_{c} = ( ∏ r : R(s_{a}) ) ( Σ d : R^{∘∘}(s_{c}) ) ( ∏ b : P^{∘∘}(s_{c}, d) ) ( Σ p : P(s_{a}, r) ) s_{a}[r/p] ⪯ s_{c}[d/b]

Let us suppose we know how to define this. In general, an element of a set s_{a} ⪯ s_{c}, which we may tendentiously call a morphism, has the form

λr. (d(r), λb. (p(r, b), m(r, b)))

where

d : R(s_{a}) → R^{∘∘}(s_{c})
p : ( ∏ r : R(s_{a}) ) P^{∘∘}(s_{c}, d(r)) → P(s_{a}, r)
m : ( ∏ r : R(s_{a}), b : P^{∘∘}(s_{c}, d(r)) ) s_{a}[r/p(r, b)] ⪯ s_{c}[d(r)/b]

There are natural (copycat) unit morphisms 1_{α} = λr. (r, λb. (b, 1_{α[r/b]})), and a straightforward composition operation. So at any rate ⪯ is a pre−order. If we put a suitable equivalence relation on the sets s_{a} ⪯ s_{c}, then I presume we get a category in which the objects are states, and the morphisms are implementations of one state, using another. (Perhaps there is an interesting pre−order on the Hom sets? After all, one program can be better than another, in various ways.)

A problem with the relation s_{a} ⪯ s_{c} describing morphisms between states in a rule structure is whether it is well defined. It seems we need to use greatest fixed points. (If we used least fixed points, then the morphisms would only be strategies for beating ∘ on s_{a} or • on s_{c}.) It is not clear in general how to treat coinduction in type theory. Some ideas.

• Work instead with the complement of s_{a} ⪯ s_{c}, which can be inductively defined as a least fixed point. The classical notion of equality is ‘negative’ – you can not tell the equal things apart. From a constructive perspective positive relations often turn out to be more important. In this case it is presumably a difference relation.

• Characterise a morphism in s_{a} ⪯ s_{c} as (oh, I don’t know …) a function from Φ^{∘∘}(False, s_{a}) to Φ^{∘∘}(False, s_{c}). (We can be ‘busted’ by a only when we can go and bust c.) [This will not work as it stands. That is just a necessary condition. ]

• Use the least solution, but extending a given relation. That gives us an operator on relations. Do something with this ….

• See Lars Hallnäs (?Maximal bisimulation?), Ingrid Lindström A construction of non−well−founded sets in Martin−Löf type theory. What about the relation ⋂_{n} ⪯_{n}?

s_{a} ⪯_{0} s_{c}  =^{Δ} N_{1}
s_{a} ⪯_{n+1} s_{c}  =^{Δ} ( ∏ c : C (s_{a}) ) (Φ^{∘∘})^{∘}({ s : S | ( Σ r : R(s_{a}, c) ) s_{a}[c/r] ⪯_{n} s }, s_{c})

8.1 Bugs

Dual to the category of implementations, we have a structure (which may perhaps be called an anti−category?) of bugs, meaning things a tester can do which will inevitably cause an alleged implementation to ‘hang’. The relation s_{a} ≻ s_{c} (s_{a} is beyond s_{c}) is the least solution of

s_{a} ≻ s_{c} = ( Σ r : R(s_{a}) ) ( ∏ d : R^{∘∘}(s_{c}) ) ( Σ b : P^{∘∘}(s_{c}, d) ) ( ∏ p : P(s_{a}, r) ) s_{a}[r/p] ≻ s_{c}[d/b]

In general, an element of a set s_{a} ≻ s_{c} has the form

(r, λd. (b(d), λp. e(d, p)))

where

r : R(s_{a})
b : ( ∏ r′ : R^{∘∘}(s_{c}) ) P(s_{c}, r′)
e : ( ∏ r′ : R^{∘∘}(s_{c}), p : P(s_{a}, r) ) s_{a}[r/p] ≻ s_{c}[r′/b(r′)]

9 The mother of all closure operations

A natural number can encode a pair consisting of a natural number and a finite set of natural numbers, which is to say a finitary inference in which the statements are represented by natural numbers. This is the basis of the model P(ω) for the untyped λ calculus: each set of natural numbers represents a set of finitary inferences, which in turn represents a continuous predicate transformer, or operator on sets of natural numbers. (We can of course restrict the sets used in the model to be recursively enumerable.) The operation ‘^{∗}’ which maps a (so represented) rule set to (the representation of) its closure, can itself be represented by a set of natural numbers, and moreover one which is its own closure. The fixed points of this representable closure operation are precisely the (representatives of) closure operations.

This suggests to me the doubtless at least partly confused idea that under certain ‘regularity’ conditions on the set of states (enjoyed by the set of natural numbers), the operator which maps a rule structure over those states to its closure may be represented as a family of states. This would be the mother of all closure operations over that set of states, in somewhat the sense that a universal Turing machine can be called the mother of all Turing machines. (The rule structures probably have to satisfy some condition akin to ‘finitary’, meaning that the sets involved must live in a restricted universe. Perhaps this is really admissible sets.) The following definitions are towards a suitable state space.

If A : Set, B : A → Set is a family of sets which is closed under the ( Σ ) quantifier and other amenities, and G is a set, define the set of iterated sequents over G to be the data type

S = G + S × ( Σ a : A ) S^{B(a)}
≅ G × ( Σ a : A ) S^{B(a)}
≅ ( Σ a : A ) S^{B(a)+1}

So an element of S is either of ground form, or a pair consisting of a sequent (the conclusion) and an (A, B)−family of sequents (the hypotheses). (It loses no generality to take the conclusion always of ground form.)

Given an equivalence relation ∼_{G} on G, we extend it to an equivalence relation on sequents ∼_{S} inductively as follows:

(g_{1}, (a_{1}, p_{1})) ∼_{S} (g_{2}, (a_{2}, p_{2}))

= (g_{1} ∼_{G} g_{2}) \begin{matrix}×( ∏ h_{1} : B(a_{1}) ) ( Σ h_{2} : H (a_{2}) ) p_{1}(h_{1}) ∼_{S} p_{2}(h_{2}) \\ ×( ∏ h_{2} : B(a_{2}) ) ( Σ h_{1} : H (a_{1}) ) p_{1}(h_{1}) ∼_{S} p_{2}(h_{2}) \end{matrix}

This is the natural analogue of Aczel’s extensional equality on ‘tree sets’. It seems necessary to have some such relation so as to able to make predicates out of families.

Another interesting relation in the vicinity is

(g_{1}, (a_{1}, p_{1})) ≤_{S} (g_{2}, (a_{2}, p_{2}))
= g_{1} ≤_{R} g_{2} ×( ∏ h_{2} : B(a_{2}) ) ( Σ h_{1} : B(a_{1}) ) p_{2}(h_{2}) ≤_{S} p_{1}(h_{1})

This extends a relation ≤_{G} on G between ground formulae to sequents, in a manner consonant with some idea of the ‘strength’ of a sequent.

10 General perspective on rule sets

A rule set (inferential system/interactive system) is an object of the type:

( Σ S : Set ) S →
( Σ R : Set ) R →
( Σ P : Set ) P → S

From a categorical point of view, it is a coalgebra for Fam^{2}.

It is natural to call the following the type of transition systems.

( Σ S : Set ) S →
( Σ T : Set ) T → S

A transition system is a coalgebra for Fam. (In Aczel’s ‘Non−well−founded sets’ [2] Ch7, they are called simply ‘systems’.)

Simplifying even further, it is natural to call the following the type of dynamical systems.

( Σ S : Set ) S → S

A dynamical system is a coalgebra for 1 = Fam^{0}.

This is indeed a ‘holy trinity’ of structures of extreme interest in computer science. See P. Gardiner, C. Martin, and O. de Moor, An Algebraic Construction of Predicate Transformers, 1993 online at

http://www.comlab.ox.ac.uk/oucl/publications/books/algebra/papers/newalg.ps.gz

In one direction, from dynamic systems to inference systems, the idea is that just as one can represent a relation R on a set S as an equivalence class of pairs of functions to that set (one such consists of the projections from the graph of the relation), so by an analogous construction one can represent a monotone predicate transformer on a set by an equivalence class of pairs of relations on that set. The construction has much in common with the usual representation of an integer as an equivalence class of ordered pairs of natural numbers, or of a rational as an equivalence class of certain ordered pairs of integers. One representation of a predicate transformer by a pair of relations uses one relation (a partial equivalence relation) as a precondition and the other as a next−state relation. It is odd how there is, as it were, a south pole and a north pole.

Conversely, just as a function can be thought of as a relation which is total and single valued, so a relation can be thought of as a predicate transformer which satisfies analogous properties. These properties however mention the inclusion order on the Hom sets of the category of sets and relations.

The hierarchy does not extend any further than predicate transformers, because the category of sets and predicate transformers between them lacks ‘pullovers’. A pullover is an order−enriched isotope of a pullback, necessary for defining composition between morphisms represented by spans.

None of this seems to work constructively, at least not exactly, and certainly not without assuming equality relations everywhere. But a transition system represents a certain kind of ‘asymmetrical’ or ‘directed’ relation, modulo equivalence of states. Moreover a rule set represents a ‘dipole’ pair of predicate transformers ^{∘} and ^{•}. So the exact arrangement of these things is quite interesting, or at least obscure.

11 Related notions

The notion of rule set is that of a set of abstract (featureless, structureless) statements, and a set of (possibly infinitary) first order inferences. (First order means that there are no inferences which discharge assumptions.) A rule is really a form of inference; that is a template to generate or to be matched against purported inferences. To analyse rules as opposed to merely the inferences that are their instances, one needs some structure on the statements (for example, first order terms), so as to be able to model substitution instances of rules. This seems quite feasible, though necessarily intricate. Other directions of generalisation include (perhaps) accommodating variable binding and discharge of assumptions, as well as notions of context dependency.

References

[1] P. Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739–782. North−Holland, Amsterdam, 1977.

[2] P. Aczel. Non−well−founded sets. CSLI lecture notes, no. 14, Stanford, 1988.

[3] R−J. Back and J. von Wright. Refinement Calculus. Springer−Verlag, 1998.

[4] P. Dybjer. A general formulation of simultaneous inductive−recursive definitions in type theory. JSL, 1997.