{-
\begin{verbatim} Time-stamp: "1999-02-09 18:45:14 peter" \end{verbatim}
Make the checker load certain scripts in other files.
\begin{verbatim} #include "./standard.half" #include "./Boole.half" #include "./world.half" \end{verbatim}
\tableofcontents
-}
{-
\section{Introduction} Notes on inductive definitions. (Petersonn-Synek trees.)
\newcommand{\defocc}[1]{\framebox{\emph{#1}}} % Defining occurrence \newcommand{\power}[1]{\ensuremath{\mathcal{P}(#1)}}
What is an inductive definition? In a sense, this is one of those questions like `what is a set?' which \textit{a priori} has no complete answer. One can try to answer with some kind of fable about building things up from below, or one can try to give a technical answer. In both cases, one has I think to be content with failure. But there are degrees and kinds of failure.
What gets defined? The answer to even this question isn't straightforward. Peter Aczel's chapter of the `Handbook of Mathematical Logic' gives a marvellously clear account of inductive definitions of \emph{subsets of a base set}, from the standpoint of standard set theory. By the time it gets to inductive definitions, standard set theory (a fabulous creature if ever there was one) has put away all or most the poetical apparatus that it used to somehow persuade you that you know what a set is. By the time it gets to inductive definitions, predicative type theory hasn't really got going at all, because the notion of `set' is intimately related to, and in some sense maybe even identical with the notion of `inductive definition'. I am especially interested in getting a very clear view of how things fit together conceptually in the predicative story.
So to speak, the inductive definitions of predicative type theory are `in thin air'. They don't just define subsets of base sets: they define the base sets themselves, and all types (and kinds) of other thing. Then there are inductive-recursive definitions (where a set is defined inductively, simultaneously with a function defined by structural recursion over that set), and even wilder things. Among these, inductive definitions which define subsets of a base set are comparatively easy to understand. Let us think about these.
In the following, by `inductive definition' I mean `inductive definition of a subset of a given base set'. I take `subset' in the sense of propositional function, and so by the Curry-Howard correspondence, an inductive definition can also be thought of as a definition of a family of sets defined on a given base set, the whole family being defined simultaneously.
A particularly large and interesting class of inductive definitions consists of those in `sum of products form'. (It means we have a monotone inductive definition, and I don't understand non-monotone definitions at all.)
By `sum of products form', I mean that the inductive definition is given by a function from subsets to subsets which can be expressed in terms of a `Sigma Pi' combination of quantifiers -- c.f. disjunctive normal form in the propositional calculus. The function defines a subset, uniquely -- the least fixed point of the function. That it is the least fixed point, means that we have an initial algebra for the functor, to put it categorically, or can do `structural recursion' to put it more vaguely. Sorry for the poor explanation but the code may be clearer.
Why do we have a least fixed point? Is there a predicative argument? It seems to be part, if not parcel of what it means to be a set, that you have things `in' it called `elements', and if you have two expressions for elements, you can decide a priori whether they are equivalent expressions, for `the same' element. If they differ in value, then there must be some inspectable difference -- that is to say, the expressions must be for values which are built up `from below'. (The argument is vanishingly weak here.) Blah blah blah so we can do structural recursion, which is what one means by having a `least fixed point', where operators on the type of propositional functions of a base set are concerned.
Rule sets... to use `replacement-notation'. \[ \{ \, \{ \, \frac{ \{ \, d(a,b,c) \, | \, c \in C(a,b) \, \} } { a } \, | \, b \in B(a) \, \} \, | \, a \in A \, \} \]
-}
ID = {- a theory of sum-of-products inductive definitions -}
let
{ {- local definitions -}
{-
\section{Closure operations} \label{sec:closureOps}
If we have an operation on the large type of sets, or of predicates over a base set, or of worlds (families of sets), then we can form an operation extending it which closes up its argument under the given operation.
So we have a variety of level 2 functionals. What is the most general form?
-}
ClosureSet
= {- set closed under Phi -}
\ Phi X ->
data { $Ur ( x : X )
, $Gen ( p : Phi (ClosureSet Phi X) ) }
: OP (OP Set) {- = OP (Pow Set) -}
, {- simultaneous definition of a family on a given set -}
ClosurePow( S : Set )
= \ Phi X s ->
data { $Ur ( x : X s)
, $Gen ( p : Phi (ClosurePow S Phi X) s) }
: OP (OP (Pow S))
, {- simultaneous definition of a family with its domain -}
ClosureFam
= \ Phi X ->
let { A = X.I : Set
, B = X.g : Pow A
, UT = struct {
I=data { $ground ( a : A )
, $gen ( p : (Phi (ClosureFam Phi UT)).I ) },
g=\i->case i of {
$ground a -> B a,
$gen p -> (Phi (ClosureFam Phi UT)).g p}}
: Fam Set
}
in UT
: OP (OP (Fam Set))
,
{-
\section{Sums of products}
An inductive definition of a subset of a set $S$ is given by an operator $\Phi$ on the powerset of $S$: \textit{i.e.} $\Phi(X)\subseteq S$ for $X\subseteq S$. An operator on the powerset is much the same thing as a function which assigns to an element $s$ of the set the subset of the powerset consisting of $X \subseteq S$ such that $s \in \Phi(X)$. If we take `subset' in the sense of `indexed family', then the following definition gives a possible analysis, as a type operator, of inductive definitions on a set.
-}
T ( S : Type )
= ( s : S )-> Fam (Fam S)
: Type
,
Tofficial
= sig { S : Set, phi : T S }
: Type
,
Talt1 ( A : Type )
= sig { B : Pow A
, C : ( s : A )-> Pow (B s)
, d : ( s : A, b : B s, c : C s b )-> A
}
: Type
,
Talt
= sig { A : Set
, B : Pow A
, C : ( s : A )-> Pow (B s)
, d : ( s : A, b : B s, c : C s b )-> A
}
: Type
,
UNPACK
( S : Type, phi : T S )
= struct
{ B = \ s -> (phi s).I
, C = \ s b -> ((phi s).g b).I
, d = \ s b c -> ((phi s).g b).g c
}
: Talt1 S
,
{-
Having split an inductive definition into its components, we can put them back together again.
-}
PACK ( A : Type
, B : Pow A
, C : ( a : A) -> Pow (B a )
, d : ( a : A, b : B a, c : C a b )-> A
) = \s->
struct { I = B s
, g = \ i ->
struct { I = C s i, g = d s i }
}
: T A
{-
\section{Client server}
-}
,
{-
The following definitions concern these unpacked
components. They introduce two families of tree-sets.
In the first, called \texttt{Client},
a tree node contains an element of a \texttt{C}, and the branches
from the node are labelled by elements of the corresponding \texttt{R} set. In the
other kind of tree, called \texttt{Server}, a node contains a function mapping a
\texttt{C} to a corresponding \texttt{R}, and the branches are labelled by
\texttt{C}. The trees are also allowed to have leaves, provided a
certain property holds.
The names used here for variables come from the interpretation of the data as a Command-Response protocol, in which \texttt{S} is a set of states, \texttt{C} gives the set of commands legal in state \texttt{s}, \texttt{R} the set of responses that can be made per command, and \texttt{n} gives the next-state of the protocol. Then elements of a set \texttt{Client s} are programs for the command side of the protocol. The programs run to a voluntary exit, or force the responder to stop, by issueing a command to which there is no legal response. Elements of a set \texttt{Server} are programs for the responder, or state machines. They run to a voluntary exit, or force the command side to stop, in a state in which no command is legal.
-}
guts
( S : Type {- State -}
, C : Pow S {- Commands per state-}
, R : ( s : S )-> Pow ( C s ) {- Responses per command per state -}
, n : ( s : S, c : C s, r : R s c )-> S {- next state function -}
) = theory
{
IO
= \ X s ->Sigma (C s) (\c->Pi (R s c) (\r->X (n s c r)))
: OP (Pow S )
,
OI
= \ X s ->Pi (C s) (\c->Sigma (R s c) (\r->X (n s c r)))
: OP (Pow S )
,
Close
{- cf: the closure operations above -}
{- (Section \ref{sec:closureOps} on page \pageref{sec:closureOps}). -}
= \ Phi X s ->
data
{
$Escape ( x : X s )
,
$Step ( p : Phi (Close Phi X) s )
}
: OP (OP (Pow S))
,
Client ( X : Pow S )
= {- predicate of states that they are Client-safe for X -}
{- This means there-s a client program for which -}
{- all non-terminating interactions reach X -}
\ s ->
data
{
$Escape ( x : X s ) {- Predicate has to hold -}
,
$Call ( c : C s {- Essentially IO (Client X) -}
, resume
: ( r : R s c
)-> Client X (n s c r)
)
}
: Pow S
,
Server ( X : Pow S )
= {- predicate of states that they are Server-safe for X -}
\ s ->
data
{
$Escape ( x : X s )
,
$Respond ( resp : ( c : C s )-> R s c
, next : ( c : C s )-> Server X (n s c (resp c))
) {- cf the classical definition of state machine -}
}
: Pow S
, {- some neater variants. Need merging -}
Client' ( X : Pow S )
= Close IO X
: Pow S
,
Server' ( X : Pow S )
= Close OI X
: Pow S
, {- now chain-sets: i.e. sets of paths in the different kinds of tree -}
ResponseTrace
( X : Pow S
, s : S
)
= {- predicate of clients that a some chain of responses -}
{- can lead to X from state s -}
\ cl ->
case cl of
{
$Escape x
-> data
{ $nil }
,
$Call c fork {- could use IO here -}
-> data
{ $cons ( r :R s c
, rs :ResponseTrace X (n s c r) (fork r)
)
}
}
: Pow (Client X s)
,
CallTrace
( X : Pow S
, s : S
)
= {- predicate of servers that some chain of calls can lead to X from state s -}
\ sv ->
case sv of
{
$Escape x
-> data { $nil }
,
$Respond resp next
-> data
{ $cons ( c : C s
, cs : CallTrace X (n s c (resp c)) (next c)
)
}
}
: Pow (Server X s)
,
ClientYield
( X : Pow S
, s : S
, cl : Client X s
, rt : ResponseTrace X s cl
)
= {- final state -}
case cl of
{ $Escape x
-> case rt of { $nil -> s }
, $Call c resum
-> case rt of
{ $cons r rs -> ClientYield X (n s c r) (resum r) rs }
}
: S
,
ServerYield
( X : Pow S
, s : S
, sv : Server X s
, ct : CallTrace X s sv
)
= {- -}
case sv of
{ $Escape x
-> case ct of { $nil -> s }
, $Respond resp next
-> case ct of
{ $cons c cs -> ServerYield X (n s c (resp c)) (next c) cs }
}
: S
}
: Theory
{-
\section{Closure and kernel}
-}
,
{-
An inductive definition has a closure (also called its
`derivative'). Intuitively, it gives the least subset of \texttt{S}
including a given subset which is closed under the operator.
-}
CL ( S : Type )
= \ phi ->
let
{ X = UNPACK S phi : Talt1 S
, Y = guts S X.B X.C X.d : Theory
, E = \a->data{} : Pow S
} in PACK S
(\a->Y.Client E a)
(\a b->Y.ResponseTrace E a b)
(\a b c->Y.ClientYield E a b c)
: OP (T S)
,
{-
I believe the following operator, which is in some sense dual to the closure of an inductive definition, is called the kernel.
-}
KRN ( A : Type )
= \ phi ->
let
{ X = UNPACK A phi : Talt1 A
, Y = guts A X.B X.C X.d : Theory
, E = \ s -> data {} : Pow A
} in
PACK A
(\a->Y.Server E a)
(\a b->Y.CallTrace E a b)
(\a b c->Y.ServerYield E a b c)
: OP (T A)
} in
theory
{ {- nothing exported yet -}
}
: Theory