![[McsHomepage]](/images/McsLogoIcon.gif)
1996/1
Approximation of Smooth Functions by sk-Splines
A.K. Kushpel, J. Levesley and W. Light
In the classical sense a spline is a piecewise polynomial. Schoenberg is the father of modern spline theory but such functions go as far back as the time of Leibnitz. The last fifty years have seen an explosion if interest in splines resulting in many generalisations. In this paper we study one such generalisation; the sk-spline. The space of sk-splines is the linear span of shifts of a single kernel $k$. Such spline functions have been considered by many different investigators (Cheney, Chui, Dyn, Light, Micchelli, Pinkus, and Tikhomirov, to name but a few) under very restrictive conditions on the kernel $k$. We impose more general conditions and this enables us to give a unified treatment for a wide range of spline functions, having finite, fractional, infinite, analytic, or entire smoothness. For instance, we will consider problems of existence and uniqueness of sk-spline interpolants, give an error analysis for sets of functions of different smoothness, present a variational approach, and give some extremal properties of sk-splines. We conclude by outlining a generalisation of sk-splines to compact Abelian groups.
1996/2
(ps.gz)
On Representing Finite Lattices as Intervals in Subgroup Lattices
of Finite Groups
R. Baddeley and A. Lucchini
Let M_n be the lattice of length 2 with n>0 atoms. It is an open problem to decide whether or not every such lattice (or indeed whether or not every finite lattice) can be represented as an interval in the subgroup lattice of some finite group. We complete the work of the second author, Lucchini, by reducing this problem to a series of questions concerning the finite non-abelian simple groups.
1996/3
(dvi.gz)
On Fixpoint Objects and Gluing Constructions
R.L. Crole
This article (AMS classification 18 C 10) has two parts:
In the first part, we present some general results about fixpoint objects. The minimal categorical structure required to model soundly the equational type theory which combines higher order recursion and computation types is shown to be precisely a let-category possessing a fixpoint object. Functional completeness for such categories is developed. We also prove that categories with fixpoint operators do not necessarily have a fixpoint object.
In the second part, we extend Freyd's gluing construction for cartesian closed categories to cartesian closed let-categories, and observe that this extension does not obviously apply to categories possessing fixpoint objects. We solve this problem by giving a new gluing construction for a limited class of categories with fixpoint objects; this is the main result of the paper. We use this category-theoretic construction to prove a type-theoretic conservative extension result.
A version of this paper is due to appear in the Journal of Applied Categorical Structures.
1996/4
Verification of Fault-Tolerance and Real-Time
Z. Liu
A transformational method is given for specifying and verifying fault-tolerant
real-time programs. Such a program needs to be provably correct according to
its both functional and real-time requirements, despite of the presence of
possible system failures. The paper demonstrates that a suitably expressive
logic for real-time systems allows to naturally model the state changes by
system failures and determine their effect on the functional and real-time
properties of executions.
Keywords: fault-tolerance, fault-tolerant refinement, real-time,
specification, transformation.
1996/5
Relating Operational and Denotational Semantics for Input/Output
Effects
R.L. Crole and A.D. Gordon
We study the longstanding problem of semantics for input/output (I/O) expressed using side-effects. Our vehicle is a small higher-order imperative language, with operations for interactive character I/O and based on ML syntax. Unlike previous theories, we present both operational and denotational semantics for I/O effects. We use a novel labelled transition system that uniformly expresses both applicative and imperative computation. We make a standard definition of bisimilarity. We prove bisimilarity is a congruence using Howe's method.
Next, we define a metalanguage M in which we may give a denotational semantics to O. M generalises Crole and Pitts' FIX-logic by adding in a parameterised recursive datatype, which is used to model I/O. M comes equipped both with an operational semantics and a domain-theoretic semantics in the category CPPO of cppos (bottom-pointed posets with joins of w-chains) and Scott continuous functions. We use the CPPO semantics to prove that M is computationally adequate for the operational semantics using formal approximation relations. The existence of such relations is based on recent work of Pitts for untyped languages, and uses the idea of minimal invariant objects due to Freyd.
A monadic-style textual translation into M induces a denotational semantics on O. Our final result validates the denotational semantics: if the denotations of two O programs are equal then the O programs are in fact operationally equivalent.
1996/6
Regular Subgraphs in Graphs and Rooted Graphs, and Definability
in Monadic Second-order Logic
I.A. Stewart
We investigate the definability in monadic \Sigma_1^1 and monadic \Pi_1^1 of the problems REG_k, of whether there is a regular subgraph of degree k in some given graph, and XREG_k, of whether, for a given rooted graph, there is a regular subgraph of degree k in which the root has degree k, and their restrictions to graphs in which every vertex has degree at most k, namely REG_k^k and XREG_k^k, respectively, for k >=2 (all our graphs are undirected). Our motivation partly stems from the fact (which we prove here) that REG_k^k and XREG_k^k are logspace equivalent to CONN and REACH, respectively, for k >= 3, where CONN is the problem of whether a given graph is connected and REACH is the problem of whether a given graph has a path joining two given vertices. We use monadic first-order reductions, monadic \Sigma_1^1 games and a recent technique due to Fagin, Stockmeyer and Vardi to almost completely classify whether these problems are definable in monadic \Sigma_1^1 and monadic \Pi_1^1, and we compare the definability of these problems (in monadic \Sigma_1^1 and monadic \Pi_1^1) with their computational complexity (which varies from solvable using logspace to NP-complete).
1996/7
Higher vn Torsion in Lie Groups
J. Hunton, M. Mimura, T. Nishimoto and B. Schuster
We study the Morava K-theory of the exceptional Lie groups at the prime 2, and of certain projective Lie groups at a variety of primes.
1996/8
Presentations for Subsemigroups - Applications to Ideals of Semigroups
C.M. Campbell, E.F. Robertson, N. Ruskuc, R.M. Thomas.
A method for finding presentations for subsemigroups of semigroups defined by presentations is used to investigate when ideals are finitely presented. It is shown that an ideal of a finitely presented semigroup is not necessarily finitely presented, even if it is finitely generated as a semigroup. By way of contrast, it is then proved that in a free product of two, or indeed of finitely many, finite semigroups, every right ideal which is finitely generated as a semigroup is finitely presented.
1996/9
On embedding cycles in $k$-ary $n$-cubes
Y.A. Ashir, I.A. Stewart
We completely classify when a $k$-ary $n$-cube $Q_n^k$, for $k\geq 3$ and $n\geq 2$, contains a cycle of some given length. Our analysis yields an efficient algorithm for generating a cycle of any given length, if indeed one exists, thus answering a question posed by Bose, Broeg, Kwon and Ashir.
1996/10
Logics with zero-one laws that are not fragments of bounded-variable
infinitary logic
I.A. Stewart
We show that the (NP-complete) problem CUB, being the problem of deciding whether a graph has a cubic subgraph, can not be defined in ${\cal L}^\omega_{\infty\omega}$; and so the logic $(\pm\mbox{CUB})^\ast[\mbox{FO}]$ has a zero-one law and can not be regarded as a fragment of ${\cal L}^\omega_{\infty\omega}$. It had previously been shown that the logic $(\pm\mbox{3COL})^\ast[\mbox{FO}]$, where 3COL is the problem of deciding whether a graph can be 3-coloured, enjoys a similar status. In an attempt to clarify their relative expressibilities, we show that the problems 3COL and CUB are not equivalent with respect to first-order translations but that there exist problems definable in $(\pm\mbox{3COL})^\ast[\mbox{FO}]$ and $(\pm\mbox{CUB})^\ast[\mbox{FO}]$ that are not first-order definable: it remains open as to whether these two logics have the same expressibility. In order to prove our results we slightly extend a technique due to Cai, F\"{u}rer and Immerman, and we formulate and play (extended Ehrenfeucht-Fra\"{\i}ss\'{e}) games very similar to those proposed by Kolaitis and V\"{a}\"{a}n\"{a}nen, and Gr\"{a}del.
1996/13
On classifying all full factorisations and multiple-factorisations
of the finite almost simple groups
R. Baddeley, C.E. Praeger
We present some general results on factorisations of almost simple groups. These results are consequences of the classification of all maximal factorisations of almost simple groups (due to Liebeck, Saxl, and the second author), and are needed for applications to the theory of quasiprimitive permutation groups.
1996/14
On primitive overgroups of quasiprimitive permutation groups
R. Baddeley, C.E. Praeger
A permutation group is said to be quasiprimitive if all its non-trivial normal subgroups are transitive. We investigate pairs (G,H) of permutation groups of degree n such that G< H<S_n with G quasiprimitive and H primitive. An explicit classification of such pairs is obtained except in the cases where the primitive group H is either almost simple or the blow-up of an almost simple group. (The theory in the latter case is investigated in a separate paper.)
1996/15
Preconditions for the Adaptive h-p Version Finite Element Method
Ainsworth B. Senior D. Andrews
A domain decomposition preconditioner suitable for $h$-$p$ finite element approximation on adaptively refined meshes with non-uniform polynomial degree is described. The preconditioner is highly suited for parallel computation and generalizes methods proposed by B.F.Smith for the $h$-version finite element method with piecewise linear basis functions, and by J.Mandel for the $p$-version finite element method. The preconditioner was recently analysed by Ainsworth where it was shown that the condition number of the preconditioned system grows at most logarithmically in the degree $p$ and mesh size $h$. This result generalizes the known sharp estimates in each of the cases mentioned above. The preconditioner is used to solve the linear systems on highly non-uniform adaptive $h$-$p$ meshes arising from the adaptive solution of a problem with a crack singularity.
1996/16
On Fixpoint Objects for Commutative Faithful Monads
R.L. Crole
We give an adapted version of a result due to Alex Simpson, that under suitable conditions the data which specify a fixpoint object (FPO) are the same as the data given by the canonical isomorphism of certain initial algebras and final coalgebras. The original source upon which this report is based is an unpublished note by Simpson.
1996/17
How Linear is Howe?
R.L. Crole
In recent years there has been much progress in the use of operationally based methods for reasoning about programs. Notions such as contextual equivalence and bisimilarity, which are historically more usually associated with functional programming and concurrency respectively, have been shown to be very closely connected, and such connections can be seen throughout the functional, concurrent and indeed imperative paradigms. In this paper we show that operational techniques from these three settings also apply in a linear functional setting, by proving that in a simple linear type theory involving function types and tensor types, one can establish linear contextual equivalences by coinductive techniques.
1996/18
On the power of built-in relations in certain classes of program schemes
S.R. Chauhan, I.A. Stewart
We consider the computational power of the classes of program schemes obtained from NPS by including built-in relations from $\{successor,linear$-$order,addition, multiplication\}$: we are motivated by the known characterization of the complexity class NL (nondeterministic logspace) as those problems accepted by the program schemes of NPS in the presence of a built-in successor relation (the class of program schemes NPS consists of, essentially, nondeterministic while programs with quantifier-free tests, which take as input some finite structure over some fixed signature). We completely classify the relative computational power of these classes of program schemes, as we do for the relative descriptive power of similar extensions of the bounded-variable infinitary logic ${\cal L}_{\infty\omega}^\omega$ and its existential fragment. Our proofs involve playing (infinitary) pebble games.
1996/23
A Posteriori Error Estimation for Fully Discrete Hierarchic Models of Elliptic Boundary Value Problems on Thin Domains
Mark Ainsworth
A posteriori error estimators for fully discrete hierarchic modelling on thin domains are derived and are shown to provide computable upper bounds on the discretization error and on the total error. The estimators are shown to be robust and do not degenerate as the thickness of the domain tends to zero. If the discretization part of the error is negligible, the estimator for the modelling error reduces to the one recently obtained for semi-discrete hierarchical modelling by Babuska and Schwab.
1996/24
On Hochschild Cohomology of Preprojective Algebras, I
Karin Erdmann, Nicole Snashall
We study the Hochschild cohomology of a finite-dimensional preprojective algebra $\Lambda$; this is periodic by a result of A. Schofield. In particular, for $\Lambda$ of type $A_n$ we obtain the dimensions and explicit characterizations and bases for all Hochschild cohomology groups.
1996/25
On Hochschild Cohomology of Preprojective Algebras, II
Karin Erdmann, Nicole Snashall
We study the Hochschild cohomology of a finite-dimensional preprojective algebra; this is periodic by a result of A. Schofield. We determine the ring structure of the Hochschild cohomology ring given by the Yoneda product. As a result we obtain an explicit presentation by generators and relations.
1996/26
Positive versions of polynomial time
C. Lautemann, T. Schwentick, I.A. Stewart
We show that restricting a number of characterizations of the complexity class {\bf P} to be positive (in natural ways) results in the same class of (monotone) problems which we denote by {\bf posP}. By a well-known result of Razborov, {\bf posP} is a proper subclass of the class of monotone problems in {\bf P}. We exhibit complete problems for {\bf posP} via weak logical reductions, as we do for other logically defined classes of problems. Our work is a continuation of research undertaken by Grigni and Sipser, and subsequently Stewart; indeed, we introduce the notion of a positive deterministic Turing machine and consequently solve a problem posed by Grigni and Sipser.
1996/28
Communication algorithms in $k$-ary $n$-cube interconnection networks
Y.A. Ashir, I.A. Stewart
In this paper we consider several communication algorithms in the $k$-ary $n$-cube interconnection network; in particular, we develop and analyse routing, multi-node broadcasting, single-node scattering and total exchange algorithms. All of our algorithms are optimal if we assume one-port I/O communication.
1996/29
An Adaptive Refinement Strategy of hp-finite Elemens Computations
M Ainsworth, B Senior
A refinement strategy for fully adaptive $hp$-finite element solution of elliptic boundary value problems is presented. The algorithm is based on the local regularity of the exact solution. A method is given for estimating the local regularity {\em a posteriori}. The performance of the algorithm is illustrated for some simple representative problems.
1996/30
Fault-tolerant embeddings of Hamiltonian circuits in $k$-ary $n$-cubes
Y.A. Ashir, I.A. Stewart
We consider the fault-tolerant capabilities of networks of processors whose underlying topology is that of the $k$-ary $n$-cube $Q_n^k$, where $k\geq 3$ and $n\geq 2$. In particular, given a copy of $Q_n^k$ where some of the inter-processor links may be faulty but where every processor is incident with at least two healthy links, we show that if the number of faults is at most $4n-5$ then $Q_n^k$ still contains a Hamiltonian circuit, but that there are situations where the number of faults is $4n-4$ (and every processor is incident with at least two healthy links) and no Hamiltonian circuit exists. We also show that given a faulty $Q_n^k$, the problem of deciding whether there exists a Hamiltonian circuit is NP-complete.
1996/37
Generalized Hex and logical characterizations of polynomial space.
A A Arratia-Quesada, I A Stewart
We answer a question posed by Makowsky and Pnueli and show that the logic $(\pm\mbox{HEX})^\ast[\mbox{FO}_s]$, where HEX is the operator (i.e., uniform sequence of Lindstr\"om quantifiers) corresponding to the well-known {\bf PSPACE}-complete decision problem Generalized Hex, collapses to the fragment $\mbox{HEX}^1[\mbox{FO}_s]$ and, moreover, that this logic has a particular normal form which results in the problem HEX being complete for {\bf PSPACE} via quantifier-free projections with successor (HEX is the first ``natural'' problem to be shown to have this property). Our proof of this normal form result is remarkably similar to Immerman's original proof that transitive closure logic, $(\pm\mbox{TC})^\ast[\mbox{FO}_s]$, has such a normal form; which is surprising given that $(\pm\mbox{HEX})^\ast[\mbox{FO}_s]$ captures {\bf PSPACE} and $(\pm\mbox{TC})^\ast[\mbox{FO}_s]$ captures {\bf NL}. We also show that $(\pm\mbox{HEX})^\ast[\mbox{FO}]$ does not capture {\bf PSPACE} and that this logic does not have a corresponding normal form.
1996/38
Formalizing Real-Time Scheduling as Program Refinement
Z Liu, M Joseph
A real-time program can be developed by refining a specification into program code. Verification of the timing properties of the program is then usually done at two levels: verification of the ordering of timed actions in the program and proof that execution of the program on a specific system will meet its timing requirements. Refinement is done within a formal model but the second step requires a different framework in which scheduling theory analysis is used and actual program execution times can be taken into account. The implementation of a program on a system is said to be {\em feasible} or {\em schedulable} if it will meet all the timing deadlines.
This paper shows how the {\em feasibility} of scheduling a real-time program can also be proved as a step in the refinement of the program from its specification. Verification of this step of refinement makes use of both formal methods and scheduling theory, and uses a logic and a single semantic model.
Keywords: real-time program; specification; refinement; feasibility; schedulability.
1996/39
Coalgebraic Algebra
J Hunton, P Turner
We investigate module objects in categories of coalgebras, setting up tensor products and initiating the study of the resulting homological algebra.
![[Top]](/images/McsTopIcon.gif)