THEORY SEMINAR
                      AUTUMN TERM 2001

TIME AND PLACE:    Fridays 4 p.m. 
                   Room 144 New building, School of Computer Science--
                   usually.

ORGANISER:         Mateja Jamnik and Sammy Snow
                   (M.Jamnik@cs.bham.ac.uk, ext 44793, 
                    S.Snow@cs.bham.ac.uk, ext 44774)

SPEAKERS and TITLES

-- Friday 31 August 4pm, Dan Ghica, Queen's University, Canada
   Games-based techniques for program verification

-- Friday 7 September 4pm, Prof. Aaron Sloman, University of Birmingham
   When is seeing (possibly in your mind's eye) better than deducing for reasoning?

-- Friday 14 September 4pm, Alex Simpson, University of Edinburgh
   New building Room 144
   ****** Note the new place! ******
   Verifying Temporal Properties Using Explicit Approximations:
   Completeness for Context-free Processes

-- Friday 21 September 4pm, Julian Richardson, Heriot-Watt University
   New building Room 144
   ****** Note the new place! ******
   Continuing Continuations of Proof Strategies

-- Friday 28 September 4pm, Dimitar Guelev, Birmingham University
   New building Room 144
   ****** Note the new place! ******
   Interval Temporal Logics: A Survey

-- Friday 5 October 4pm, Martin Hyland, University of Cambridge (Uday)
   Polarised linear logic and tensor-not categories

-- Friday 12 October 4pm, Michael Huth, Imperial College (Achim)
   Toward abstract interpretation of object-modelling languages

-- Friday 19 October 4pm, Martin Otto, University of Wales, Swansea (Achim)
   Modal and Guarded Logics

-- Friday 26 October 4pm, Song Yan, Aaston University (Peter Coxhead)
   Number Theoretic Cryptography and Quantum Factoring
   ***** CANCELLED! ******

-- Friday 26 October 4pm, Joe Hurd, University of Cambridge (Marta)
   Verifying Probabilistic Algorithms using the HOL Theorem Prover

-- Friday  2 November 4pm, Alan Sexton, Birmingham University
   Generalising Quicksort to Index Structures

-- Friday 9 November 4pm, Roland Backhouse, Nottingham University (Achim)
   Abstract Interpretations for Free

-- Friday 16 November 4pm, Sylvain Peyronnet, University of Paris (Marta)
   Probabilistic Abstraction

-- Friday 23 November 4pm, Antonio Pacheco, IST, Lisbon (Marta)
   Traffic Modelling of Multimedia Wireless Networks

-- Friday 30 November 4pm, Jonathan Farley, University of Oxford and Vanderbilt University, USA (Achim)
   Probabilistic Powerdomains and Valuations on Distributive Lattices

-- Friday 7 December 4pm, Prof. Andy Pitts, University of Cambridge (Achim)
   ***** POSTPONED to 11 January, 2002! ******

-- Friday 7 December 4pm, John Longley, University of Edinburgh
   Getting at the computation strategy behind a program

-- Friday 14 December 4pm, Simon Colton, Edinburgh University and York University
   ***** POSTPONED to 1 February, 2002! ******

-- Friday 14 December 4pm, ??Daniele Veracca,  University of Cambridge (Marta, Achim)

________________________________________________________________________

			ABSTRACTS


-- Friday 31 August 4pm, Dan Ghica, Queen's University, Canada
   Games-based techniques for program verification

The Abramsky-McCusker games model of Idealized Algol with active
expressions can be substantially simplified in the absence of recursion
and higher-order procedures. Terms are interpreted by their sets of
complete plays (instead of strategies); such sets turn out to be regular
languages. The simplified regular-language model can validate term
equivalences in a simple and algorithmic manner.

The second part of the talk will examine how it is possible to apply the
model to interpret and model-check Hoare-style correctness statements. We
will discuss some of the issues and desiderata relevant to this technique
and the way they are addressed by a new games-based programming logic.
This final part describes work in progress.

_________________________________________________________________________
-- Friday 7 September 4pm, Prof. Aaron Sloman, University of Birmingham
   When is seeing (possibly in your mind's eye) better than deducing for reasoning?

In philosophy, psychology and AI there is a very long history of
discussion about different forms of reasoning -- what they are, how
they work, and whether they are valid. In the early days of AI,
research on problem solving, planning, theorem-proving, and other
topics was dominated by people who were committed to the use of
logical forms of representation and logical forms of derivation
(based on pioneering work in logic in the 19th Century by Frege).
However even in the early days of AI there were those who pointed
to the human ability to use diagrams and visual images, even in
reasoning about very abstract mathematical problems, and my first
paper on AI in 1971 was such a critique of the "logic suffices"
view, propounded in 1969 by McCarthy and Hayes.

Since then, there has been much research in AI on spatial and visual
reasoning, often using arrays and other supposedly "visual"
data-structures, and there have been a number of interesting
demonstrations of mechanised reasoning (including work by Mateja
Jamnik, in this school). The topic seems to be growing in popularity
now, e.g. with regular conferences on diagrammatic reasoning.
However I have deep reservations, about this because I feel that we
don't yet have a good analysis of what we are trying to explain, since
we don't know how to characterise human visual capabilities except in
very shallow ways.

In the talk I shall give a few examples of visual reasoning and use them
to point to problems in the analysis of what a visual system is. The
most important point is that besides providing information about
objects, their identities, their, properties and relations, seeing also
provides information about possible changes and constraints on changes
in structures and relationships. This is a generalisation of Gibson's
notion of "affordance". The study of mechanisms for perceiving and using
affordances may give us new insight into mathematical reasoning
capabilities in humans.


J.J Gibson, 1979
    The Ecological Approach to Visual Perception,
    Lawrence Earlbaum Associates,

M. Jamnik and A. Bundy and I. Green, 1999
    On Automating Diagrammatic Proofs of Arithmetic Arguments,
    Journal of Logic, Language and Information, 8, 3,
    pp. 297--321,

J. McCarthy and P.J. Hayes, 1969,
    Some philosophical problems from the standpoint of AI,
    in Machine Intelligence 4, Eds. B. Meltzer and D. Michie,
    Edinburgh University Press,
    http://www-formal.stanford.edu/jmc/mcchay69/mcchay69.html

A. Sloman, 1995
    Musings on the roles of logical and non-logical representations, in
    intelligence, in Diagrammatic Reasoning: Computational and
    Cognitive Perspectives, MIT Press,
    Eds. J. Glasgow, H. Narayanan and Chandrasekaran, pp. 7--33
    http://www.cs.bham.ac.uk/research/cogaff/Aaron.Sloman_musings.ps
    http://www.cs.bham.ac.uk/research/cogaff/Aaron.Sloman_musings.pdf

_________________________________________________________________________
-- Friday 14 September 4pm, Alex Simpson, University of Edinburgh
   Verifying Temporal Properties Using Explicit Approximations:
   Completeness for Context-free Processes

The modal mu-calculus offers a rich logic for expressing temporal
properties of processes, and much effort has gone into developing
techniques for automatically model-checking such properties of
finite state processes. However, general processes (for example
arbitrary CCS processes) are not finite state, and the
problem of checking whether a process (expressed in a process
algebra) satisfies a formula is undecidable. 

In the face of undecidability, one seeks formal systems that are
sound for establishing properties of processes. Although necessarily
incomplete, one would like to find systems that provide perspicuous
reasoning methods which suffice in practice. Much of the talk will be 
devoted to presenting a sequent calculus, strongly based on a system
proposed by Mads Dam and Dilian Gurov, that I believe satisfies
these requirements. The crucial idea, due to Dam and Gurov, is to
introduce explicit mu-calculus approximants into the proof system,
allowing induction and coinduction arguments to be subsumed by
a global combinatorial condition on proofs. 

It is an interesting question to what extent the methods
provided by the proof system do suffice in practice. One way
of addressing this is to obtain restricted completeness results,
showing completeness in special cases where such results are at least
possible in theory. I shall conclude by discussing a new result in
this direction, due to my MSc student Ulrich Schoepp. He has
shown that the proof system is complete for establishing
arbitrary mu-calculus properties of context-free processes.
The decidability of this problem has long been known, but
previous algorithms have used techniques specific to 
context-free processes. As far as we know, this is the first
such result based on showing that general purpose techniques
suitable for arbitrary processes are complete when specialised
to context-free processes.

_________________________________________________________________________
-- Friday 21 September 4pm, Julian Richardson, Heriot-Watt University
   G42, Mech Eng
   ****** Note the unusual place! ******
   Continuing Continuations of Proof Strategies

In this talk I describe recent work which extends that reported in
[RS01].

Complex proof strategies can be formed by combining tactics
using tacticals. Similarly, complex proof planning strategies can
be formed by combining proof planning methods using methodicals.

In this talk I briefly describe methods and methodicals, as implemented 
in the LambdaClam higher-order proof planner.

I present a meta-interpreter which gives a semantics to methodical
expressions. In conjunction with a mechanism for executing methods and
a search strategy, this meta-interpreter can be used as a proof
planner. This planner does not have any notion of proof state, and is
unsuitable for interactive proof.

I present a set of transformation rules which can be used to define a
new meta-interpreter which does maintain a notion of proof state, is
suitable for interactive proof. It is limited in that it does not
provide a good treatment of branching, or the "cut" methodical, but
despite these limitations it has been used successfully for some time as
the basis of an interactive proof planner in LambdaClam. It can be
proven that it is equivalent to the original meta-interpreter in the
sense that it produces the same plans (for the fragment of the
methodical language considered).

The transformation rules can be interpreted as defining a notion of
continuation for proof planning strategies. Based on this observation,
I show how previous work on a continuation semantics for Prolog can be
adapted to provide a continuation semantics for proof planning
strategies which correctly treats both and- and or- branching, and the
cut methodical.

Reference

"Continuations of Proof Strategies", Short Papers of International Joint 
Conference on Automated Reasoning Siena, Italy, June 2001, Rajeev Gore, Alexander Leitsch, Tobias Nipkov (Eds.). Available at: http://www.cee.hw.ac.uk/~julianr/methodicals_ijcarfinal.ps.gz

________________________________________________________________________
-- Friday 28 September 4pm, Dimitar Guelev, Birmingham University
   Interval Temporal Logics: A Survey

Interval Temporal Logic (ITL) was introduced by Ben Moszkowski in 1985
both as a specification formalism and a programming language. Since
then, it has been extended in various ways for the purpose of the
specification of real time systems. 
In this talk I present the basic system of ITL, the Duration Calculus
(DC, Zhou, Hoare and Ravn, 1991), which is the most widely applied and
thoroughly studied of its extensions, and the extension of ITL and DC by
neighbourhood modalities, a least fixed point operator, higher order
quantifiers and a projection operator.
I briefly discuss the part that each of these extensions has in the
specification of real-time systems.

_________________________________________________________________________
-- Friday 5 October 4pm, Martin Hyland, University of Cambridge (Uday)
   Polarised linear logic and tensor-not categories

Polarised linear logic is a relatively unproblematic
fragment of linear logic which is used as the basis 
for translations of classical logic and which
motivates `Ludics'.  I shall explain the system
and its connection with response categories and so
with the basis of CPS translations. Then I shall start 
with (a categorical version of) a lambda calculus
translation and show how to derive a fresh model
of CPS: this is a basic construction which should have
applications. Finally I shall say something about 
the connection with Ludics.

_________________________________________________________________________
-- Friday 12 October 4pm, Michael Huth, Imperial College (Achim)
   Toward abstract interpretation of object-modelling languages

We conduct a semantic case study as a first step toward
abstraction-based model checking of object models whose state aspects
and behavior may involve terms and large/infinite types. Specifically,
we consider partial models --- conventional first-order logic models
that "forget" the meaning of some constants, functions, and relations.
We use the Smyth powerdomain to give partial models a formal, three-valued
semantics. We develop notions of refinement and abstraction and
prove their soundness for "monotone scopes". Conventional first-order
logic embeds conservatively into the set of maximal elements of the
respective Smyth powerdomains. Given the discrete set {True, False},
set-union on its Smyth powerdomain functions as a consensus operator
that enables the reduction of the three-valued model-checking problem for
partial models to two conventional model checks of standard first-order
logic models, creating an opportunity to re-use established concepts and
tools.

_________________________________________________________________________
-- Friday 19 October 4pm, Martin Otto, University of Wales, Swansea (Achim)
   Modal and Guarded Logics

Guarded logics have, since the introduction of the guarded fragment
GF of first-order logic FO by Andreka, van Benthem and Nemeti, seen
a career as a promising intermediary between basic modal logics and FO.
Not only do they offer a much more satisfactory explanation
of the good behaviour of modal logics in their manifold applications,
but they also promise to extend some of the power of algorithmic and
model theoretic techniques from the modal domain to much richer domains.

I shall review some of the recent history of this development and
illustrate parallels between the modal and guarded scenarios,
in the light of some key results.

The guiding ideas come from the model theoretic games that capture
the underlying semantic invariances -- bisimulation invariance and
guarded bisimulation invariance, respectively.
Their properties account for the specific model theoretic tools
that can be brought to bear.

_________________________________________________________________________
-- Friday 26 October 4pm, Joe Hurd, University of Cambridge (Marta)
   Verifying Probabilistic Algorithms using the HOL Theorem Prover

Probabilistic algorithms can be difficult to implement correctly,
since it is hard to use conventional testing methods to catch bugs of
the form 'wrong probability distribution'. Formal methods offer an
opportunity to verify that probabilistic algorithms work correctly,
and in this talk I'll describe an approach using the HOL theorem
prover.

The talk will first sketch out the general framework for specifying
and verifying probabilistic algorithms in the theorem prover, and then
move on to some examples: a sampling algorithm for the binomial
distribution, optimal dice, and the Miller-Rabin primality test.  No
prior knowledge of the HOL theorem prover will be assumed.

_________________________________________________________________________
-- Friday  2 November 4pm, Alan Sexton, Birmingham University
   Generalising Quicksort to Index Structures

In managing large external collections of complex objects, sorting by
various criterion is sometimes required. However high object comparison
costs make merge sort less practical and complex ordering requirements
severely limit the applicability of index scans. We motivate this
problem with examples from geographic information systems, information
retrieval and theorem proving systems and then present an original
algorithm for an index sort based on an order theoretic generalisation
of Quicksort and discuss some issues arising from its development.

_________________________________________________________________________
-- Friday 9 November 4pm, Roland Backhouse, Nottingham University (Achim)
   Abstract Interpretations for Free

Abstract interpretation is a technique for approximating the execution  
behaviour of  a  computer program.  It is used, for example, for
strictness analysis of  functional programs; the results of such an
analysis are approximate in the sense that  non-strict programs will
always be correctly identified as such but strict programs may be
incorrectly classified.  In this sense the approximation is "safe".   

The basis of  abstract interpretation is the notion of a Galois
connection between ordered sets. 

"Theorems-for-free" is a remarkable feature  of parametrically
polymorphic functions, namely that knowing just the type of  a
function it is possible to derive algebraic properties of the
function.  For example, it is possible to  show that any function that
has the same type as function composition must be associative. 

This talk will introduce abstract interpretations, Galois connections
and  "theorems-for-free" to the non-expert audience.  The talk will
conclude with  a brief account of a recent result, namely that safe
abstract interpretations can be constructed ``for free'' by suitably
exploiting the properties of  parametrically polymorphic functions. 

This is joint work with Kevin Backhouse, Computing Laboratory,
University of Oxford.
_________________________________________________________________________
-- Friday 16 November 4pm, Sylvain Peyronnet, University of Paris, France (Marta)
   Probabilistic Abstraction

In model checking, program correctness on all inputs is verified by
considering the transition system underlying a given program. In
practice, the system can be intractably large. In property testing, a
property of a single input is verified by looking at a small subset of
that input. We join the strengths of both approaches by introducing to
model checking the notion of probabilistic abstraction. We put forth
the notion of eps-reducibility which is implicit in many property
testers. Our probabilistic abstraction associates a set of small random
transition systems to a program. Under some conditions, these
transition systems are sufficient to guarantee that a program
approximately decides on all its inputs a property like bipartiteness,
k-colorability, or any first order graph properties of type
existsforall. We give a concrete example of an abstraction for a
program which decides bipartiteness.

_________________________________________________________________________
-- Friday 23 November 4pm, Antonio Pacheco, IST, Lisbon (Marta)
   Traffic Modelling of Multimedia Wireless Networks

Mobile broadband wireless networks are seen today as one of the key
factors for the development of the emerging global communication
infrastructure in the near future. Their design, planning and control
must be supported by suitable traffic models in which both mobility
and the new teletraffic aspects are merged in an integrated way.

We develop a traffic model for scenarios allowing mobility in multiple 
directions in the plane. The transient and limit analysis of the
number of mobiles per call state in a cell as well as the handoff
processes between cells are investigated. The new and handoff call
blocking probabilities for network planning are derived, and the
distribution of the required capacity in a short time interval for
network control is obtained. 

We will present simulation results that have been carried out to
validate the analytical results and give insight on how network
performance measures may be computed.

_________________________________________________________________________
-- Friday 30 November 4pm, Jonathan Farley, University of Oxford and Vanderbilt University, USA (Achim)
   Probabilistic Powerdomains and Valuations on Distributive Lattices

A famous problem in domain theory is the following question: Is the
probabilistic powerdomain of an FS-domain an FS-domain?  We do not answer
this question, as we only just learned about FS-domains last week.
Instead, we attempt to understand the structure of probabilistic
powerdomains by using the fact that they are valuations on distributive
lattices.  Hence, Priestley duality for distributive lattices might yield
some insights.

_________________________________________________________________________
-- Friday 7 December 4pm, John Longley, University of Edinburgh
   Getting at the computation strategy behind a program

Consider the not very interesting game in which two players take turns to
name a natural number (that's all!). This can be considered as a "universal
game" in the sense that a large class of other games can be encoded in it.
Strategies for this game can be represented straightforwardly by values of
the following type in ML:

    datatype Forest = forest of nat -> (nat * Forest)

As I will show, this type can be given the structure of a lambda algebra,
which yields as its Karoubi envelope a semantically rich category of
"sequential processes", closely related to one of Abramsky's categories of
games. Moreover, the application and abstraction operations for this
lambda algebra can actually be implemented in New Jersey SML, making
essential use of continuations.

On the theoretical side, this gives us a seemingly new completeness
result: the category of games in question is a fully abstract and universal
model of an extension of PCF with continuations and first-order state.
On the practical side, one upshot of this is that for any type t, we can
write a program of type t -> Forest which explicitly gives us the computation
strategy underlying any operation of type t; this in turn has applications
to (interactive) execution tracing, debugging, and program optimization.
I will demonstrate a prototype system illustrating these capabilities.

The Karoubi envelope of a lambda algebra is of course a cartesian closed
(i.e. intuitionistic) category. However, there is also some interesting
linear structure around, which I am starting to explore. I will say a bit
about how this promises to yield good denotational models for object
oriented languages.

_________________________________________________________________________
_________________________________________________________________________