A game semantics for disjunctive logic programming

Denotational semantics of logic programming and its extensions (by allowing negation, disjunctions, or both) have been studied thoroughly for many years. In 1998, a game semantics was given to definite logic programs by Di Cosmo, Loddo, and Nicolet, and a few years later it was extended to deal with negation by Rondogiannis and Wadge. Both approaches were proven equivalent to the traditional semantics. In this paper we define a game semantics for disjunctive logic programs and prove soundness and completeness with respect to the minimal model semantics of Minker. The overall development has been influenced by the games studied for PCF and functional programming in general, in the styles of Abramsky–Jagadeesan–Malacaria and Hyland–Ong–Nickau.     

Full abstraction for Reduced ML

We present the first effectively presentable fully abstract model for Stark?s Reduced ML, a call-by-value higher-order programming language featuring integer-valued references. The model is constructed using techniques of nominal game semantics. Its distinctive feature is the presence of carefully restricted information about the store in plays, combined with conditions concerning the participants? ability to distinguish reference names. We show how it leads to an explicit characterization of program equivalence.     

Imperative programs as proofs via game semantics

Game semantics extends the Curry–Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. The system is expressive: it contains all of the connectives of Intuitionistic Linear Logic, and first-order quantification. Use of Laird?s sequoid operator allows proofs with imperative behaviour to be expressed. Thus, we can embed first-order Intuitionistic Linear Logic into this system, Polarized Linear Logic, and an imperative total programming language.     

Strong normalization results by translation

We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed λμ-calculus. We also extend Mendler’s result on recursive equations to this system.     

Separating the basic logics of the basic recurrences

This paper shows that, even at the most basic level (namely, in combination with only ¬,∧,∨), the parallel, countable branching and uncountable branching recurrences of computability logic validate different principles.     

A lower bound for higher topological complexity of real projective space

We obtain an explicit formula for the best lower bound for the higher topological complexity, ${\mathrm{TC}}_k(R{P}^n)$, of real projective space implied by mod 2 cohomology.     

A note on “Extensional PERs”

In the paper “Extensional PERs” by P. Freyd, P. Mulry, G. Rosolini and D. Scott, a category C of “pointed complete extensional PERs” and computable maps is introduced to provide an instance of an algebraically compact category relative to a restricted class of functors. Algebraic compactness is a synthetic condition on a category which ensures solutions of recursive equations involving endofunctors of the category. We extend that result to include all internal functors on C when C is viewed as a full internal category of the effective topos. This is done using two general results: one about internal functors in general, and one about internal functors in the effective topos.     

Relativization makes contradictions harder for Resolution

We provide a number of simplified and improved separations between pairs of Resolution-with-bounded-conjunction refutation systems, Res(d)$\mathrm{Res}(d)$, as well as their tree-like versions, Res^?(d)${\mathrm{Res}}^{?}(d)$. The contradictions we use are natural combinatorial principles: the Least number principle  , _LNPn${\mathrm{LNP}}_n$ and an ordered variant thereof, the Induction principle  , _IPn${\mathrm{IP}}_n$.     

On list primitive recursion and the complexity of computinginf

We present a primitive recursive programinf_with_lists computing the minimum of two natural numbersn andp (written in unary notation) and using primitive recursion on lists. This program has at first sight the required property of visiting simultaneously its inputs, so it is a counterexample to a theorem showing that such a program cannot be written in the language of primitive recursion on natural numbers, in the more general framework of primitive recursion on term algebras. However, its complexity is at leastinf(n,p)² so it does not implement the algorithm we have in mind to computeinf(n,p).     

Congruence preserving functions of Wilke’s tree algebras

As a framework for characterizing families of regular languages of binary trees, Wilke introduced a formalism for defining binary trees that uses six many-sorted operations involving letters, trees and contexts. In this paper a completeness property of these operations is studied. It is shown that all functions involving letters, binary trees and binary contexts which preserve congruence relations of the free tree algebra over an alphabet, are generated by Wilke’s functions, if the alphabet contains at least seven letters. That is to say, the free tree algebra over an alphabet with at least seven letters is affine-complete. The proof yields also a version of the theorem for ordinary one-sorted term algebras: congruence preserving functions on contexts and members of a term algebra are substitution functions, provided that the signature consists of constant and binary function symbols only, and contains at least seven symbols of each rank. Moreover, term algebras over signatures with at least seven constant symbols are affine-complete.Received March 18, 2004; accepted in final form October 8, 2004.     

A restricted computation model on Scott domains and its partial primitive recursive functionals

The paper builds on both a simply typed term system and a computation model on Scott domains via so-called parallel typed while programs (PTWP). The former provides a notion of partial primitive recursive functional on Scott domains supporting a suitable concept of parallelism. Computability on Scott domains seems to entail that Kleene's schema of higher type simultaneous course-of-values recursion (scvr) is not reducible to partial primitive recursion. So extensions and PTWP are studied that are closed under scvr. The twist are certain type 1 G?del recursors for simultaneous partial primitive recursion. Formally, denotes a function , however, is modelled such that is finite, or in other words, a partial sequence. As for PTWP, the concept of type writable variables is introduced, providing the possibility of creating and manipulating partial sequences. It is shown that the PTWP-computable functionals coincide with those definable in plus a constant for sequential minimisation. In particular, the functionals definable in denoted can be characterised by a subclass of PTWP-computable functionals denoted . Moreover, hierarchies of strictly increasing classes in the style of Heinermann and complexity classes are introduced such that . These results extend those for and PTWP [Nig94]. Finally, scvr is employed to define for each type the enumeration functional of all finite elements of . Received January 30, 1996     

A modal logic framework for reasoning about comparative distances and topology

We propose and investigate a uniform modal logic framework for reasoning about topology and relative distance in metric and more general distance spaces, thus enabling the comparison and combination of logics from distinct research traditions such as Tarski’s S4 for topological closure and interior, conditional logics, and logics of comparative similarity. This framework is obtained by decomposing the underlying modal-like operators into first-order quantifier patterns. We then show that quite a powerful and natural fragment of the resulting first-order logic can be captured by one binary operator comparing distances between sets and one unary operator distinguishing between realised and limit distances (i.e., between minimum and infimum). Due to its greater expressive power, this logic turns out to behave quite differently from both S4 and conditional logics. We provide finite (Hilbert-style) axiomatisations and ExpTime-completeness proofs for the logics of various classes of distance spaces, in particular metric spaces. But we also show that the logic of the real line (and various other important metric spaces) is not recursively enumerable. This result is proved by an encoding of Diophantine equations.     

The logic of justified belief,explicit knowledge,and conclusive evidence

We present a complete, decidable logic for reasoning about a notion of completely trustworthy (“conclusive”) evidence and its relations to justifiable (implicit) belief and knowledge, as well as to their explicit justifications. This logic makes use of a number of evidence-related notions such as availability, admissibility, and “goodness” of a piece of evidence, and is based on an innovative modification of the Fitting semantics for Artemov?s Justification Logic designed to preempt Gettier-type counterexamples. We combine this with ideas from belief revision and awareness logics to provide an account for explicitly justified (defeasible) knowledge based on conclusive evidence that addresses the problem of (logical) omniscience.     

Subrecursive functions on partial sequences

The paper studies a domain theoretical notion of primitive recursion over partial sequences in the context of Scott domains. Based on a non-monotone coding of partial sequences, this notion supports a rich concept of parallelism in the sense of Plotkin. The complexity of these functions is analysed by a hierarchy of classes similar to the Grzegorczyk classes. The functions considered are characterised by a function algebra generated by continuity preserving operations starting from computable initial functions. Its layers are related to those above by showing , thus generalising results of Schwichtenberg/Müller and Niggl. Received: 18 November 1996     

Cut elimination for a calculus with context-dependent rules

Context-dependent rules are an obstacle to cut elimination. Turning to a generalised sequent style formulation using deep inferences is helpful, and for the calculus presented here it is essential. Cut elimination is shown for a substructural, multiplicative, pure propositional calculus. Moreover we consider the extra problems induced by non-logical axioms and extend the results to additive connectives and quantifiers. Received: 11 April 1998 / Published online: 25 January 2001     

Construction of the circle in UniMath

We show that the type $\mathrm{T}\mathbb{Z}$ of $\mathbb{Z}$-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence Axiom and propositional truncation, yielding a stand-alone construction of the circle not using higher inductive types.     

A recursion-theoretic approach to NP

An implicit characterization of the class NP is given, without using any minimization scheme. This is the first purely recursion-theoretic formulation of NP.     

Information categories

Information systems have been introduced by Dana Scott as a convenient means of presenting a certain class of domains of computation, usually known as Scott domains. Essentially the same idea has been developed, if less systematically, by various authors in connection with other classes of domains. In previous work, the present authors introduced the notion of anI-category as an abstraction and enhancement of this idea, with emphasis on the solution ofdomain equations of the formD F(D), withF a functor. An important feature of the work is that we arenot confined to domains of computation as usually understood; other classes of spaces, more familiar to mathematicians in general, become also accessible. Here we present the idea in terms of what we callinformation categories, which are concrete I-categories in which the objects are structured sets of tokens and morphisms are relations between tokens. This is more in the spirit of information system work, and enables more specific results to be obtained. Following an account of the general theory, several examples are discussed in some detail: Stone spaces (as an ordinary mathematical example), Scott domains, SFP domains, and continuous bounded complete domains.