This page provides an implementation of a cost functions comparator as described in the following paper

Use the links to navigate to the relevant information

• Download
• Usage
• Syntax of Cost Functions
• Examples

Download

Download the file ub_checker.pl. It requires SWI-Prolog, but should work in any other Prolog system that provides a CLP(Q) library.

Usage

First load the checker into Prolog

?- use_module(ub_checker).
%  library(clpq) compiled into clpq 0.08 sec, 2,541 clauses
% ub_checker compiled into ub_checker 0.08 sec, 2,677 clauses
true.

Then, the main predicate used to compare two cost functions is ub_compare(+Exp1,+Exp2,+Phi,+Options,-Result) where

• Exp1 and Exp2 are cost functions that adhere to the syntax described in the Syntax section.
• Phi is a list of linear constraints [c1,c2,...] over the variables that appear in Exp1 and Exp2. The syntax of a linear constraint c_i is described in the Syntax section.
• Options is a list of options, where each element is of the form OptionName=Value. The different options are described below.
• Result is the output of the checker. It takes the value yes if the checker succeeds to prove that Exp1 =< Exp2 in the context Phi, and the value no otherwise.

The options available are:

• sum_alg: it controls how sums of products are compared. In its default value, i.e. general, the checker uses the algorithm in Definition 11. If it is set to basic, the checker uses the algorithm in Definition 9.
• check_strict_pos: it controls whether the checker verifies that cost functions are strictly positive. In its default value, i.e. no, this checked is skipped for efficiency although the result may not be correct for extreme cases. If it is set to yes, the checker attemps to verify that every basic cost expression is greater than or equal to 1, and that every product is greater than or equal to 1.
• pow_norm_scheme: it controls how power expressions are handled in the checker. In its default value, i.e., merge, expressions of the form nat(l)*nat(l) are merged into pow(nat(l),2). It it is set to the value split, expressions of the form pow(nat(l),2) are split into nat(l)*nat(l). By using split, the comparator can handle more cases, however, using merge the comparison is usually more efficient.

Syntax

A cost function e adheres to the following following syntax

 e :== n | nat(l) | e+e | e*e | log(a,nat(l)+1) | pow(a,nat(l)) | pow(nat(l),a) | max([e1,...,en]) | min([e1,...,en])

where n and a are non-negative integers such that n > 0 and a >= 2. The expression nat(l) stands for max(l,0) such that l is a linear expression that adheres to the following syntax

 l :== n | n*X | l+l

where n is an integer value and X is a Prolog variable (a sequence of letters, numbers or underscore such that it starts with an upper-case letter). A linear constraint c should adhere to the following syntax

 c :== l >= l | l =< l | l == l

Note that max can be use only when comparing upper bounds, and min only when comparing lower bounds. Mixing these expressions is not allowed.

Examples

?- compare_ubs(3*log(2,nat(A)+1),10*nat(B),[A>=4,B>=0,A+1==2],[],Res)
Res = yes

?- compare_ubs(max([nat(A),nat(B)]),nat(C),[C>=A,C>=B],[],Res)
Res = yes

?- compare_ubs(pow(nat(A),2),nat(B)*nat(C),[C>=A,B>=A,A>=0,B>=0,C>=0],[pow_norm_scheme=split],Res)
Res = yes

?- compare_ubs(min([nat(A),nat(B)]),nat(C),[C>=A,B>=2*C],[],Res)
Res = yes