Type systems are widely used in programming languages as a powerful tool providing safety to programs, and forcing the programmers to write code in a clearer way. functionallogic languages have inherited Damas & ...
详细信息
ISBN:
(纸本)9783642119989
Type systems are widely used in programming languages as a powerful tool providing safety to programs, and forcing the programmers to write code in a clearer way. functionallogic languages have inherited Damas & Milner type system from their functional part due to its simplicity and popularity. In this paper we address a couple of aspects that can be subject of improvement. One is related to a problematic feature of functionallogic languages not taken under consideration by standard systems: it is known that the use of opaque HO patterns in left-hand sides of program rules may produce undesirable effects from the point of view of types. We re-examine the problem, and propose a Damas & Milner-like type system where certain uses of HO patterns (even opaque) are permitted while preserving type safety, as proved by a subject reduction result that uses HO-let-rewriting, a recently proposed reduction mechanism for HO functionallogic programs. the other aspect is the different ways in which polymorphism of local definitions can be handled. At the same time that we formalize the type system, we have made the effort of technically clarifying the overall process of type inference in a whole program.
In this paper, we extend the well-known Naish's declarative debugging scheme for diagnosing wrong computed answers in first-order lazy functional-logic programs to the higher-order setting of the simply typed A-ca...
详细信息
ISBN:
(纸本)9783642119989
In this paper, we extend the well-known Naish's declarative debugging scheme for diagnosing wrong computed answers in first-order lazy functional-logic programs to the higher-order setting of the simply typed A-calculus, where programs are presented by conditional pattern rewrite systems. Our approach generalizes and combines declarative debugging techniques previously developed for less expressive declarative programming paradigms involving applicative rewrite rules instead of A-abstractions and decidable higher-order unification. Debugging starts withthe observation of a wrong computed answer which the user regards as incorrect w.r.t. an intended model that provides a declarative description of the program's semantics. Debugging proceeds by exploring an abridged proof tree built on a higher-order rewriting logic with A-abstractions that provides a purely declarative view of the computation. Finally, debugging ends withthe detection of a defined function rule in the program that is incorrect w.r.t. the intended model. We prove the logical correctness of the debugging method for any sound goal solving system whose computed answers are logical consequences of the program.
We discuss the realization of evaluation strategies for the concurrent constraint-based functional language ccfl within the translation schemata when compiling ccfl programs into the hierarchical graph rewriting langu...
详细信息
We discuss the realization of evaluation strategies for the concurrent constraint-based functional language ccfl within the translation schemata when compiling ccfl programs into the hierarchical graph rewriting language lmntal. the support of lmntal to express local computations and to describe the migration of processes and rules between local computation spaces allows a clear and simple encoding of typical evaluation strategies.
the proceedings contain 9 papers. the topics discussed include: from marriages to coalitions: a soft CSP approach;solving CSPs with naming games;an efficient decision procedure for functional decomposable theories bas...
ISBN:
(纸本)3642032508
the proceedings contain 9 papers. the topics discussed include: from marriages to coalitions: a soft CSP approach;solving CSPs with naming games;an efficient decision procedure for functional decomposable theories based on dual constraints;challenges in constraint-based analysis of hybrid systems;from rules to constraint programs withthe rules2CP modeling language;combining symmetry breaking and global constraints;iterative flattening search on RCPSP/max problems: recent developments;robust solutions in unstable optimization problem;and IDB-ADOPT: a depth-first search DCOP algorithm.
Some constraint problems have a combinatorial structure where the constraints allow the sequence of variables to be rotated (necklaces), if not also the domain values to be permuted (unlabelled necklaces), without get...
详细信息
Some constraint problems have a combinatorial structure where the constraints allow the sequence of variables to be rotated (necklaces), if not also the domain values to be permuted (unlabelled necklaces), without getting an essentially different solution. We bring together the fields of combinatorial enumeration, where efficient algorithms have been designed for (special cases of) some of these combinatorial objects, and constraintprogramming, where the requisite symmetry breaking has at best been done statically so far. We design the first search procedure and identify the first symmetry-breaking constraints for the general case of unlabelled necklaces. Further, we compare dynamic and static symmetry breaking on real-life scheduling problems featuring (unlabelled) necklaces. (C) 2008 Elsevier Inc. All rights reserved.
the proceedings contain 37 papers. the topics discussed include: functional interpretations of intuitionistic linear logic;fixed-point definability and polynomial time;Kleene's amazing second recursion theorem;jum...
ISBN:
(纸本)3642040268
the proceedings contain 37 papers. the topics discussed include: functional interpretations of intuitionistic linear logic;fixed-point definability and polynomial time;Kleene's amazing second recursion theorem;jumping boxes: representing Lambda-calculus boxes by jumps;tree-width for first order formulae;algorithmic analysis of array-accessing programs;decidable relationships between consistency notions for constraint satisfaction problems;cardinality quantifiers in MLO over trees;from coinductive proofs to exact real arithmetic;on the relation between sized-types based termination and semantic labelling;expanding the realm of systematic proof theory;intersection, universally quantified, and reference types;linear game automata: decidable hierarchy problems for stripped-down alternating tree automata;enriching an effect calculus with linear types;degrees of undecidability in term rewriting;upper bounds on stream I/O using semantic interpretations;and efficient type-checking for amortised heap-space analysis.
the proceedings contain 17 papers. the topics discussed include: a guide for manual construction of difference-list procedures;linear weighted-task-sum-scheduling prioritized tasks on a single resource;encoding of pla...
ISBN:
(纸本)3642006744
the proceedings contain 17 papers. the topics discussed include: a guide for manual construction of difference-list procedures;linear weighted-task-sum-scheduling prioritized tasks on a single resource;encoding of planning problems and their optimizations in linear logic;constraint-based timetabling system for the German University in Cairo;squash: a tool for analyzing, tuning and refactoring relational database applications;relational models for tabling logic programs in a database;integrating XQuery and logicprogramming;causal subgroup analysis for detecting confounding;using declarative specifications of domain knowledge for descriptive data mining;integrating temporal annotations in a modular logic language;visual generalized rule programming model for prolog with hybrid operators;and narrowing for first order functionallogic programs with call-time choice semantics.
We define an abstract pebble game that provides game interpretations for essentially all known consistency algorithms for constraint satisfaction problems including arc-consistency, (j, k)-consistency, k-consistency, ...
详细信息
ISBN:
(纸本)9783642040269
We define an abstract pebble game that provides game interpretations for essentially all known consistency algorithms for constraint satisfaction problems including arc-consistency, (j, k)-consistency, k-consistency, k-minimality, and refinements of arc-consistency such as peek arc-consistency and singleton arc-consistency. Our main result is that for any two instances of the abstract pebble game where the first satisfies the additional condition of being stacked, there exists an algorithm to decide whether consistency with respect to the first implies consistency with respect to the second. In particular, there is a decidable criterion to tell whether singleton arc-consistency with respect to a given constraint language implies k-consistency with respect to the same constraint language, for any fixed k. We also offer a new decidable criterion to tell whether arc-consistency implies satisfiability which pulls from methods in Ramsey theory and looks more amenable to generalization.
this paper introduces the COMPANION framework: a constraint-optimizing method for person-acceptable navigation. In this framework, human social conventions, such as personal space and tending to one side of hallways, ...
详细信息
this paper introduces the COMPANION framework: a constraint-optimizing method for person-acceptable navigation. In this framework, human social conventions, such as personal space and tending to one side of hallways, are represented as constraints on the robot's navigation. these constraints are accounted for at the global planning level. In this paper, we present the rationale for, and implementation of, this framework, and we describe the experiments we have run in simulation to verify that the method produces human-like behavior in a mobile robot. Our approach is novel in that it can express an arbitrary number of social conventions and explicitly accounts for these conventions in the planning phase.
暂无评论