{-
\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