|
Properties of Coinductive
Proof Nets Laura Korte Laboratory for Foundations of Computer
Science Abstract Even though in recent years, research has
shifted away from GOFAI, both the strong historic link between symbolic logic
and Artificial Intelligence, and the contribution of the first to the latter,
is undeniable. Of course there are many aspects of the original classical
logic which make it unsuitable to model human reasoning, but many other, more
appropriate logics have been introduced since then. In my MSc Thesis [4], I
propose to introduce a new system of coinductive proof
nets, which solves two of the most striking shortcomings of classical
logic: the inability to reason with limited resources and the inability to
reason with infinite objects. This article describes the properties of the
new system and outlines some of their proofs. Full proofs can be found in my
MSc Thesis [4] which was supervised by Dr. Vincent van Oostrom. Introduction Coinductive proof nets are created by
specifying a coinductive
definition of proof nets. This is
in analogy with Joachimski’s coinductive
λ-calculus in [3], which specifies a coinductive
definition of the λ-calculus. Joachimski’s
work on the coinductive λ-calculus, in
combination with the existence of a correspondence between the
λ-calculus and proof nets, also provides the major incentive to
investigate a coinductive version of proof nets: if
there exists an infinite version of the
λ-calculus, it is worth specifying and investigating the properties of
an infinite version of proof nets as well. The result of such an
investigation could help us determine the relevance of both coinductive proof nets and the coinductive
λ-calculus. However,
the motivation for our research on coinductive
proof nets is not solely theoretical. Practical application of the
λ-calculus like functional programming and natural language processing
are well-known throughout the AI community, and because of the correspondence
between the (coinductive) λ-calculus and (coinductive) proof nets, each practical application of
the former, presents the latter with a potential application as well.
Furthermore, the aforementioned relation between proof nets and λ-terms
is one of implementation: each λ-term can be represented by a proof net.
Only proof nets present us with a more efficient way of reduction than the
λ-calculus does, and it has the advantage of proof identification. That
is, there is more than one way to reduce a λ-term to its normal form, yet
no way to either identify or distinguish between these reduction sequences.
Proof nets on the other hand supply us with only one proof for all reduction
sequences that are equal modulo the order in which the individual reductions
were applied. We can therefore draw the conclusion that the λ-calculus
does not only give us many possible practical applications for coinductive proof nets, but also that most of these
applications could potentially benefit from the introduction of coinductive proof nets. Coinductive Proof Nets As
mentioned before, coinductive proof nets are
created by specifying a coinductive definition of
proof nets. This description is composed of two important parts: coinductive definition and proof nets, each of which we will discuss in turn. Research on coinduction is a relatively new research area, but its
dual induction is much more wide
spread. However, the reason for using a coinductive
definition instead of an inductive one, is that the
former is restricted to finite objects, whereas the latter has the ability to
define infinite ones as well. The reader is referred to [2] for more
information about coinduction, coalgebras
and coinductive definitions. |
||
|
The
second part in the description of coinductive proof
nets is proof nets. The logic for
proof nets, linear logic, was first
defined by Girard in [1] and its most important
feature is resource sensitivity. Because of the correspondence between the
λ-calculus and proof nets, every λ-term can be portrayed by a proof
net. Figure 1 shows the proof net of a λ-term with an infinite reduction
sequence: (λx.xx)(λx.xx). To
determine the relevance of coinductive proof nets
and the coinductive λ-calculus, we would like
the coinductive proof nets to have some reduction
properties which prevent them from disruptive non-determinism and possibly
even from infinite reduction sequences. A formal definition of these
properties can be found in [5] and below: |
Figure 1: Proof net of (λx.xx)(λx.xx) |
|
|
Confluence: a Î A is confluent
if "b,c Î A (c *¬ a ®* b) Ş $d Î A (c ®* d *¬ b) The
rewrite relation ® is confluent if
every a Î A is confluent. Strong Normalisation: a Î A is strongly normalising if every reduction sequence starting from a
is finite. The rewrite relation ® is strongly normalising if every a Î A is strongly
normalising. Proving
proof nets confluent, implies that
there is no disruptive non-determinism in the system and would allow us to
infer that if a proof net has a normal form, it is a unique normal form.
Proving our system strongly normalising,
would allow us to infer that every proof net has a normal form. Confluence
and strong normalisation together imply that there is a unique normal form
for every proof net. However,
it is clear that strong normalisation does not hold for the type-free version
of (co)inductive proof nets. We only need a λ-term like (λx.xx)(λx.xx),
which has an infinite reduction sequence and therefore no normal form. It
follows directly from this example and the correspondence between proof nets
and the λ-calculus, that there is a proof net with an infinite reduction
sequence and no normal form, hence strong normalisation does not hold for the
type-free version of (co)inductive proof nets. Confluence
on the other hand, can be proven to hold for (co)inductive proof nets. In
[4], we present a new proof of confluence for proof nets which does not use
finiteness as an assumption and therefore holds for both inductive and coinductive proof nets. Note that even though we can
adapt counter examples from the (co)inductive λ-calculus, it is
necessary to build proofs like the one for confluence from scratch, because
the set of proof nets representing valid λ-terms is only a subset of the
set of all proof nets. Up to
this point, we have only spoken about the type-free version of (co)inductive
proof nets, for which we have seen that confluence does, but strong
normalisation does not hold. In the λ-calculus we see the exact same
thing, but we also see that strong normalisation does hold for a typed version of the inductive λ-calculus.
In [4] we present a new proof of the fact that strong normalisation also
holds for inductive proof nets, but not for coinductive
proof nets. A counter example for the latter can be constructed by taking any
typed proof net with an infinite number of redexes. |
||
|
Of course
a result like this is to be expected when working with infinite objects, but
in [4] we note that even the counterpart of strong normalisation in the
infinite domain, head normalisation,
does not hold either. The purpose of head normalisation is to contract only
those redexes that are strictly necessary, i.e. the
redexes that would be contracted no matter what
reduction strategy is applied. Our counter example against head normalisation
for typed coinductive proof nets is taken from the coinductive λ-calculus: CE = (λx.x) (λx.x)
(λx.x) (λx.x) ¼ ¥ It is
clear that regardless of the redex we choose, a
reduction of CE will always result
in CE itself. Consequently, the infinite
reduction sequence starting from CE
is not head normalizing. However, it is perfectly typable. Figure 2 shows the infinite proof net of CE.
Since a proof net is merely an implementation of a λ-term, it too will
have an infinite reduction sequence which is not head
normalizing. |
Figure 2: Proof net of CE |
|
|
Conclusions and Future Work In this
article we have seen that coinductive proof nets do
indeed possess the desirable property of confluence, but we also saw that it
does not have other ones like strong normalisation or even for head
normalisation, its counterpart in the infinite domain. So when we come to
evaluating the relevance of coinductive proof nets
we are as yet undecided. Future work on the system would include developing a
standardisation procedure, which always reduces a proof net to its head
normal form, if there is one. A successful attempt at this, would
significantly improve the relevance of coinductive
proof nets and because of their close relation, the coinductive
λ-calculus as well. References [1] Jean-Yves Girard, Linear Logic, Theoretical Computer Science 50, 1987. [2] Bart Jacobs and Jan Rutten, A Tutorial on (Co)Algebras and (Co)Induction,
Bulletin of the European Association for Theoretical
Computer Science 62, 1997. [3] Felix Joachimski,
Reduction Properties of П
IE-Systems, PhD Thesis, LMU München, 2001. [4] Laura Korte, Coinductive Proof Nets, MSc Thesis, Utrecht
University 2002. [5] Terese, Term Rewriting Systems, |
||
