Modeling linear logic with implicit functions

Just as intuitionistic proofs can be modeled by functions, linear logic proofs, being symmetric in the inputs and outputs, can be modeled by relations (for example, cliques in coherence spaces). However generic relations do not establish any functional dependence between the arguments, and therefore it is questionable whether they can be thought as reasonable generalizations of functions. On the other hand, in some situations (typically in differential calculus) one can speak in some precise sense about an implicit functional dependence defined by a relation. It turns out that it is possible to model linear logic with implicit functions rather than general relations, an adequate language for such a semantics being (elementary) differential calculus. This results in a non-degenerate model enjoying quite strong completeness properties.     

Tactics for Hierarchical Proof

There is something of a discontinuity at the heart of popular tactical theorem provers. Low-level, fully-checked mechanical proofs are large trees consisting of primitive logical inferences. Meanwhile, high-level human inputs are lexically structured formal texts which include tactics describing search procedures. The proof checking process maps from the high-level to low-level, but after that, explicit connections are usually lost. The lack of connection can make it difficult to understand the proof trees produced by successful tactic proofs, and difficult to debug faulty tactic proofs. We propose the use of hierarchical proofs, also known as hiproofs, to help bridge these levels. Hiproofs superimpose a labelled hierarchical nesting on an ordinary proof tree, abstracting from the underlying logic. The labels and nesting are used to describe the organisation of the proof, typically relating to its construction process. In this paper we introduce a foundational tactic language Hitac which constructs hiproofs in a generic setting. Hitac programs can be evaluated using a big-step or a small-step operational semantics. The big-step semantics captures the intended meaning, whereas the small-step semantics is closer to possible implementations and provides a unified notion of proof state. We prove that the semantics are equivalent and construct valid proofs. We also explain how to detect terms which are stuck in the small-step semantics, and how these suggest interaction points with debugging tools. Finally we show some typical examples of tactics, constructed using tactical combinators, in our language.     

Soft Constraint Logic Programming and Generalized Shortest Path Problems

In this paper we study the relationship between Constraint Programming (CP) and Shortest Path (SP) problems. In particular, we show that classical, multicriteria, partially ordered, and modality-based SP problems can be naturally modeled and solved within the Soft Constraint Logic Programming (SCLP) framework, where logic programming is coupled with soft constraints. In this way we provide this large class of SP problems with a high-level and declarative linguistic support whose semantics takes care of both finding the cost of the shortest path(s) and also of actually finding the path(s). On the other hand, some efficient algorithms for certain classes of SP problems can be exploited to provide some classes of SCLP programs with an efficient way to compute their semantics.     

From Lucid to TransLucid: Iteration, Dataflow, Intensional and Cartesian Programming

We present the development of the Lucid language from the Original Lucid of the mid-1970s to the TransLucid of today. Each successive version of the language has been a generalisation of previous languages, but with a further understanding of the problems at hand. The Original Lucid (1976), originally designed for purposes of formal verification, was used to formalise the iteration in while-loop programs. The pLucid language (1982) was used to describe dataflow networks. Indexical Lucid (1987) was introduced for intensional programming, in which the semantics of a variable was understood as a function from a universe of possible worlds to ordinary values. With TransLucid, and the use of contexts as firstclass values, programming can be understood in a Cartesian framework.      

On the equivalence between logic programming semantics and argumentation semantics

In the current paper, we re-examine the connection between formal argumentation and logic programming from the perspective of semantics. We observe that one particular translation from logic programs to instantiated argumentation (the one described by Wu, Caminada and Gabbay) is able to serve as a basis for describing various equivalences between logic programming semantics and argumentation semantics. In particular, we are able to show equivalence between regular semantics for logic programming and preferred semantics for formal argumentation. We also show that there exist logic programming semantics (L-stable semantics) that cannot be captured by any abstract argumentation semantics.     

An axiomatic semantics for nested concurrency

We give transformation rules for the concurrent parts of Hoare's language CSP, transforming concurrent CSP programs into nondeterministic, sequential programs.On the basis of these transformations we define an axiomatic semantics for CSP with nested concurrency.This axiomatic system includes a rule for binary, associative process composition, enabling modular verification dealing with parts of concurrent systems as well as full programs.The proof system is fully abstract, in the sense that the internal structure of processes is irrelevant in the specification inasmuch it is not externally observable.An outline of a verification of a recursive, concurrent sorter is given as an example.     

L.P.L. a fuzzy programming language: 1. Syntactic aspects

The L.P.L. language (Linguistic oriented Programming Language) that we shall present in this paper and in a forthcoming one is a new language aiming at an implementation of the concepts of the fuzzy sets theory. In the first paper, after an introduction to the basic concepts. we shall describe the syntactic aspects of L.P.L., i.e., the data declarations structure, the statements structure, the general structure of L.P.L. models. The second paper will deal first with the basic semantic and the semantics of logical expressions, then the semantics of basic statements as well as the semantics of the control structure of programs.     

Simd language design using prescriptive semantics

The goal of this article is to isolate a set of primitives necessary for the construction of SIMD programs and to give a denotational semantics for these primitives. The intent is to devise a language with a simple semantics rather than to propose a language which may be conveniently implemented. The approach taken results in the addition of a synchronous parallel assignment statement and a synchronous communication statement to the familiar sequential programming language control structures of composition, projection and iteration.     

Existence and asymptotical behavior of the minimizer of Hartree type equation with periodic potentials

ABSTRACT

In the present paper, we consider Hartree type equation with periodic potential. On the one hand, we prove the existence and nonexistence of the minimizer for the energy functional by using concentration-compactness lemma. On the other hand, we prove the energy estimates and describe the asymptotical behavior of the minimizer     

Quantaloids for Concurrency

S. Abramsky has introduced interaction categories as a new semantics for concurrent computation. We show that interaction categories can be naturally described in the language of quantaloids. More precisely, they are closely related to fix-points of a certain comonad on the category of quantaloids with biproducts.     

Computational adequacy for recursive types in models of intuitionistic set theory

This paper provides a unifying axiomatic account of the interpretation of recursive types that incorporates both domain-theoretic and realizability models as concrete instances. Our approach is to view such models as full subcategories of categorical models of intuitionistic set theory. It is shown that the existence of solutions to recursive domain equations depends upon the strength of the set theory. We observe that the internal set theory of an elementary topos is not strong enough to guarantee their existence. In contrast, as our first main result, we establish that solutions to recursive domain equations do exist when the category of sets is a model of full intuitionistic Zermelo–Fraenkel set theory. We then apply this result to obtain a denotational interpretation of FPC, a recursively typed lambda-calculus with call-by-value operational semantics. By exploiting the intuitionistic logic of the ambient model of intuitionistic set theory, we analyse the relationship between operational and denotational semantics. We first prove an “internal” computational adequacy theorem: the model always believes that the operational and denotational notions of termination agree. This allows us to identify, as our second main result, a necessary and sufficient condition for genuine “external” computational adequacy to hold, i.e. for the operational and denotational notions of termination to coincide in the real world. The condition is formulated as a simple property of the internal logic, related to the logical notion of 1-consistency. We provide useful sufficient conditions for establishing that the logical property holds in practice. Finally, we outline how the methods of the paper may be applied to concrete models of FPC. In doing so, we obtain computational adequacy results for an extensive range of realizability and domain-theoretic models.     

Constructive agents

Brouwer’s ideas of construction, proof, and inquiry in mathematics are more widely applicable. On a well-known philosophical view, intuitionistic logic is a general account of meaning and reasoning for natural language and epistemology. In this brief discussion piece, I go one step further, and discuss how intuitionistic semantics fits with information update and belief revision in agency. In the process, I define a number of new logical systems that give rise to several open problems.     

Infinitary S5-Epistemic Logic

It is known that a theory in S5-epistemic logic with several agents may have numerous models. This is because each such model specifies also what an agent knows about infinite intersections of events, while the expressive power of the logic is limited to finite conjunctions of formulas. We show that this asymmetry between syntax and semantics persists also when infinite conjunctions (up to some given cardinality) are permitted in the language. We develop a strengthened S5-axiomatic system for such infinitary logics, and prove a strong completeness theorem for them. Then we show that in every such logic there is always a theory with more than one model.     

Three time-based scale formulations for the two-stage lot sizing and scheduling in process industries

In this paper, we propose three novel mathematical models for the two-stage lot-sizing and scheduling problems present in many process industries. The problem shares a continuous or quasi-continuous production feature upstream and a discrete manufacturing feature downstream, which must be synchronized. Different time-based scale representations are discussed. The first formulation encompasses a discrete-time representation. The second one is a hybrid continuous-discrete model. The last formulation is based on a continuous-time model representation. Computational tests with state-of-the-art MIP solver show that the discrete-time representation provides better feasible solutions in short running time. On the other hand, the hybrid model achieves better solutions for longer computational times and was able to prove optimality more often. The continuous-type model is the most flexible of the three for incorporating additional operational requirements, at a cost of having the worst computational performance.     

A Functorial Framework for Constraint Normal Logic Programming

The semantic constructions and results for definite programs do not extend when dealing with negation. The main problem is related to a well-known problem in the area of algebraic specification: if we fix a constraint domain as a given model, its free extension by means of a set of Horn clauses defining a set of new predicates is semicomputable. However, if the language of the extension is richer than Horn clauses its free extension (if it exists) is not necessarily semicomputable. In this paper we present a framework that allows us to deal with these problems in a novel way. This framework is based on two main ideas: a reformulation of the notion of constraint domain and a functorial presentation of our semantics. In particular, the semantics of a logic program P is defined in terms of three functors: that apply to constraint domains and provide the operational, the least fixpoint and the logical semantics of P, respectively. To be more concrete, the idea is that the application of to a specific constraint solver provides the operational semantics of P that uses this solver; the application of to a specific domain provides the least fixpoint of P over this domain; and, the application of to a theory of constraints provides the logic theory associated to P. In this context, we prove that these three functors are in some sense equivalent.      

CTL AgentSpeak(L): A specification language for agent programs

This work introduces CTL AgentSpeak(L), a logic to specify and verify expected properties of rational agents implemented in the well-known agent oriented programming language AgentSpeak(L). Our approach is closely related to the BDICTL multi-modal logic, used to reason about agents in terms of their beliefs (B), desires (D), intentions (I), and the temporal logic CTL. A new interpretation for the temporal operators, grounded in the transition system induced by the operational semantics of AgentSpeak(L), is proposed. The main contribution of the approach is a better understanding of the relation between the programming language and its logical specification, enabling us to prove expected or desired properties for any agent programmed in the language, e.g., commitment strategies. The results, as well as the specification language proposed, are very useful to reconcile computational and philosophical aspects of practical reasoning, e.g., approaching single-minded commitment as a policy-based reconsideration case.     

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.     

The distribution semantics for normal programs with function symbols

The distribution semantics integrates logic programming and probability theory using a possible worlds approach. Its intuitiveness and simplicity have made it the most widely used semantics for probabilistic logic programming, with successful applications in many domains. When the program has function symbols, the semantics was defined for special cases: either the program has to be definite or the queries must have a finite number of finite explanations. In this paper we show that it is possible to define the semantics for all programs. We also show that this definition coincides with that of Sato and Kameya on positive programs. Moreover, we highlight possible approaches for inference, both exact and approximate.