Assert the Truth, Unassert the Untruth

April 20, 2016

Quasar has a logic system, that is centered around the assert function and that can be useful for several reasons:

Assertions can be used for testing a specified condition, resulting in a runtime error (error) if the condition is not met:
```
assert(positiveNumber>0,"positiveNumber became negative while it shouldn't")
```
Assertions can also help the optimization system. For example, the type of variables can be “asserted” using type assertions:
```
assert(type(cubicle, "cube[cube]"))
```
The compiler can then verify the type of the variable cubicle and if it is not known at this stage, knowledge can be inserted into the compiler, resulting in the compilation message:
```
assert.q - Line 4: [info] 'cubicle' is now assumed to be of type 'cube[cube]'.
```
At runtime, the assert function just behaves like usual, resulting in an error if the condition is not met.
Assertions are useful in combination with reduction-where clauses:
```
reduction (x : scalar) -> abs(x) = x where x >= 0
```
If we previously assert that x is a positive number, then this assertion will eliminate the runtime check for x >= 0.
Assertions can be used to cut branches:
```
assert(x > 0 && x < 1)
if x < 0
    ...
endif   
```
Here, the compiler will determine that the if-block will never be executed, so it will destroy the entire content of the if-block, resulting in a compilation message:
```
assert.q - Line 10: [info] if-branch is cut due to the assertions `x > 0 && x < 1`.
```
Similarly, pre-processor branches can be constructed with this approach.
Assertions can be combined with generic function specialization. Later more about this.

It is not possible to fool the compiler. For example, if the compiler can determine at compile-time that the assertion will never be met, an error will be generated, and it will not be even possible to run the program.

Logic system

The Quasar compiler has now a propositional logic system, that is able to “reason” about previous assertions. Also, different assertions can be combined using the logical operators AND &&, OR ||and NOT !.

There are three meta functions that help with assertions:

$check(proposition) checks whether proposition can be satisfied, given the previous set of assertions, resulting in three possible values: "Valid", "Satisfiable" or "Unsatisfiable".
$assump(variable) lists all assertions that are currently known about a variable, including the implicit type predicates that are obtained through type inference. Note that the result of $assumpis an expression, so for visualization it may be necessary to convert it to a textual representation using $str(.) (to avoid the expression from being evaluated).
$simplify(expr) simplifies logic expressions based on the knowledge that is inserted through assertions.

Types of assertions

There are different types of assertions that can be combined in a transparent way.

Equalities

The most simple cases of assertions are the equality assertions a==b. For example:

symbolic a, b
assert(a==4 && b==6)

assert($check(a==5)=="Unsatisfiable")
assert($check(a==4)=="Valid")
assert($check(a!=4)=="Unsatisfiable")
assert($check(b==6)=="Valid")
assert($check(b==3)=="Unsatisfiable")
assert($check(b!=6)=="Unsatisfiable")
assert($check(a==4 && b==6)=="Valid")
assert($check(a==4 && b==5)=="Unsatisfiable")
assert($check(a==4 && b!=6)=="Unsatisfiable")
assert($check(a==4 || b==6)=="Valid")
assert($check(a==4 || b==7)=="Valid")
assert($check(a==3 || b==6)=="Valid")
assert($check(a==3 || b==5)=="Unsatisfiable")
assert($check(a!=4 || b==6)=="Valid")

print $str($assump(a)),",",$str($assump(b)) % prints (a==4),(b==6)

Here, we use symbolic to declare symbolic variables (variables that are not to be “evaluated”, i.e. translated into their actual value since they don’t have a specific value). Next, the function assert is used to test whether the $check(.) function works correctly (=self-checking).

Inequalities

The propositional logic system can also work with inequalities:

symbolic a
assert(a>2 && a<4)
assert($check(a>1)=="Valid")
assert($check(a>3)=="Satisfiable")
assert($check(a<3)=="Satisfiable")
assert($check(a<2)=="Unsatisfiable")
assert($check(a>4)=="Unsatisfiable")
assert($check(a<=2)=="Unsatisfiable")
assert($check(a>=2)=="Valid")
assert($check(a<=3)=="Satisfiable")
assert($check(!(a>3))=="Satisfiable")

Type assertions

As in the above example:

assert(type(cubicle, "cube[cube]"))

Please note that assertions should not be used with the intention of variable type declaration. To declare the type of certain variables there is a more straightforward approach:

cubicle : cube[cube]

Type assertions can be used in functions that accept generic ?? arguments, then for example to ensure that a cube[cube] is passed depending on another parameter.

User-defined properties of variables

It is also possible to define “properties” of variables, using a symbolic declaration. For example:

symbolic is_a_hero, Jan_Aelterman

Then you can assert:

assert(is_a_hero(Jan_Aelterman))

Correspondingly, if you perform the test:

print $check(is_a_hero(Jan_Aelterman))   % Prints: Valid
print $check(!is_a_hero(Jan_Aelterman))  % Prints: Unsatisfiable

If you then try to assert the opposite:

assert(!is_a_hero(Jan_Aelterman))

The compiler will complain:

assert.q - Line 119: NO NO NO I don't believe this, can't be true! 
Assertion '!(is_a_hero(Jan_Aelterman))' is contradictory with 'is_a_hero(Jan_Aelterman)'

Unassert

In some cases, it is neccesary to undo certain assertions that were previously made. For this task, the function unassert can be used:

unassert(propositions)

This function only has a meaning at compile-time; at run-time nothing needs to be done.

For example, if you wish to reconsider the assertion is_a_hero(Jan_Aelterman) you can write:

unassert(is_a_hero(Jan_Aelterman))

print $check(is_a_hero(Jan_Aelterman))   % Prints: most likely not
print $check(!is_a_hero(Jan_Aelterman))  % Prints: very likely

Alternatively you could have written:

unassert(!is_a_hero(Jan_Aelterman))

print $check(is_a_hero(Jan_Aelterman))   % Prints: Valid
print $check(!is_a_hero(Jan_Aelterman))  % Prints: Unsatisfiable

Posted in Documentation and tagged New features