#Ceil

#Ceil

#Ceil( φ ) is the Matching Logic predicate that is #True if pattern φ is defined (matches any values) and #False otherwise. From this definition, it follows that:

(1)    φ = φ #And #Ceil( φ )  // φ is any pattern
(2)    #Ceil( P ) = P  // P is any Matching Logic predicate (#Ceil, #Equals, etc.)

We also emphasize this important fact about symbols:

(3)   #Ceil( σ(φ₁, φ₂, ...) ) #Implies #Ceil( φ₁ ) #And #Ceil( φ₂ ) #And ...  // σ is any symbol

Note that (3) is written with #Implies because the symbol may not be defined at all points. If a function is defined at all points, it should be given the attribute functional, which implies a rule:

(3')  #Ceil( σ(φ₁, φ₂, ...) ) #Equals #Ceil( φ₁ ) #And #Ceil( φ₂ ) #And ...  // σ is a total symbol

Note the use of #Equals in (3') compared to #Implies in (3).

Uninterpreted and undefined functions

We emphasize that "undefined" is not the same as "uninterpreted" (or "unspecified"). Consider the following three functions, which are all very similar:

positive_total is a total function that maps every Int to a Bool:

syntax Bool ::= positive_total( Int ) [function]
rule positive_total(X:Int) => true  requires X  >Int 0
rule positive_total(X:Int) => false requires X <=Int 0

From this definition, we can conclude:

• positive_total(1) matches the value true
• positive_total(-1) matches the value false

We can also say that

rule #Ceil( positive_total(X:Int) ) => #True
// or:
rule #Exists B:Bool . { B #In positive_total(X:Int) } => #True

In other words, for all X:Int, there exists a B:Bool that matches positive_total(X:Int). Total functions should be given the functional attribute, as a hint to the backend that the axiom above holds.

Now consider this example of a partial function:

syntax Bool ::= positive_partial( Int ) [function]
rule positive_partial(X:Int) => true   requires X  >Int 0
rule positive_partial(X:Int) => #False requires X <=Int 0

From this definition,

• positive_partial(1) matches true
• positive_partial(-1) is undefined; it does not match anything

The negative case can also be stated as:

#Not( #Exists B:Bool . { B #In positive_partial(-1) } )

Partial functions must not be given the functional attribute because they are undefined over some points.

Finally, consider a function with an unspecified (or uninterpreted) case:

syntax Bool ::= positive_unspecified( Int ) [function]
rule positive_unspecified(X:Int) => true requires X >Int 0

In the positive case, positive_unspecified(1) matches true. In the negative case, we cannot conclude anything about positive_unspecified(-1); it could match false, or true, or nothing at all. We say that case is unspecified, or that the function is uninterpreted at that point. Uninterpreted functions may be given the functional attribute; this implies that they do match some value at every point, but without actually specifying the value at every point.

As an extreme example, we can use an uninterpreted function to encode an arbitrary constant:

syntax Int ::= arbitrary() [function, functional, no-evaluators]

The attribute no-evaluators tells the backend that we intentionally did not define any evaluation rules. Without that attribute, the backend will issue a warning to remind us to define arbitrary. From this definition, the only thing we know is that:

#Exists X:Int . { X #In arbitrary() }

That is, arbitrary() matches some integer, but the actual value is not specified.

Variables, unification, and rule application

Matching Logic element variables are singular (matching exactly one value), so unifying a variable X with a term foo() introduces a condition #Ceil( foo() ). If this happens when unifying the left-hand side of a rule with the configuration, then #Ceil( foo() ) becomes a requirement to apply the rule. Writing rules with element variables on the left-hand side ensures that proofs do not rewrite after infeasible states. (By the principle ex falso quodlibet, an infeasible state satisfies any claim.) Recall that the backend splits the configuration on the rule's requirements:

1. the state where the requirement holds, so the rule applies (#Ceil( foo() ) etc.)
2. the state where the requirement does not hold, so the rule does not apply (#Not( #Ceil( foo() ) ) etc.)

Usually, the #Not #Ceil( foo() ) case needs to be refuted, or the proof becomes stuck. This case can often be refuted by applying statement (1) above to the configuration and using statement (3) to recurse through the cells of the configuration. The backend applies this formula to the left-hand side of the claim when checking the final implication, introducing #Ceil(left-hand side) into the side condition at the top level. The implication check happens at each step before applying any rules, to avoid rewriting any part of the left-hand side which has already reached the terminal configuration. Because rule application happens later in each proof step, the right-hand side of a rule will not have #Ceil applied until the start of the next proof step. When foo() appears in the left-hand term, the #Ceil(left-hand side) will contradict the #Not #Ceil( foo() ) so that the claim is shown to hold by the principle ex falso quodlibet.

If and only if foo() cannot be evaluated directly and does not appear as a sub-term of the left-hand side of the claim, it may be necessary to add a rule or rules that define #Ceil( foo() ) so that #Not( #Ceil( foo() ) ) can be refuted by other conditions on the claim. However, it is very unusual for this to actually be necessary and the user should do so only after submitting a bug report.