[Prev][Next][Index][Thread]

Re: A FIXPOINT THEOREM IN LINEAR LOGIC

Date: Thu, 6 Feb 92 08:19:09 PST
To: linear@cs.stanford.edu

			PORTABLE INDUCTION

			  Vaughan Pratt

A portable program (concept) is one that maximizes the number of
systems it can be run on (interpreted for) by minimizing the number of
system properties it depends on.  The following can be understood as
asking for a port of induction to a certain system.

	Date: Wed, 5 Feb 92 14:51:20 +0100
	From: Jean-Yves Girard <Jean-Yves.Girard@inria.fr>

	4.2. in typed lambda-calculi

	under specific positivity assumptions, one can add to the
	fixpoint the strongest requirement "smallest fixpoint" ; LU
	seems the right formalism to do this. Observe that we would get
	both primitive recursion and one step predecessor. Observe too
	that all "petty" axioms are now logically provable that all
	partial functions can be defined... hence the major problem is
	the following : CAN WE ALSO MAKE A MAJOR PROGRESS ON INDUCTION?

I understand induction as an abstraction better than I understand the
target of this particular port.  With some luck the abstract properties
of induction described below will prove useful in the above port, but
this will have to be determined by someone else.

In "Was Sind und Was Sollen Die Zahlen" (The nature and meaning of
numbers) [Ded88] Dedekind in 1888 defines a *simply infinite* set to be
a set N with a distinguished element 1 for which there exists an
injective function f with domain N and range a subset of N-{1} such
that N is the "f-chain" of 1, defined as the intersection of all
subsets A of N closed under f (f(A) < A) and containing 1.  He then
shows that all simply infinite sets are isomorphic, and infers that any
simply infinite set can be taken as constituting the positive
integers.

Dedekind's definition admits of two orthogonal improvements.  One,
found by Peano in 1889 [Pea89], is to strip out the notion of chain
thereby reducing the notion of number to its now familiar first-order
formulation.  The other, found by Schroeder in 1895 [Sch95], is to
strip out the notion of number and generalize the notion of chain to
the notion of reflexive transitive closure of any binary relation
(Dedekind defined "chain" only for functions).

Peano's definition of number has all the advantages of first order
logic over second.  Schroeder's definition of reflexive transitive
closure has the same advantages when we treat relations as
individuals.

But whereas Peano's definition of number has the distinct drawback of
not uniquely determining the natural numbers, Schroeder's definition of
the reflexive transitive closure a* of a as the least reflexive
transitive relation including a *does* uniquely determine reflexive
transitive closure, as a corollary of the simple fact that the least
element of a subset of a poset is uniquely determined.

A small matter of logical framework remains.  What is the minimal
framework in which the minimality of a* can be expressed?

Universal Horn logic suffices: we may define a* to satisfy 1 < a*,
a*;a* < a*, a < a*, and the "Horn induction" rule

	1 < b & b;b < b & a < b ==> a* < b              (HI)

(where 1 is now the unit satisfying a;1 = a = 1;a, not the integer 1).
Here 1 < b and b;b < b assert respectively the reflexivity and
transitivity of b.  Hence HI asserts that a* is least among all
reflexive transitive extensions of a.

But is Horn logic necessary?  A Horn clause seems more like a rule of
inference than an axiom.  Is there perhaps an equational or
inequational equivalent of HI?  Indeed there is, for which it suffices
to admit a suitable antimonotone operation into the language.  Here are
two rather different ways of going about this.

============================

1.  Define a *subtractive monoid* to be an algebra (A, +, 0, -, ;, 1)
such that (A, +, 0) is a unital semilattice, (A, ;, 1) is a monoid with
a;b monotone in a and b (with respect to the semilattice order---this
can be expressed equationally as a;b < (a+a');(b+b')), a;0 = 0, and
a-(a+b) = 0.  (We read a<b as synonymous with a+b=b.  Subtraction can
be defined "on the nose" if preferred, via a<b+c iff a-b < c, making
(A,+,0,-,;,1) a *coHeyting monoid*.)

Induction in a subtractive monoid can be expressed as:

	a*;b < b + a*;(a;b - b)			(1)

Theorem.  Horn induction holds in any subtractive monoid.

Proof.  Suppose (i) 1 < b, (ii) b;b < b, and (iii) a < b, the premises
of Horn induction.  Then a* < a*;b by (i) and monotonicity of a;b in
b.  Also a;b < b;b (by (iii) and monotonicity of a;b in a) < b (by
(ii)), whence a;b - b = 0.  Hence a* < a*;b < b + a*;(a;b - b) = b +
a*;0 = b + 0 = b, so a* < b, the conclusion of Horn induction.  QED

This equational axiomatization of transitive closure is based on
Segerberg induction for propositional dynamic logic, 1977.  As it
stands it can be read as saying that if after some number of a's b
holds, then either b holds now or after some number of a's b is still
false but will hold after one more a.  Or, taking its contrapositive,
writing -(a*;-b) as [a*]b, replacing -b by p, writing a-b as -(-b ->
-a), and assuming double negation, --p = p, we obtain

	p & [a*](p -> [a]p) < [a*]p

This is recognizable as Segerberg induction: if p is true and no matter
how long a runs p is preserved by one more step of a, then no matter
how long a runs p will remain true.

============================

2.  Define a *residuated poset* to be a structure (A, <, ;, 1, ->) such
that (A, <) is a poset, (A, ;, 1) is a monoid with a;b monotone in a
and b, a->b is monotone in b, and a;(a->b) < b < a->(a;b) (defined this
way to make all axioms (in)equations).  In 1977 (the same year that
Segerberg gave his induction axiom), in the setting of relation
algebras (a much smaller class than residuated posets), Tarski and Ng
[NT77] gave what amounts to the following inequality based on
residuation a->b.

	(a->a)* < a->a				(2)
	a* is monotone in a			(3)

Theorem.  Horn induction holds in any residuated poset.

Proof.  Suppose (i) 1 < b, (ii) b;b < b, and (iii) a < b.  Then b <
b->b (by (ii)), so b* < (b->b)* (by (3)) < b->b (by (2)).  Also a* < b*
by (iii) and (3), whence a* < b->b, so b;a* < b.  But a* < b;a* by (i),
so a* < b.  QED

There remains the question of how to express equationally the
monotonicity of a;b in a and b, a->b in b, and a* in a.  This can be
solved in the obvious way by taking the poset to be a semilattice;
e.g.  a* < (a+a')* expresses monotonicity of *.  In addition all
inequalities a<b can then be translated to equations a+b = b.

By "Currying" (2) to a;(a->a)* < a we obtain something looking more
like Peano induction, provided we read the first a as the basis, a->a
as the inductive step, * as a sort of universal quantifier, and the
last a as what was to be proved by induction.

Tarski-Ng induction is a "purer" form of induction than Segerberg
induction in that it only requires one variable!

It is interesting that (1) is strong enough to entail monotonicity of *
on its own (since Horn induction easily implies monotonicity of *, just
set b to (a+a')*) while (2) is not.

These ideas are developed in more detail in [Pr90].


While I don't know whether any of this is helpful in answering
Jean-Yves' question, I do think the combination of these two equational
induction axioms gets closer to the abstract heart of induction than
any previous account of induction.  In particular the two together show
that equationally defined induction is a robust notion that is not
terribly fussy about just where it gets its antimonotonicity from.

	Vaughan Pratt

	@Book(
Ded88,	Author="Dedekind, R.",
	Title="Essays on the Theory of Numbers",
	Note="Translation by W.W. Beman of {\it {S}tetigkeit und
	irrationale {Z}ahlen} (1872) and {\it {W}as sind und was sollen die
	{Z}ahlen?} (1888), reprinted 1963 by Dover Press",
	Publisher="Open Court Publishing Company", Year=1901)

	@Article(
NT77,	Author="Ng, K.C. and Tarski, A.",
	Title="Relation algebras with transitive closure,
		{A}bstract 742-02-09",
	Journal="Notices Amer. Math. Soc.", Volume=24, Pages="A29-A30",
	Year=1977)

	@PhDThesis(
Ng84,	Author="Ng, K.C.",
	Title="Relation Algebras with Transitive Closure",
	School="University of California, Berkeley",
	Note="157+iv pp.", Year=1984)

	@Book(
Pea89,	Author="Peano, G.",
	Title="Arithmetices Principia, Nova Methodo exposita",
	Address="Turin", Year=1889)

	@InProceedings(
Pr90,	Author="Pratt, V.R.",
	Title="Action Logic and Pure Induction",
	Booktitle="Logics in AI: European Workshop JELIA '90, LNCS 478",
	Editor="J. van Eijck", Publisher="Springer-Verlag", Pages="97-120",
	Address="Amsterdam, NL", Month=Sep, Year=1990)

	(Available as boole.stanford.edu:/pub/jelia.{tex,dvi})

	@Book(
Sch95,	Author="Schr{\"o}der, E.",
	Title="Vorlesungen {\"u}ber die {A}lgebra der {L}ogik ({E}xakte
	{L}ogik).  {D}ritter {B}and: {A}lgebra und {L}ogik der
	{R}elative", Publisher="B.G. Teubner", Address="Leipzig", Year=1895)