Skip to content

On This Page

  • REL
  • REFERENCE
  • Libraries
  • stdlib

The Standard Library (stdlib)

Broad collection of Rel relations that perform essential and commonly used tasks.

^Date

^Date[year in Int, month in Int, day in Int]

Create a Date from its three components: year, month and day. The three arguments are required to be Int64.

Definition

@infinite
def ^Date(year in Int, month in Int, day in Int, date in Date) =
    rel_primitive_construct_date(year, month, day, date)

^Date

^Date[dt in DateTime, tz in String]

Create a Date from a DateTime, with timezone tz.

The timezone argument is necessary for the Date because DateTime is an instant of time that is timezone independent. For different locations on earth (timezones), a DateTime has different dates.

Definition

@infinite
def ^Date(instant in DateTime, tz in String, date in Date) =
    rel_primitive_datetime_date_convert(instant, tz, date)

^DateTime

^DateTime[year, month, day, hour, minute, second, millisecond, tz in String]

Create a DateTime from a year, month, day, hour, minute, second, and millisecond.

The timezone argument tz is necessary to correctly interpret what instant in time this is.

There can be multiple DateTime values for one set of arguments: for example, with the ending of daylight saving time at 2am, every time between 1am and 2am occurs twice and has two corresponding instants of time.

For part values that are out of range, there are no tuples (there is no error).

Definition

@infinite
def ^DateTime(
    year in Int, month in Int, day in Int,
    hour in Int, minute in Int, second in Int, millisecond in Int,
    tz in String, instant in DateTime) =
    rel_primitive_construct_datetime(
        year, month, day, hour, minute, second, millisecond, tz, instant)

^DateTime

^DateTime[date, hour, minute, second, millisecond, tz in String]

Create a DateTime from a date, hour, minute, second, and millisecond.

This constructor uses the year, month, and day from the date and then constructs a DateTime in the same way as the constructor with all parts as arguments.

Definition

@infinite
def ^DateTime(
    date in Date,
    hour in Int, min in Int, sec in Int, ms in Int,
    tz in String, instant in DateTime) =
    exists(year in Int, month in Int, day in Int:
        date_year(date, year) and
        date_month(date, month) and
        date_day(date, day) and
        ^DateTime(year, month, day, hour, min, sec, ms, tz, instant))

^DateTime

^DateTime[year, month, day, tz in String]

Create a DateTime for the given year, month, and day, with the time components all set to

  1. The resulting DateTime is the first millisecond for the given date and timezone tz.

See the ^DateTime constructor with time components as arguments for more details.

Definition

@infinite
def ^DateTime(year in Int, month in Int, day in Int, tz in String, instant in DateTime) =
    ^DateTime(year, month, day, 0, 0, 0, 0, tz, instant)

^DateTime

^DateTime[date in Date, tz in String]

Create a DateTime for the given Date, with the time components all set to

  1. The resulting DateTime is the first millisecond of the given Date and timezone tz.

See the ^DateTime constructor with time components as arguments for more details.

Definition

@infinite
def ^DateTime(date in Date, tz in String, instant in DateTime) =
    exists(year in Int, month in Int, day in Int:
        date_year(date, year) and
        date_month(date, month) and
        date_day(date, day) and
        ^DateTime(year, month, day, tz, instant))

abs

abs[x]

The absolute value of x.

Examples:

abs[-2] = 2
abs[-2.0] = 2.0

Definition

@inline
def abs[x] = rel_primitive_abs[x]

acos

acos[x]

Inverse cosine (in radians).

Defined for x between -1 and 1 (inclusive).

Example:

acos[0] = 1.5707963267948966

Definition

@inline
def acos[x] = rel_primitive_acos[x]

acosh

acosh[x]

Inverse hyperbolic cosine.

Defined for x >= 1.

Definition

@inline
def acosh[x] = rel_primitive_acosh[x]

acot

acot[x]

Inverse cotangent (in radians).

Definition

@inline
def acot[x] = rel_primitive_acot[x]

add

add[x, y]
add(x, y, s)
x + y

Addition of two numbers. Addition of a DateTime/Date x with a time duration y.

Parameters

Numeric data

ParameterTypeDescription
xNumericA number.
yNumericA number.
sNumericThe sum of x and y.

Note: Not all numeric values can be mixed with each other, but 64-bit integers can be mixed with any other numeric data type.

Time data

ParameterTypeDescription
xTimestamp/periodA DateTime, Date, or date/time period.
yTime periodA date/time period.
sTimestamp/periodA DateTime or Date. Same type as x.

Note:

  • If x is a date, y needs to be a date period.
  • If x is a date/time period, y needs to be of the same type.

Explanation

Addition evaluates the sum of x and y and assigns it to s. In procedural languages, usually x and y are given. In Rel–-a declarative language–-addition can be thought of as a mapping where x and y are the keys and s is the value, which is functionally dependent on x and y.

However, with addition–-add(x, y, s)–-it is sufficient to know any two of the three arguments. The third one can always be inferred. Usually x and y are given, but knowing x and s is enough to infer y.

In Rel, this means two of the three arguments need to be grounded. Valid grounding combinations are as follows:

  • x and y
  • x and s
  • y and s

Examples

Addition of Numbers

Add two integers using +:

def output = 1 + 2
//output> 3

Add an integer and a float using add:

def output = add[1, 2.5]
//output> 3.5

Add two floats using full expression:

def output(x) = add(1.7, 2.8, x)
//output> 4.5

Add integer to a rational:

def output = 1 + rational[16][2, 3]
//output> 5/3

Addition of time

Add time to a timestamp:

def output:tomorrow = datetime_now + Day[1]
def output:next_hour = datetime_now + Hour[1]

Add weeks to a date:

def output = 2022-12-24 + Week[2]
//output> 2023-01-07

Add seconds together:

def output = Second[1] + Second[2]
//output> 3

See Also

subtract, divide, multiply

Definition

@inline
def add(x, y, z) = rel_primitive_add(x, y, z)
 
 
@inline
def (+)(x, y, z) = add(x, y, z)

Any

Any(x)

Holds for any x, where x exists. (Any functions as a wildcard.)

Example:

Integrity constraint that tests whether x is of any type:

def R = (1, 3) ; (1, "foo")
 
ic any_ic {subset(R, (Int, Any) )}

Definition

@inline
def Any(x) = true

approx_eq

approx_eq(tolerance, x, y)

Approximate equality. Use to compare scalar numbers and check if x and y are within the absolute tolerance (tolerance) of each other.

Parameters

ParameterTypeDescription
toleranceInt64 or Float64.A positive number of type Int64 or Float64.
xNumberA valid number. Must be the exact same data type as y.
yNumberA valid number. Must be the exact same data type as x.

Explanation

“approximately equal” is defined as number values being within the absolute tolerance (tolerance) of each other, or non-number values being equal.

The parameter tolerance stands for the absolute tolerance and must be of type Int64 or Float64. Also, tolerance must be a positive number; negative numbers will return false

x and y should be of the exact same data type. For example, x and y can be of type Decimal or Rational, but types must have the same bits and precision.

If x or y is not a number, approx_eq defaults to eq.

Examples

Approximate equality determined as true:

def output = approx_eq(0.05, 0.1, 0.15)
//output> () // () = true

Approximate equality determined as false:

def output = approx_eq(0.01, 0.1, 0.15)
//output>    // false

See Also

equal, eq, approx_equal, full_relation_approx_equal

Definition

@inline
def approx_eq(tolerance, x in Number, y in Number) = abs[x - y] <= abs[tolerance]
 
@inline
def approx_eq(tolerance, x, y) = eq(x, y)

approx_equal

approx_equal(tolerance, R, S)

Approximate relational equality. To hold true, the values in the last column of R must be approximately equal to values in the last column of S given the same key (prefix).

Parameters

ParameterTypeDescription
toleranceInt64 or Float64.A positive number of type Int64 or Float64.
RRelationA relation with corresponding keys and last arguments that can be compared to S.
SRelationA relation with corresponding keys and last arguments that can be compared to R.

Explanation

Two relations R and S are considered “relationally approximately equal” when for each tuple (k..., x) in S there exists a tuple (k..., y) in R where x and y are considered approximately equal. This approximate equality is symmetric and holds equally true when the places of R and S are swapped.

See approx_eq for the details about approximate equality between two data values.

The parameter tolerance stands for the absolute tolerance and must be of type Int64 or Float64. tolerance must be a positive number; negative numbers will evaluate to false.

Keys must match for approx_equal to be true.

All values of the last column in R and S must be of the exact same data type. For example, the values can all be of type Decimal or Rational, but types must have the same bits and precision. Otherwise, approx_equal evaluates to false.

Note the correspondence between approx_equal and equal : approx_equal(0, R, S) if and only if equal(R, S).

approx_equal applies only to the values in the last column in R and S. That is, if the values are not within tolerance, approx_equal will evaluate to false even if other arguments in the relations are within tolerance. If full relation comparison functionality is required, see full_relation_approx_equal.

Examples

Approximate relational equality determined as true:

def salary1 = {("John", 10.0) ; ("Mary", 20.0); ("Paul", 17.0) ; ("Peter", 15.0) }
def salary2 = {("John", 9.99) ; ("Mary", 20.01); ("Paul", 17.0) ; ("Peter", 15.0) }
 
def output = approx_equal(0.1, salary1, salary2)
//output> () //true

Approximate relational equality determined as false:

def salary1 = {("John", 10.0) ; ("Mary", 20.0); ("Paul", 17.0) ; ("Peter", 15.0) }
def salary2 = {("John", 11.0) ; ("Mary", 21.0); ("Paul", 17.0) ; ("Peter", 15.0) }
 
def output = approx_equal(0.1, salary1, salary2)
//output>   //false

Approximate relational equality determined as false because keys are different:

def salary1 = {("John", 10.0) ; ("Mary", 20.0); ("Paul", 17.0) ; ("Peter", 15.0) }
def salary3 = {("John", 9.99) ; ("Ben", 20.0); ("Paul", 17.0) ; ("Peter", 15.0) }
 
def output = approx_equal(0.1, salary1, salary3)
//output>   //false

Approximate relational equality determined as false, even though the first arguments are within tolerance:

def coordinates1 = (1.0, 2.0); (3.0, 6.0)
def coordinates2 = (1.0000001, 2.0); (2.9999999, 6.0000001)
 
def output = approx_equal(0.001, coordinates1, coordinates2)
//output>   //false

See Also

full_relation_approx_equal, approx_eq, equal, eq

Definition

@inline
def approx_equal(tolerance, R, S) =
    forall(k..., x where R(k..., x): count[R[k...]] = count[S[k...]] and
        exists(y where S(k..., y): approx_eq(tolerance, x, y))
    ) and
    forall(k..., x where S(k..., x): count[S[k...]] = count[R[k...]] and
        exists(y where R(k..., y): approx_eq(tolerance, x, y))
    )

argmax

argmax[R]

Find the keys for the largest value of the relation R.

Examples:

def output = argmax[{(2, 3); (1, 6)}]
1
 
def output = argmax[{(2, 6); (1, 6); (5, 0)}]
1
2
 
// find the teams with the largest aggregated salary:
argmax[d in team: sum[salary[p] for p in member[d]]]

Definition

@inline
def argmax[R] = R.(max[R])

ArgMax

ArgMax[R]

Please use argmax[R]. Deprecates in near future

Definition

@inline
def ArgMax = argmax

argmin

argmin[R]

Find the keys for the smallest value of the relation R.

Examples:

def output = argmin[{(2, 3); (1, 6)}]
2
 
def output = argmin[{(2, 6); (1, 6); (5, 10)}]
1
2
 
// find the teams with the smallest aggregated salary:
argmin[d in team: sum[salary[p] for p in member[d]]]

Definition

@inline
def argmin[R] = R.(min[R])

ArgMin

ArgMin[R]

Please use argmin[R]. Deprecates in near future

Definition

@inline
def ArgMin = argmin

arity

arity[R]

The arity of a relation. In some cases, it can be an over-approximation.

Arity is a higher-order relation that is always evaluated at compile-time.

Examples:

def output = arity[3]
1
def output = arity[{1; 2; 3}]
1
def output = arity[(1, 2)]
2
def output = arity[add]
3
def output = arity[{1; 2; (1,2)}]
1
2

Arity can be used to do meta-programming in logic. For example, the following abstraction verbalize implements specific cases using arity.

Examples:

@inline def verbalize[R] = "nullary", arity[R] = 0;
                            "unary", arity[R] = 1;
                            "binary", arity[R] = 2
def output = verbalize[true]
"nullary"
def output = verbalize[1]
"unary"

Arity can be used in higher-order abstractions to check at compile-time that they are used correctly.

Arity can be used in integrity constraints to state expectation on EDB or IDB relations. Because arity is evaluated at compile-time, it can catch mistakes in the logic before the logic executes.

Example:

def p = 1,2,3
ic { arity[p] = 3 }

Note that there is a difference between R(_, _) and arity(R) = 2. The first requires R to be non-empty, which is an runtime property of R.

Definition

@inline
def arity[R] = rel_primitive_arity[R]

asin

asin[x]

Inverse sine (in radians).

Defined for x between -1 and 1 (inclusive).

Example:

asin[1] = 1.5707963267948966

Definition

@inline
def asin[x] = rel_primitive_asin[x]

asinh

asinh[x]

Inverse hyperbolic sine.

Definition

@inline
def asinh[x] = rel_primitive_asinh[x]

atan

atan[x]

Inverse tangent (in radians).

Defined for x between -1 and 1 (inclusive).

Definition

@inline
def atan[x] = rel_primitive_atan[x]

atan2

atan2[y, x]

Inverse tangent: an angle (in radians) between the positive x-axis and the ray to the point (x, y).

Definition

@inline
def atan2[x,y] = rel_primitive_atan2[x,y]

atanh

atanh[x]

Inverse hyperbolic tangent.

Definition

@inline
def atanh[x] = rel_primitive_atanh[x]

auto_number

auto_number[R]

DEPRECATED

This function is deprecated and should be avoided. It will be removed soon.

AutoNumber a relation.

auto_number takes a relation R(xs...) and produces a relation R(xs..., i) where i is a distinct AutoNumberValue index.

Note that auto_number can give different results each time it is called.

Example:

def sample = 'a'
def output = auto_number[sample]
('a', AutoNumberValue(0x12))
 
def sample = {'a'; 'b'; 'c'}
def output = auto_number[sample]
('a', AutoNumberValue(0x132))
('b', AutoNumberValue(0x133))
('c', AutoNumberValue(0x134))

Definition

@inline
def auto_number = rel_primitive_auto_number

AutoNumber

AutoNumber(x)

DEPRECATED

This function is deprecated and should be avoided. It will be removed soon.

Test if the given value is an AutoNumberValue.

Definition

@inline
def AutoNumber = rel_primitive_AutoNumberValue

average

mean[R]
average[R]

The arithmetic mean of (the last argument of) the relation R, if non-empty. False if R is empty.

Definition

@inline
def average = mean

bitwise_and

bitwise_and[x, y]

Bitwise and of two integers.

Example:

bitwise_and[3,2] = 2
bitwise_and[0x10011, 0x11100] = 0x00010000

Definition

@inline
def bitwise_and[x, y] = rel_primitive_bitwise_and[x, y]

bitwise_left_shift

bitwise_left_shift[x, n]

Bitwise left shift of an integer x by n bits.

Examples:

bitwise_left_shift[8, 1] = 16
bitwise_left_shift[1, 10] = 1024
bitwise_left_shift[0xF, 1] = 0x1d

Definition

@inline
def bitwise_left_shift[x, n] = rel_primitive_bitwise_left_shift[x, n]

bitwise_not

bitwise_not[x]

Bitwise not of an integer.

Examples:

bitwise_not[8] = -9
bitwise_not[-9] = 8
bitwise_not[0x00011] = 0xffffffee

Definition

@inline
def bitwise_not[x] = rel_primitive_bitwise_not[x]

bitwise_or

bitwise_or[x, y]

Bitwise or of two integers.

Example:

bitwise_or[3, 2] = 3
bitwise_or[0x00011, 0x11100] = 0x00011111

Definition

@inline
def bitwise_or[x, y] = rel_primitive_bitwise_or[x, y]

bitwise_right_shift

bitwise_right_shift[x, n]

Bitwise right shift of an integer x by n bits while preserving the sign.

Examples:

bitwise_right_shift[1024, 1] = 512
bitwise_right_shift[-1024, 1] = -512

Definition

@inline
def bitwise_right_shift[x, n] = rel_primitive_bitwise_signed_right_shift[x, n]

bitwise_unsigned_right_shift

bitwise_unsigned_right_shift[x,n]

Bitwise right shift of an integer by n bits.

Examples:

bitwise_unsigned_right_shift[8, 1] = 4
bitwise_unsigned_right_shift[-8, 1] = 9223372036854775804

Definition

@inline
def bitwise_unsigned_right_shift[x, n] = rel_primitive_bitwise_unsigned_right_shift[x, n]

bitwise_xor

bitwise_xor[x, y]

Bitwise xor of two integers.

Example:

bitwise_xor[3, 2] = 1
bitwise_xor[0x00011, 0x11100] = 0x00011111

Definition

@inline
def bitwise_xor[x, y] = rel_primitive_bitwise_xor[x, y]

Boolean

Boolean(x)

Holds if x is a Boolean.

Example:

def json = parse_json["""{"a": true, "b": false}"""]
def output(x) = json(:a, x) and Boolean(x)

Definition

@inline
def Boolean = rel_primitive_Boolean

boolean_and

boolean_and(x, y, z)

Logical AND operator for the Boolean data type.

Example:

def output(x, y, z) = boolean_and(x, y, z) and boolean_true(z)

Definition

@inline
def boolean_and(x in Boolean, y in Boolean, z in Boolean) =
    if boolean_true(x) and boolean_true(y) then
        boolean_true(z)
    else
        boolean_false(z)

boolean_false

boolean_false(x)

Holds if x is a Boolean of value false.

Definition

@inline
def boolean_false = rel_primitive_boolean_false

boolean_not

boolean_not(x,y)

Negation(not) operator for the Boolean data type. Example:

def output(x, y) = boolean_not(x, y) and boolean_false(x)

Definition

@inline
def boolean_not(x in Boolean, y in Boolean) =
    if boolean_true(x) then
        boolean_false(y)
    else
        boolean_true(y)

boolean_or

boolean_or(x, y, z)

Logical or operator for the Boolean data type. Example:

def output(x, y, z) = boolean_or(x, y, z) and boolean_false(z)

Definition

@inline
def boolean_or(x in Boolean, y in Boolean, z in Boolean) =
    if boolean_false(x) and boolean_false(y) then
        boolean_false(z)
    else
        boolean_true(z)

boolean_true

boolean_true(x)

Holds if x is a Boolean of value true.

Definition

@inline
def boolean_true = rel_primitive_boolean_true

bottom

bottom[k, R]

Select the bottom k facts of relation R according to the sort order of R.

bottom is reverse_sort (which sorts highest to lowest) restricted to the first k facts.

Example:

def output =  bottom[2, {'a'; 'b'; 'c'; 'd'}]
(1, 'd')
(2, 'c')

Definition

@inline
def bottom[k, R] =
    reverse_sort[R][i] for i where i <= k

byte

byte[str]
byte[str, i]
byte(str, i, b)

Indexes into a string at byte position i, mapping each position i to a byte b, as a UInt8 value.

If a string contains Unicode characters, the byte at index i might be only a partial character. Be careful with your indexing logic.

Both i and b can be optionally bound externally. When only str is bound, this is the mapping from each index to its corresponding byte.

Examples: Indexing into a known byte index:

byte["abcd", 2] = 0x62
byte["中文例子", 2] = 0xb8

Abstracting over the byte index:

equal(byte["中文"],
        { 1, 0xe4;
          2, 0xb8;
          3, 0xad;
          4, 0xe6;
          5, 0x96;
          6, 0x87; })
equal((i : byte["awesome", i](0x65)), {3; 7})

Definition

@inline
def byte[s](i, b) =
    rel_primitive_byte(s, i, b) and range[1, num_bytes[s], 1](i)

capture_group_by_index

capture_group_by_index[regex, input_string, offset]

A set of capture groups, each of the form (index, substring), where index is the capture group index, and substring is the first regex match in input_string, starting at the character index specified by offset. regex can be a string or a pattern.

Offsets (character indexes) start at 1.

Example:

capture_group_by_index["(\\d+):(\\d+)",
    "Appointment from  12:45 to 1:30",
    19]

is equal to

{(1, "12"); (2, "45")}

Definition

@inline
def capture_group_by_index[re, str, offset](idx, capture) =
    rel_primitive_capture_grp[regex_compile[re], str, offset](idx, capture)

capture_group_by_name

capture_group_by_name[regex, input_string, offset]

A set of capture groups, each of the form (name, substring), where name is the capture group name, and substring is the first regex match in input_string, starting at the character index specified by offset. regex can be a string or a pattern.

Offsets (character indexes) start at 1.

Each capture group should have a unique name.

Example:

capture_group_by_name["(?<hour>\\d+):(?<minute>\\d+)",
    "Appointment from 12:45 to 1:30",
    19]

is equal to

(("hour","12"); ("minute","45"))

Definition

@inline
def capture_group_by_name[re, str, offset](name, capture) =
    exists( idx: rel_primitive_capture_grp[regex_compile[re], str, offset](idx, capture)
            and rel_primitive_capture_names(regex_compile[re], idx, name))

cart

cart[R, S]
R × S

Cartesian product.

Examples:

def output = 1 ✕ 2
(1,2)
def output = {1; 2} ✕ {3; 4}
(1,3)
(1,4)
(2,3)
(2,4)

Definition

@inline
def cart[R, S](x..., y...) = R(x...) and S(y...)
 
@inline
def (×) = cart

cbrt

cbrt[x]

The cube root of x.

Example:

cbrt[27] = 3.0

Definition

@inline
def cbrt[x] = rel_primitive_cbrt[x]

ceil

ceil[x]

Round up to the nearest integer.

Examples:

ceil[4.5] = 5.0
ceil[-4.5] = -4.0
ceil[4] = 4

Definition

@inline
def ceil[x] = round[:ROUND_UP, x]

char

char[str]
char[str, i]
char(str, i, c)

Indexes into a string at (Int) position i, mapping each index i to the i-th character, c.

Since this is indexed using character positions, the characters will always be whole Unicode characters.

A character is also known as a “Code Point” in the Unicode specification.

Both i and c can be optionally bound externally. When only str is bound, this is the mapping from each character index to its corresponding character.

Examples:

Indexing into a known character index:

char["abcd", 2] = 'b'
char["中文例子", 2] = '文'

Abstracting over the character index:

equal(char["中文"],
        { 1, "中"; 2, "文" })
equal((i : char["awesome", i]('e')), {3; 7})

Definition

@inline
def char[s](i, c) =
    rel_primitive_char(s, i, c) and range[1, num_chars[s], 1](i)

Char

Char(x)

Holds if x is of type Char, which has a Unicode character as its value and is specified with single quotes.

Examples:

Integrity constraint that tests whether x is of type Char:

def R = 't'
 
ic mychar_ic(x in R)
    Char(x)
}

Schema defined in a relation using Char:

def myrelation(x in Char, y in Int) {
    x = 'a' and y = 123
}
 
def output = myrelation
//output> (a, 123)

Definition

@inline
def Char = rel_primitive_Char

clamp

clamp[lo, hi, v]

clamp limits the value v to a given range(lo, hi), changing values outside the range to the closest lo, hi value if necessary. The arguments should have the same type.

Examples:

clamp[2, 5, 1] = 2
clamp[2, 5, 6] = 5
clamp[2, 5, 3] = 3

Definition

@inline
def clamp[lo, hi, v] = min[{max[{lo; v}]; hi}]

complement

complement[R]

The complement of the relation R.

Definition

@inline
def complement[R](x...) = not R(x...)

concat

concat[val1, val2]

String concatenation of two arbitrary values

Example:

concat["a", "b"] = "ab"
concat["a", 'b'] = "ab"
concat['a', "b"] = "ab"
concat['a', 'b'] = "ab"
concat["a_", 1] = "a_1"
concat[1, 3.14] = "13.14"

Definition

@inline
def concat[x, y] = rel_primitive_concat[string[x], string[y]]

contains

contains(s, substring)

True iff the second argument, substring, occurs as a substring in the first argument, s.

Examples:

contains("Rel is cool!", "Rel is cool!")        // true
contains("Rel is cool!", " is coo")             // true
contains("Rel is cool!", 'c')                   // true
contains("Rel is cool!", 'C')                   // false

Definition

@inline
def contains = rel_primitive_contains

cos

cos[x]

Cosine of x (given in radians).

Defined for non-infinite x.

Example:

cos[pi_float64] = -1.0

Definition

@inline
def cos[x] = rel_primitive_cos[x]

cosh

cosh[x]