-
Towards a Generic Trace for Rule Based Constraint Reasoning
Authors:
Armando Gonçalves Da Silva Junior,
Pierre Deransart,
Luis-Carlos Menezes,
Marcos-Aurélio Almeida Da Silva,
Jacques Robin
Abstract:
CHR is a very versatile programming language that allows programmers to declaratively specify constraint solvers. An important part of the development of such solvers is in their testing and debugging phases. Current CHR implementations support those phases by offering tracing facilities with limited information. In this report, we propose a new trace for CHR which contains enough information to a…
▽ More
CHR is a very versatile programming language that allows programmers to declaratively specify constraint solvers. An important part of the development of such solvers is in their testing and debugging phases. Current CHR implementations support those phases by offering tracing facilities with limited information. In this report, we propose a new trace for CHR which contains enough information to analyze any aspects of \CHRv\ execution at some useful abstract level, common to several implementations. %a large family of rule based solvers. This approach is based on the idea of generic trace. Such a trace is formally defined as an extension of the $ω_r^\lor$ semantics of CHR. We show that it can be derived form the SWI Prolog CHR trace.
△ Less
Submitted 24 April, 2012;
originally announced April 2012.
-
Generic Traces and Constraints, GenTra4CP revisited
Authors:
Pierre Deransart
Abstract:
The generic trace format GenTra4CP has been defined in 2004 with the goal of becoming a standard trace format for the observation of constraint solvers over finite domains. It has not been used since. This paper defines the concept of generic trace formally, based on simple transformations of traces. It then analyzes, and occasionally corrects, shortcomings of the proposed initial format and shows…
▽ More
The generic trace format GenTra4CP has been defined in 2004 with the goal of becoming a standard trace format for the observation of constraint solvers over finite domains. It has not been used since. This paper defines the concept of generic trace formally, based on simple transformations of traces. It then analyzes, and occasionally corrects, shortcomings of the proposed initial format and shows the interest that a generic tracer may bring to develop portable applications or to standardization efforts, in particular in the field of constraints.
△ Less
Submitted 31 May, 2011;
originally announced May 2011.
-
Towards a Generic Framework to Generate Explanatory Traces of Constraint Solving and Rule-Based Reasoning
Authors:
Pierre Deransart,
Rafael Oliveira
Abstract:
In this report, we show how to use the Simple Fluent Calculus (SFC) to specify generic tracers, i.e. tracers which produce a generic trace. A generic trace is a trace which can be produced by different implementations of a software component and used independently from the traced component. This approach is used to define a method for extending a java based CHRor platform called CHROME (Constrai…
▽ More
In this report, we show how to use the Simple Fluent Calculus (SFC) to specify generic tracers, i.e. tracers which produce a generic trace. A generic trace is a trace which can be produced by different implementations of a software component and used independently from the traced component. This approach is used to define a method for extending a java based CHRor platform called CHROME (Constraint Handling Rule Online Model-driven Engine) with an extensible generic tracer. The method includes a tracer specification in SFC, a methodology to extend it, and the way to integrate it with CHROME, resulting in the platform CHROME-REF (for Reasoning Explanation Facilities), which is a constraint solving and rule based reasoning engine with explanatory traces.
△ Less
Submitted 13 January, 2010;
originally announced January 2010.
-
Observational semantics of the Prolog Resolution Box Model
Authors:
Pierre Deransart,
Mireille Ducassé,
Gérard Ferrand
Abstract:
This paper specifies an observational semantics and gives an original presentation of the Byrd box model. The approach accounts for the semantics of Prolog tracers independently of a particular Prolog implementation. Prolog traces are, in general, considered as rather obscure and difficult to use. The proposed formal presentation of its trace constitutes a simple and pedagogical approach for tea…
▽ More
This paper specifies an observational semantics and gives an original presentation of the Byrd box model. The approach accounts for the semantics of Prolog tracers independently of a particular Prolog implementation. Prolog traces are, in general, considered as rather obscure and difficult to use. The proposed formal presentation of its trace constitutes a simple and pedagogical approach for teaching Prolog or for implementing Prolog tracers. It is a form of declarative specification for the tracers. The trace model introduced here is only one example to illustrate general problems relating to tracers and observing processes. Observing processes know, from observed processes, only their traces. The issue is then to be able to reconstitute, by the sole analysis of the trace, part of the behaviour of the observed process, and if possible, without any loss of information. As a matter of fact, our approach highlights qualities of the Prolog resolution box model which made its success, but also its insufficiencies.
△ Less
Submitted 26 November, 2007;
originally announced November 2007.
-
Une sémantique observationnelle du modèle des boîtes pour la résolution de programmes logiques (version étendue)
Authors:
Pierre Deransart,
Mireille Ducassé,
Gérard Ferrand
Abstract:
This report specifies an observational semantics and gives an original presentation of the Byrd's box model. The approach accounts for the semantics of Prolog tracers independently of a particular implementation. Traces are, in general, considered as rather obscure and difficult to use. The proposed formal presentation of a trace constitutes a simple and pedagogical approach for teaching Prolog…
▽ More
This report specifies an observational semantics and gives an original presentation of the Byrd's box model. The approach accounts for the semantics of Prolog tracers independently of a particular implementation. Traces are, in general, considered as rather obscure and difficult to use. The proposed formal presentation of a trace constitutes a simple and pedagogical approach for teaching Prolog or for implementing Prolog tracers. It constitutes a form of declarative specification for the tracers. Our approach highlights qualities of the box model which made its success, but also its drawbacks and limits. As a matter of fact, the presented semantics is only one example to illustrate general problems relating to tracers and observing processes. Observing processes know, from observed processes, only their traces. The issue is then to be able to reconstitute by the sole analysis of the trace the main part of the observed process, and if possible, without any loss of information.
△ Less
Submitted 25 June, 2007; v1 submitted 21 June, 2007;
originally announced June 2007.
-
On using Tracer Driver for External Dynamic Process Observation
Authors:
Pierre Deransart
Abstract:
One is interested here in the observation of dynamic processes starting from the traces which they leave or those that one makes them produce. It is considered here that it should be possible to make several observations simultaneously, using a large variety of independently developed analyzers. For this purpose, we introduce the original notion of ``full trace'' to capture the idea that a proce…
▽ More
One is interested here in the observation of dynamic processes starting from the traces which they leave or those that one makes them produce. It is considered here that it should be possible to make several observations simultaneously, using a large variety of independently developed analyzers. For this purpose, we introduce the original notion of ``full trace'' to capture the idea that a process can be instrumented in such a way that it may broadcast all information which could ever be requested by any kind of observer. Each analyzer can then find in the full trace the data elements which it needs. This approach uses what has been called a "tracer driver" which completes the tracer and drives it to answer the requests of the analyzers. A tracer driver allows to restrict the flow of information and makes this approach tractable. On the other side, the potential size of a full trace seems to make the idea of full trace unrealistic. In this work we explore the consequences of this notion in term of potential efficiency, by analyzing the respective workloads between the (full) tracer and many different analyzers, all being likely run in true parallel environments. To illustrate this study, we use the example of the observation of the resolution of constraints systems (proof-tree, search-tree and propagation) using sophisticated visualization tools, as developed in the project OADymPPaC (2001-2004). The processes considered here are computer programs, but we believe the approach can be extended to many other kinds of processes.
△ Less
Submitted 17 January, 2007;
originally announced January 2007.
-
Rigorous design of tracers: an experiment for constraint logic programming
Authors:
Mireille Ducasse,
Ludovic Langevine,
Pierre Deransart
Abstract:
In order to design and implement tracers, one must decide what exactly to trace and how to produce this trace. On the one hand, trace designs are too often guided by implementation concerns and are not as useful as they should be. On the other hand, an interesting trace which cannot be produced efficiently, is not very useful either. In this article we propose a methodology which helps to effici…
▽ More
In order to design and implement tracers, one must decide what exactly to trace and how to produce this trace. On the one hand, trace designs are too often guided by implementation concerns and are not as useful as they should be. On the other hand, an interesting trace which cannot be produced efficiently, is not very useful either. In this article we propose a methodology which helps to efficiently produce accurate traces. Firstly, design a formal specification of the trace model. Secondly, derive a prototype tracer from this specification. Thirdly, analyze the produced traces. Fourthly, implement an efficient tracer. Lastly, compare the traces of the two tracers. At each step, problems can be found. In that case one has to iterate the process. We have successfully applied the proposed methodology to the design and implementation of a real tracer for constraint logic programming which is able to efficiently generate information required to build interesting graphical views of executions.
△ Less
Submitted 22 October, 2003;
originally announced October 2003.
-
HyperPro An integrated documentation environment for CLP
Authors:
AbdelAli Ed-Dbali,
Pierre Deransart,
Mariza A. S. Bigonha,
Jose de Siqueira,
Roberto da S. Bigonha
Abstract:
The purpose of this paper is to present some functionalities of the HyperPro System. HyperPro is a hypertext tool which allows to develop Constraint Logic Programming (CLP) together with their documentation. The text editing part is not new and is based on the free software Thot. A HyperPro program is a Thot document written in a report style. The tool is designed for CLP but it can be adapted t…
▽ More
The purpose of this paper is to present some functionalities of the HyperPro System. HyperPro is a hypertext tool which allows to develop Constraint Logic Programming (CLP) together with their documentation. The text editing part is not new and is based on the free software Thot. A HyperPro program is a Thot document written in a report style. The tool is designed for CLP but it can be adapted to other programming paradigms as well. Thot offers navigation and editing facilities and synchronized static document views. HyperPro has new functionalities such as document exportations, dynamic views (projections), indexes and version management. Projection is a mechanism for extracting and exporting relevant pieces of code program or of document according to specific criteria. Indexes are useful to find the references and occurrences of a relation in a document, i.e., where its predicate definition is found and where a relation is used in other programs or document versions and, to translate hyper-texts links into paper references. It still lack importation facilities.
△ Less
Submitted 19 November, 2001;
originally announced November 2001.
-
Prototy** CLP(FD) Tracers: a Trace Model and an Experimental Validation Environment
Authors:
Ludovic Langevine,
Pierre Deransart,
Mireille Ducasse,
Erwan Jahier
Abstract:
Develo** and maintaining CLP programs requires visualization and explanation tools. However, existing tools are built in an ad hoc way. Therefore porting tools from one platform to another is very difficult. We have shown in previous work that, from a fine-grained execution trace, a number of interesting views about logic program executions could be generated by trace analysis.
In this artic…
▽ More
Develo** and maintaining CLP programs requires visualization and explanation tools. However, existing tools are built in an ad hoc way. Therefore porting tools from one platform to another is very difficult. We have shown in previous work that, from a fine-grained execution trace, a number of interesting views about logic program executions could be generated by trace analysis.
In this article, we propose a trace model for constraint solving by narrowing. This trace model is the first one proposed for CLP(FD) and does not pretend to be the ultimate one. We also propose an instrumented meta-interpreter in order to experiment with the model. Furthermore, we show that the proposed trace model contains the necessary information to build known and useful execution views. This work sets the basis for generic execution analysis of CLP(FD) programs.
△ Less
Submitted 16 November, 2001;
originally announced November 2001.
-
Well-Typed Logic Programs Are not Wrong
Authors:
Pierre Deransart,
Jan-Georg Smaus
Abstract:
We consider prescriptive type systems for logic programs (as in Goedel or Mercury). In such systems, the ty** is static, but it guarantees an operational property: if a program is "well-typed", then all derivations starting in a "well-typed" query are again "well-typed". This property has been called subject reduction. We show that this property can also be phrased as a property of the proof-t…
▽ More
We consider prescriptive type systems for logic programs (as in Goedel or Mercury). In such systems, the ty** is static, but it guarantees an operational property: if a program is "well-typed", then all derivations starting in a "well-typed" query are again "well-typed". This property has been called subject reduction. We show that this property can also be phrased as a property of the proof-theoretic semantics of logic programs, thus abstracting from the usual operational (top-down) semantics. This proof-theoretic view leads us to questioning a condition which is usually considered necessary for subject reduction, namely the head condition. It states that the head of each clause must have a type which is a variant (and not a proper instance) of the declared type. We provide a more general condition, thus reestablishing a certain symmetry between heads and body atoms. The condition ensures that in a derivation, the types of two unified terms are themselves unifiable. We discuss possible implications of this result. We also discuss the relationship between the head condition and polymorphic recursion, a concept known in functional programming.
△ Less
Submitted 18 January, 2001; v1 submitted 20 December, 2000;
originally announced December 2000.
-
Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subty**
Authors:
Jan-Georg Smaus,
Francois Fages,
Pierre Deransart
Abstract:
We consider a general prescriptive type system with parametric polymorphism and subty** for logic programs. The property of subject reduction expresses the consistency of the type system w.r.t. the execution model: if a program is "well-typed", then all derivations starting in a "well-typed" goal are again "well-typed". It is well-established that without subty**, this property is readily ob…
▽ More
We consider a general prescriptive type system with parametric polymorphism and subty** for logic programs. The property of subject reduction expresses the consistency of the type system w.r.t. the execution model: if a program is "well-typed", then all derivations starting in a "well-typed" goal are again "well-typed". It is well-established that without subty**, this property is readily obtained for logic programs w.r.t. their standard (untyped) execution model. Here we give syntactic conditions that ensure subject reduction also in the presence of general subty** relations between type constructors. The idea is to consider logic programs with a fixed dataflow, given by modes.
△ Less
Submitted 18 January, 2001; v1 submitted 20 October, 2000;
originally announced October 2000.
