Generally speaking,confluence property is not preserved when Term Rewriting Systems(TRSs) are combined,even if they are canonical.In this paper we give some sufficient conditions for ensuring the confluence property o...Generally speaking,confluence property is not preserved when Term Rewriting Systems(TRSs) are combined,even if they are canonical.In this paper we give some sufficient conditions for ensuring the confluence property of combined left-linear,overlapping TRSs.展开更多
We describe a modular rewriting system for translating optimization problems written in a domain-specific language(DSL)to forms compatible with low-level solver interfaces.Translation is facilitated by reductions,whic...We describe a modular rewriting system for translating optimization problems written in a domain-specific language(DSL)to forms compatible with low-level solver interfaces.Translation is facilitated by reductions,which accept a category of problems and transform instances of that category to equivalent instances of another category.Our system proceeds in two key phases:analysis,in which we attempt to find a suitable solver for a supplied problem,and canonicalization,in which we rewrite the problem in the selected solver’s standard form.We implement the described system in version 1.0 of CVXPY,a DSL for mathematical and especially convex optimization.By treating reductions as first-class objects,our method makes it easy to match problems to solvers well-suited for them and to support solvers with a wide variety of standard forms.展开更多
We define here the concept of head boundedness,head normal form and head confluence of term rewriting systems that allow infinite derivations.Head confluence is weaker than confluence,but suffi- cient to guarantee the...We define here the concept of head boundedness,head normal form and head confluence of term rewriting systems that allow infinite derivations.Head confluence is weaker than confluence,but suffi- cient to guarantee the correctness of lazy implementations of equational logic programming languages. Then we prove several results.First,if a left-linear system is locally confluent and head-bounded,then it is head-confluent.Second,head-confluent and head-bounded systems have the head Church-Rosser proper- ty.Last,if an orthogonal system is head-terminating,then it is bead-bounded.These results can be ap- plied to generalize equational logic programming languages.展开更多
基金This work was supported partly by The National Science FoundationThe Ministry of Electronic Industries and High Technology Program under The National Commission of Science & Technology.
文摘Generally speaking,confluence property is not preserved when Term Rewriting Systems(TRSs) are combined,even if they are canonical.In this paper we give some sufficient conditions for ensuring the confluence property of combined left-linear,overlapping TRSs.
文摘We describe a modular rewriting system for translating optimization problems written in a domain-specific language(DSL)to forms compatible with low-level solver interfaces.Translation is facilitated by reductions,which accept a category of problems and transform instances of that category to equivalent instances of another category.Our system proceeds in two key phases:analysis,in which we attempt to find a suitable solver for a supplied problem,and canonicalization,in which we rewrite the problem in the selected solver’s standard form.We implement the described system in version 1.0 of CVXPY,a DSL for mathematical and especially convex optimization.By treating reductions as first-class objects,our method makes it easy to match problems to solvers well-suited for them and to support solvers with a wide variety of standard forms.
基金The project is supported by the National Natural Science Foundation of China.
文摘We define here the concept of head boundedness,head normal form and head confluence of term rewriting systems that allow infinite derivations.Head confluence is weaker than confluence,but suffi- cient to guarantee the correctness of lazy implementations of equational logic programming languages. Then we prove several results.First,if a left-linear system is locally confluent and head-bounded,then it is head-confluent.Second,head-confluent and head-bounded systems have the head Church-Rosser proper- ty.Last,if an orthogonal system is head-terminating,then it is bead-bounded.These results can be ap- plied to generalize equational logic programming languages.
