Practical Aspects of Declarative Languages

Frontmatter

A Model Checker for Value-Passing Mu-Calculus Using Logic Programming

Abstract

Recent advances in logic programming have been successfully used to build practical verification toolsets, as evidenced by the XMC system. Thus far, XMC has supported value-passing process languages, but has been limited to using the propositional fragment of modal mucalculus as the property specification logic. In this paper, we explore the use of data variables in the property logic. In particular, we present valuepassing modal mu-calculus, its formal semantics and describe a natural implementation of this semantics as a logic program. Since logic programs naturally deal with variables and substitutions, such an implementation need not pay any additional price- either in terms of performance, or in complexity of implementation- for having the added flexibility of data variables in the property logic. Our preliminary implementation supports this expectation.

C. R. Ramakrishnan

Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog

Abstract

We describe practical experiences of using a logic programming based approach to model and reason about concurrent systems. We argue that logic programming is a good foundation for developing, prototyping, and animating new specification languages. In particular, we present the new high-level specification language CSP(LP), unifying CSP with concurrent (constraint) logic programming, and which we hope can be used to formally reason both about logical and concurrent aspects of critical systems.

Michael Leuschel

Frappé: Functional Reactive Programming in Java

Abstract

Functional Reactive Programming (FRP) is a declarative programming model for constructing interactive applications based on a continuous model of time. FRP programs are described in terms of behaviors (continuous, time-varying, reactive values), and events (conditions that occur at discrete points in time).

This paper presents Frappé, an implementation of FRP in the Java progamming language. The primary contribution of Frappé is its integration of the FRP event/behavior model with the Java Beans event/property model. At the interface level, any Java Beans component may be used as a source or sink for the FRP event and behavior combinators. This provides a mechanism for extending Frappé with new kinds of I/O connections and allows FRP to be used as a high-level declarative model for composing applications from Java Beans components. At the implementation level, the Java Beans event model is used internally by Frappé to propagate FRP events and changes to FRP behaviors. This allows Frappé applications to be packaged as Java Beans components for use in other applications, and yields an implementation of FRP well-suited to the requirements of event-driven applications (such as graphical user interfaces).

Antony Courtney

From Subject Directories to Subject Meta-directories via Declarative Programming

Abstract

Subject directories and search engines are the most commonly used tools to search for information on the World Wide Web. We propose a novel notion of subject meta-directory on top of standard subject directories, which strongly resembles the way in which metasearch engines extend standard search engines. After analyzing the main choices arising in the design of subject meta-directories, we describe the implementation of WebGate, a subject meta-directory entirely written in Prolog.

Antonio Brogi, Gianluca Caruso

Programming Goal-Driven Web Sites Using an Agent Logic Language

Abstract

In this paper we show how an agent programming language, based on a formal theory of actions, can be employed to implement adaptive web applications, where a personalized dynamical site generation is guided by the user’s needs. For this purpose, we have developed an on-line computer seller in DyLOG, a modal logic programming language which allows one to specify agents acting, interacting, and planning in dynamic environments. Adaptation at the navigation level is realized by dynamically building a presentation plan for solving the problem to assemble a computer, being driven by goals generated by interacting with the user. The planning capabilities of DyLOG are exploited to implement the automated generation of a presentation plan to achieve the goals. The DyLOG agent is the “reasoning” component of a larger system, called WLog, which is described in this paper.

Matteo Baldoni, Cristina Baroglio, Alessandro Chiarotto, Viviana Patti

High-Level Server Side Web Scripting in Curry

Abstract

We propose a new approach to program web services. Although we base our approach on the Common Gateway Interface (CGI) to ensure wide applicability, we avoid many of the drawbacks and pitfalls of traditional CGI programming by providing an additional abstraction layer implemented in the multi-paradigm declarative language Curry. For instance, the syntactical details of HTML and passing values with CGI are hidden by a wrapper that executes abstract HTML forms by translating them into concrete HTML code. This leads to a high-level approach to server side web service programming where notions like event handlers, state variables and control of interactions are available. Thanks to the use of a functional logic language, we can structure our approach as an embedded domain specific language where the functional and logic programming features of the host language are exploited to abstract from details and frequent errors in standard CGI programming.

Michael Hanus

Logic Programming Techniques for Dynamic VRML Web Content Generation

Abstract

We explore the use of a number of Logic Programming techniques for generating dynamic Web content and the underlying architecture and implementation issues. We describe a Prolog to VRML mapping allowing generation of dynamic VRML pages through CGI and server side Prolog scripts. BinProlog’s Assumption Grammars (a form of multi-stream DCGs with implicit arguments and temporary assertions, scoping over the current AND-continuation) are used to mimic VRML syntax and semantics directly, without using a preprocessor. The resulting generator allows quick development of integrated knowledge processing and data visualization Web applications. Using BinProlog’s multi-threaded networking primitives, we describe a design integrating in a self-contained Prolog application a Web Server, a Data Extraction module and an Assumption Grammar based VRML generator.

Anima Gupta, Paul Tarau

Soft Constraints for Security Protocol Analysis: Confidentiality

Abstract

We model any network configuration arising from the execution of a security protocol as a soft constraint satisfaction problem (SCSP). We formalise the protocol goal of confidentiality as a property of the solution for an SCSP, hence confidentiality always holds with a certain security level. The policySCSP models the network configuration where all admissible protocol sessions have terminated successfully, and an imputable SCSP models a given network configuration. Comparing the solutions of these two problems elicits whether the given configuration hides a confidentiality attack. We can also compare attacks and decide which is the most significant. The approach is demonstrated on the asymmetric Needham-Schroeder protocol.

Giampaolo Bella, Stefano Bistarelli

Secure Deductive Databases

Abstract

We show how deductive databases may be protected against unauthorized retrieval and update requests issued by authenticated users. To achieve this protection, a deductive database is expressed in an equivalent form that is guaranteed to permit only authorized actions. When a user poses a query Q on the protected form of a database, the user sees the subset of the answers for Q that they are permitted to know are true in the database; when a user’s update request is received, a minimal set of authorized changes the user is permitted to make to the database is performed. The authorized retrieval and update requests are specified using a security theory that is expressed in normal clause logic. The approach has a number of attractive technical results associated with it, and can be used to protect the information in any deductive database that is expressed in normal clause logic.

Steve Barker

Specifying Authentication Protocols Using Rewriting and Strategies

Abstract

Programming with rewrite rules and strategies has been already used for describing several computational logics. This paper describes the way the Needham-Schroeder Public-Key protocol is specified in ELAN, the system developed in Nancy to model and compute in the rewriting calculus. The protocol aims to establish a mutual authentication between an initiator and a responder that communicate via an insecure network. The protocol has been shown to be vulnerable and a correction has been proposed. The behavior of the agents and of the intruders as well as the security invariants the protocol should verify are naturally described by conditional rewrite rules whose application is controlled by strategies. Similar attacks to those already described in the literature have been discovered. We show how different strategies using the same set of rewrite rules can improve the efficiency in finding the attacks and we compare our results to existing approaches.

Horatiu Cirstea

Interoperability between Bioinformatics Tools: A Logic Programming Approach

Abstract

The goal of this project is to develop solutions to enhance interoperability between bioinformatics applications. Most existing applications adopt different data formats, forcing biologists into tedious translation work. We propose to use of Nexus as an intermediate representation language. We develop a complete grammar for Nexus and we adopt this grammar to build a parser. The construction heavily relies on the peculiar features of Prolog, to easily derive effective parsing and translating procedures. We also develop a general parse tree format suitable for interconversion between Nexus andot her formats.

Juan R. Iglesias, Gopal Gupta, Enrico Pontelli, Desh Ranjan, Brook Milligan

An A-Prolog Decision Support System for the Space Shuttle

Abstract

The goal of this paper is to test if a programming methodology based on the declarative language A-Prolog and the systems for computing answer sets of such programs, can be successfully applied to the development of medium size knowledge-intensive applications. We report on a successful design and development of such a system controlling some of the functions of the Space Shuttle.

Monica Nogueira, Marcello Balduccini, Michael Gelfond, Richard Watson, Matthew Barry

tuProlog: A Light-Weight Prolog for Internet Applications and Infrastructures

Abstract

Intelligence and interaction are two key -issues in the engineering of todaycomp lex systems, like Internet-based ones. To make logic languages accomplish their vocation of sound enabling technologies for intelligent components, we first need their implementations to strictly meet some engineering properties such as deployability, configurability, and scalability. Then, we should provide them with a wide range of interaction capabilities, according to standards and common practices. This would make logic-based systems also viable tools to build deployable, configurable, dynamic, and possibly intelligent infrastructures.

In this paper, we present tuProlog, a light-weight Java-based system allowing configurable and scalable Prolog components to be built and integrated into standard Internet applications according to a multiplicityof different interaction patterns, like JavaBeans, RMI, CORBA, and TCP/IP. Even more, tuProlog offers basic coordination capabilities in terms of logic tuple spaces, which allow complex Internet-based architectures to be designed and governed. This makes it possible to use tuProlog as the core enabling technologyf or Internet infrastructures - as in the case of the TuCSoN and LuCe infrastructures for the coordination of Internet-based multi-agent systems.

Enrico Denti, Andrea Omicini, Alessandro Ricci

A Novel Implementation of the Extended Andorra Model

Abstract

Logic programming is based on the idea that computation is controlled inference. The Extended Andorra Model provides a very powerful framework that supports both co-routining and parallelism. We present the BEAM, a design that builds upon David H. D.Warren’s original EAM with Implicit Control. The BEAM supports Warren’s original EAM rewrite rules plus eager splitting and sequential conjunctions. We discuss the main issues in the implementation of the BEAM and show that the EAM with Implicit Control can perform quite well when compared with other implementations that use the Andorra principle.

Ricardo Lopes, Vítor Santos Costa, Fernando Silva

Soundcheck for SQL

Abstract

The lion’s share of datalog features have been incorporated into the SQL3 standard proposal. However, most SQL manuals still recommend to implement user-defined conditions for data integrity nondeclaratively, by triggers or stored procedures. We describe how to implement known declarative database technology for integrity checking in SQL databases. We show how to represent and evaluate arbitrarily complex constraints in SQL without incurring major disadvantages usually associated to integrity checking in large databases. Error-prone procedural specification and laborious maintenance of integrity constraints is avoided by the declarativity of the specification language. The costs of evaluation is considerably reduced by an automated translation of declarative specifications to SQL triggers.

Hendrik Decker

Compiling High-Level Type Constructors in Constraint Programming

Abstract

We propose high-level type constructors for constraint programming languages, so that constraint satisfaction problems can be modelled in very expressive ways. We design a practical set constraint language, called esra, by incorporating these ideas on top of opl. A set of rewrite rules achieves compilation from esra into opl, yielding programs that are often very similar to those that a human opl modeller would (have to) write anyway, so that there is no loss in solving efficiency.

Pierre Flener, Brahim Hnich, Zeynep Kiziltan

Constraint Database Models Characterizing Timed Bisimilarity

Abstract

The problem of deciding timed bisimilarity has received increasing attention; it is important for verification of timed systems. Using a characterization of timed bisimilarity in terms of models of constraint databases, we present to our knowledge, the first local, symbolic algorithm for deciding timed bisimilarity; previous algorithms were based on a finite, but prohibitively large, abstraction (the region graph or the full backward stable graph). Our algorithm uses XSB-style tabling with constraints. Our methodology is more general than those followed in the previous approaches in the sense that our algorithm can be used to decide whether two timed systems are alternating timed bisimilar.

Supratik Mukhopadhyay, Andreas Podelski

Spatio-temporal Annotated Constraint Logic Programming

Abstract

We extend Temporal Annotated Constraint Logic Programming (TACLP) in order to obtain a framework where both temporal and spatial information can be dealt with and reasoned about. This results in a conceptually simple, uniform setting, called STACLP (Spatio-Temporal Annotated Constraint Logic Programming), where temporal and spatial data are represented by means of annotations that label atomic first- order formulae. The expressiveness and conciseness of the approach are illustrated by means of some examples: Definite, periodic and indefinite spatio-temporal information involving time-varying objects and properties can be handled in a natural way.

Alessandra Raffaetà, Thom Frühwirth

A Meta-heuristic for Subset Problems

Abstract

In constraint solvers, variable and value ordering heuristics are used to finetune the performance of the underlying search and propagation algorithms. However, few guidelines have been proposed for when to choose what heuristic among the wealth of existing ones. Empirical studies have established that this would be very hard, as none of these heuristics outperforms all the other ones on all instances of all problems (for an otherwise fixed solver). The best heuristic varies not only between problems, but even between different instances of the same problem. Taking heed of the popular dictum “If you can’t beat them, join them!” we devise a practical meta-heuristic that automatically chooses, at run-time, the “best” available heuristic for the instance at hand. It is applicable to an entire class of NP-complete subset problems.

Pierre Flener, Brahim Hnich, Zeynep Kiziltan

Construction and Optimization of a Parallel Engine for Answer Set Programming

Abstract

In this paper we study the use of parallelism to speed up execution of Answer Set Programs (ASP). ASP is an emerging programming paradigm which combines features from constraint programming, logic programming, and non-monotonic reasoning, and has found relevant applications in areas such as planning and intelligent agents. We propose different methodologies to parallelize execution of ASP programs, and we describe a prototype which exploits one form of parallelism.

Enrico Pontelli, Omar El-Khatib

FVision: A Declarative Language for Visual Tracking

Abstract

Functional programming languages are not generally associated with computationally intensive tasks such as computer vision. We show that a declarative programming language like Haskell is effective for describing complex visual tracking systems. We have taken an existing C++ library for computer vision, called XVision, and used it to build FVision (pronounced “fission”), a library of Haskell types and functions that provides a high-level interface to the lower-level XVision code. Using functional abstractions, users of FVision can build and test new visual tracking systems rapidly and reliably. The use of Haskell does not degrade system performance: computations are dominated by low-level calculations expressed in C++ while the Haskell “glue code” has a negligible impact on performance.

FVision is built using functional reactive programming (FRP) to express interaction in a purely functional manner. The resulting system demonstrates the viability of mixed-language programming: visual tracking programs continue to spend most of their time executing low-level image-processing code, while Haskell’s advanced features allow us to develop and test systems quickly and with confidence. In this paper, we demonstrate the use of Haskell and FRP to express many basic abstractions of visual tracking.

John Peterson, Paul Hudak, Alastair Reid, Greg Hager

A Most Specific Method Finding Algorithm for Reflection Based Dynamic Prolog-to-Java Interfaces

Abstract

In the context of direct and reflection based extension mechanisms for the Jinni 2000 Java based Prolog system, we discuss the design and the implementation of a reflection based Prolog to Java interface. While the presence of dynamic type information on both the Prolog and the Java sides allows us to automate data conversion between method parameters, the presence of subtyping and method overloading makes finding the most specific method corresponding to a Prolog call pattern fairly difficult. We describe a run-time algorithm which closely mimics Java’s own compile-time method dispatching mechanism and provides accurate handling of overloaded methods beyond the reflection package’s limitations. As an application of our interfacing technique, a complete GUI library is built in Prolog using only 10 lines of application specific Java code.

Satyam Tyagi, Paul Tarau

State Generation in the PARMC Model Checker

Abstract

The PARMC system performs modelc hecking for systems described in the XL language, a variant of CCS. Extending previous work by Dong and Ramakrishnan that compiled XL specifications into an optimized transition relation, we take their transition relation and compile it into S-code, producing instructions for a new lightweight engine S that was custom designed for PARMC. Difficult constructs are handled by the XSB logic programming engine, enabling both generality (from XSB) and speed (from S). States are maintained in a compressed representation, also improving memory utilization. Experiments were performed and showed that the anticipated speed and memory improvements were achieved.

Owen Kaser

Backmatter