Wyniki wyszukiwania - BazTech

1

Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms : Theory, Implementations, and Complexity

Frühwirth Thom

Fundamenta Informaticae

|

2020

|

Vol. 173, nr 4

253--283

EN

We present a concise source-to-source transformation that introduces justifications for user-defined constraints into the rule-based Constraint Handling Rules (CHR) programming language. There is no need to introduce a new semantics for justifications. This leads to a conservative extension of the language, as we can show the equivalence of rule applications. A scheme of two rules suffices to allow for logical retraction (deletion, removal) of CHR constraints during computation. Without the need to recompute from scratch, these rules remove the constraint and also undo all its consequences. We prove a confluence result concerning the rule scheme. We prove its correctness in general and tighten the results for confluent programs. We give an implementation, show its correctness, present two classical examples of dynamic algorithms, and improve the implementation. The computational overhead of introducing justifications and of performing logical retraction, i.e. the additional time and space needed, is proportional to the derivation length in the original program. This overhead may increase space complexity, but does not change the worst-case time complexity.

2

Active object design pattern

Górski Łukasz

Studia i Materiały Informatyki Stosowanej

|

2011

|

nr 5

21--24

EN

Parallelization of software plays nowadays a major role in software efficiency increase. The paper aims to present an active object design pattern and to point out its usefulness in parallel programs design. The ProActive system is also roughly presented, together with the implementation of discussed design pattern.

3

Church–Rosser Made Easy

Kozen D.

Fundamenta Informaticae

|

2010

|

Vol. 103, nr 1-4

129-136

EN

The Church–Rosser theorem states that the λ-calculus is confluent under β-reductions. The standard proof of this result is due to Tait and Martin-Löf. In this note, we present an alternative proof based on the notion of acceptable orderings. The technique is easily modified to give confluence of the βη-calculus.

4

Complexity of Normal Form Properties and Reductions for Term Rewriting Problems

Verma R.

Fundamenta Informaticae

|

2009

|

Vol. 92, nr 1-2

145-168

EN

We present several new and some significantly improved polynomial-time reductions between basic decision problems of term rewriting systems. We prove two theorems that imply tighter upper bounds for deciding the uniqueness of normal forms (UN^=) and unique normalization (UN^&rar;) properties under certain conditions. From these theorems we derive a new and simpler polynomial-time algorithm for the UN^= property of ground rewrite systems, and explicit upper bounds for both UN^= and UN! properties of left-linear right-ground systems. We also show that both properties are undecidable for right-ground systems. It was already known that these properties are undecidable for linear systems. Hence, in a sense the decidability results are "close" to optimal.

5

On the Influence of Confluence in Modal Logics

Gasquet O.

Fundamenta Informaticae

|

2006

|

Vol. 70, nr 3

227-250

EN

In this paper we prove that adding a confluence axiom to a modal logic which behaves rather well from the viewpoint of complexity of the satisfaction problem, drastically increases its complexity and blows it up from PSPACE-completeness to NEXPTIME-completeness. More precisely, we investigate here both monomodal K + confluence and bimodal K with confluence between the two modalities.

6

Explicit environments

Sato M, Sakurai T., Burstall R.

Fundamenta Informaticae

|

2001

|

Vol. 45, nr 1,2

79-115

EN

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.

7

Tableaux based decision procedures for modal logics of confluence and density

del Cerro L.F., Gasquet O.

Fundamenta Informaticae

|

1999

|

Vol. 40, Nr 4

317-333

EN

In this paper we present a decision procedures for modal logics with transitive models together with additionnal properties like confluence and density. These procedures are tableaux-based, and we show how to handle them in this well-known framework by generalizing usual tableaux (which are trees) to richer structures: directed acyclic graphs.