Pawe³ Urzyczyn and Jean-Ives Girard
Patrick Baillot and Marco Pedicini 1-31
We introduce a geometry of interaction model given by an algebra of clauses equipped with resolution (following [10]) into which proofs of Elementary Linear Logic can be interpreted. In order to extend geometry of interaction computation (the so called execution formula) to a wider class of programs in the algebra than just those coming from proofs, we define a variant of execution (called weak execution). Its application to any program of clauses is shown to terminate with a bound on the number of steps which is elementary in the size of the program. We establish that weak execution coincides with standard execution on programs coming from proofs.
Sabine Broda and Luís Damas 33-51
We present a Counting Algorithm that computes the number of l-terms in b-normal form that have a given type t as a principal type and produces a list of these terms. The design of the algorithm follows the lines of Ben-Yelles' algorithm for counting normal (not necessarily principal) inhabitants of a type t. Furthermore, we show that one can use similar algorithms with adequate limits to count normal and principal normal inhabitants in the lI-calculus.
René David 53-77
This paper develops a general technique to analyze the head reduction of a term in a context. This technique is used to give a direct proof of the theorem of Hyland and Wadsworth : two l-terms that have the same Böhm trees, up to (possibly infinite) h-equivalence, are operationally equivalent. It is also used to prove a conjecture of R. Kerth : Every unsolvable l-term has a decoration. This syntactical result is motivated by (and gives the solution to) a semantical problem.
Masahiko Sato, Takafumi Sakurai and Rod Burstall 79-115
We introduce le, a simply typed calculus with environments as first class values. As well as the usual constructs of l and application, we have e\lbrack\lbrack a\rbrack\rbrack which evaluates term a in an environment e. Our environments are sets of variable-value pairs, but environments can also be computed by function application and evaluation in some other environments. The notion of environments here is a generalization of explicit substitutions and records. We show that the calculus has desirable properties such as subject reduction, confluence, conservativity over the simply typed lb-calculus and strong normalizability.
Rick Statman 117-121
In 1975, G. Jacopini proved the existence of an easy term, i.e., a term which can be consistently (with beta conversion) identified with any other term. In 1980, A. Visser generalized Jacopini's result to R.E. theories; namely, easy terms for consistent (with beta conversion) R.E. theories exist. Of course, no such generalization for non-R.E. theories exists. For example, it is easy to see that there is no easy term for Barendregt's theory H. In this note we shall generalize Jacopini's result to non-R.E. theories as follows. Say that an equation M = N is easy if for any consistent (with beta conversion) extension T we have that T È{ M = N} is consistent. We shall prove that easy equations exist.
C. Urban and G. M. Bierman 123-155
In this paper we present a strongly normalising cut-elimination procedure for classical logic. This procedure adapts Gentzen's standard cut-reductions, but is less restrictive than previous strongly normalising cut-elimination procedures. In comparison, for example, with works by Dragalin and Danos et al., our procedure requires no special annotations on formulae and allows cut-rules to pass over other cut-rules. In order to adapt the notion of symmetric reducibility candidates for proving the strong normalisation property, we introduce a novel term assignment for sequent proofs of classical logic and formalise cut-reductions as term rewriting rules.
János Apró and Sándor Vágvölgyi 157-172
We study that version of the ground tree transducer game where the same tree automaton appears as the first and second component of the associated ground tree transducer. We give conditions which imply that Beta has a winning strategy. Furthermore, we show the following decidability result. Given a ground tree transducer game where the underlying tree automaton A cannot evaluate some tree into a state or A is deterministic, we can decide which player has a winning strategy. Moreover, whatever player has a winning strategy, we can effectively construct a partial recursive winning strategy for him.
Philippe Balbiani and Dimiter Vakarelov 173-194
This paper is devoted to the completeness issue of PDL0Ç - an iteration-free fragment of Propositional Dynamic Logic with intersection of programs. The trouble with PDL0Ç is that the operation of intersection is not modally definable. Using new techniques connected with rules for intersection and the notions of large and maximal programs, the paper demonstrates that the presented proof theory for PDL0Ç is complete for the standard Kripke semantics of PDL0Ç.
Jean-Marc Champarnaud and Djelloul Ziadi 195-205
Our aim is to give a proof of the fact that two notions related to regular expressions, the prebases due to Mirkin and the partial derivatives introduced by Antimirov lead to the construction of identical nondeterministic automata recognizing the language of a given regular expression.
Petr Hájek and Sauro Tulipani 207-213
The satisfiability problem for the logic FP() (fuzzy probability logic over ukasiewicz logic) is shown to be NP-complete; satisfiability in FP(P) (the same over the logic joining ukasiewicz and product logic) is shown to be in PSPACE.
Padmanabhan Krishnan 215-229
In this paper we define a particular type of timed push down automata. We show that the emptiness problem for this class is decidable. We also present a notion of homomorphism and parallel decomposition for these automata. These notions are a generalisation of the homomorphism and decomposition via partitions for finite automata.
Alexander Meduna 231-235
The present paper discusses the uniform generation of languages by scattered context grammars. More specifically, it demonstrates that every recursively enumerable language can be generated by a scattered context grammar, G, so that every sentential form in a generation of a sentence has the form y1¼ym u, where u is a terminal word and each yi is a permutation of either of two equally long words, z1 Î {A, B,C}* and z2 Î {A, B, D}*, where A, B, C, and D are G's nonterminals. Then, it presents an analogical result so that u precedes y1¼ym.
Robert Saxon Milnikel 237-252
FC-normal logic programs are a generalization by Marek, Nerode, and Remmel of Reiter's normal default theories. They have the property that, unlike most logic programs, they are guaranteed to have simple stable models. In this paper it is shown that the problem of skeptical reasoning in FC-normal programs is P11-complete, the same complexity as for logic programs without the restriction of FC-normality.
FC-normal programs are defined in such a way as to make testing a program for FC-normality very difficult in general. A large subclass of FC-normal programs, locally FC-normal programs, is defined, shown to be recursive, and shown to have skeptical consequence as expressive as the entire class of FC-normal programs.
Bengt J. Nilsson 253-281
We present a fast algorithm for computing a watchman route in a simple polygon that is at most a constant factor longer than the shortest watchman route. The algorithm runs in O(nlogn) time as compared to the best known algorithm that computes a shortest watchman route which runs in O(n6) time.
Junior Barrera and Ronaldo Fumio Hashimoto 283-294
It is well known that any W-operator can be represented as the supremum (respectively, infimum) of sup-generating and (respectively, inf-generating) operators, that is, the families of sup-generating and inf-generating operators constitute the building blocks for representing W-operators. Here, we present two new families of building blocks to represent W-operators: compositions of sup-generating operators with dilations and compositions of inf-generating operators with erosions. The representations based on these new families of operators are called, respectively, sup-compact and inf-compact representations, since they may use less building blocks than the classical sup-generating and inf-generating representations. Considering the W-operators that are both anti-extensive and idempotent -in a strict sense-, we have also gotten a simplification of the sup-compact representation. We have also shown how the inf-compact representation can be simplified for any W-operator such that it is extensive and its dual operator is idempotent -in a strict sense-· Furthermore, if the W-operators are openings (respectively, closings), we have shown that this simplified sup-compact (respectively, inf-compact) representation reduces to a minimal realization of the classical Matheron's representations for translation invariant openings (respectively, closings).
Andries P. Engelbrecht 295-328
Research on improving the performance of feedforward neural networks has concentrated mostly on the optimal setting of initial weights and learning parameters, sophisticated optimization techniques, architecture optimization, and adaptive activation functions. An alternative approach is presented in this paper where the neural network dynamically selects training patterns from a candidate training set during training, using the network's current attained knowledge about the target concept. Sensitivity analysis of the neural network output with respect to small input perturbations is used to quantify the informativeness of candidate patterns. Only the most informative patterns, which are those patterns closest to decision boundaries, are selected for training. Experimental results show a significant reduction in the training set size, without negatively influencing generalization performance and convergence characteristics. This approach to selective learning is then compared to an alternative where informativeness is measured as the magnitude in prediction error.
Henning Fernau and Ralf Stiebe 329-358
We investigate four variants of valence regulations incorporated in (limited) Lindenmayer systems, focussing on hierarchical relations and closure properties. Strong connections to well-known families of languages obtained by regulated rewriting are established.
We prove several new results on valence transducers and valence generalized sequential machines (gsm). In this way, we can show new properties of ET0L languages, namely the non-closure under quasiintersection, valence gsm mappings and intersection with regular valence languages. Moreover, we solve a question marked as open in [36] by proving that the uniformly k-limited ET0L languages form a full semi-AFL for all k ³ 1.
Damas P. Gruska and Andrea Maggiolo-Schettini 359-378
Critical issues that arise when process algebras are used for protocol specifications are discussed. To overcome some of these problems, a process algebra for protocol specifications is presented. It is based on Milner's Calculus of Communicating Systems, which is enriched by time and network reasoning. Several bisimulation based semantics for the calculus are defined and their properties are discussed.
Antonino Salibra 379-392
The variety (equational class) of lambda abstraction algebras was introduced to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order predicate logic. In this paper we prove that the lattice of lambda theories is not modular and that the variety generated by the term algebra of a semi-sensible lambda theory is not congruence modular. Another result of the paper is that the Mal'cev condition for congruence modularity is inconsistent with the lambda theory generated by equating all the unsolvable l-terms.
Xishun Zhao and Decheng Ding 393-404
This paper is concerned with the complexity of default reasoning with 2CNF default theories (D,W) in which W is a set of literals and D is a set of 2CNF defaults. It is proved that the problem whether a literal occurs in at least one extension can be solved in polynomial time. But the problem whether a literal appears in all extensions is proved to be co-NP-complete. The complexity of some subclasses of 2CNF default theories is also analyzed.
File translated from TEX
by TTH, version 2.00.
On 23 Dec 2000, 13:05.