# Totalisation

## Overview

A function is *total* iff it is *defined* for any argument in its domain. In MiniZinc, the domain of a function is determined by the *type-insts* of its arguments, but not by any *constraints* on its arguments.

A function is *partial* iff it is *undefined* for certain arguments in its domain. In MiniZinc, a function is partial if its return type is not a subtype of `var opt bool`

, and at least one of these conditions holds:

- If at least one of its arguments has a constrained type. E.g.,
`function int: foo(1..3: x) = x + 1;`

is partial, because its argument`x`

is constrained. - If its body is a partially defined expression
- If it is a built-in function that is known to be partial (e.g. integer division, modulo etc.)

A function that is partial according to the rules above can be annotated as `::promise_total`

if it can be guaranteed that it will return a value for any input in its domain.

An expression is *partially defined* if its type is not a subtype of `var opt bool`

and it does not evaluate to a value for all possible evaluations of its free variables. At least one of the following conditions needs to hold for an expression to be partially defined:

- It is a call to a partial function or built-in operator
- It is a
`let`

expression with a type that is not a subtype of`var opt bool`

, and one of the cases in the`let`

is a`constraint`

, or one of the variables in the`let`

has a constrained type-inst - One of its immediate subexpressions is partially defined

## Array types

Two options:

- An undefined element in an array makes the entire array undefined (MiniZinc 2 semantics)
- An undefined element in an array only causes undefinedness if the element is accessed (Stuckey/Frisch paper)

Issues with option 2: Passing an array to a function now means that all arrays have to be arrays of tuples (even if all elements are statically known to be defined); or, we have to generate different versions (tuple and non-tuple) for each function, for all array argument types.

## Transformation

The basic idea of the transformation is to turn any partially defined expression into a pair of expressions `(b,e)`

where `b`

is a Boolean that is true iff the expression is defined, and `e`

is the value of the expression if it is defined, and `⊥`

otherwise.

- The return type of a partial function returning type
`T`

is changed to`tuple(bool, T)`

. - Any variable declaration of type
`T`

whose right hand side is a partially defined expression is changed into a variable declaration of type`tuple(bool, T)`

.**NOTE:**What about array types? Do they capture definedness for each element, or for the array? - Set literals (containing partially defined expressions)
The type is transformed from
`set of T`

into`tuple(bool, set of T)`

as follows.`{ e1, e2, pde1, ..., pdek, ... }`

into`let { any: (b1,tmp1) = pde1; any: (bk,tmpk) = pdek; } in (forall([b1,...,bk]), {e1, e2, tmp1, ..., tmpk ...})`

- Array literals (containing partially defined expressions)
~~Change type~~Change type`array[...] of T`

into`array[...] of tuple(bool, T)`

and change`[ e1, ..., pde1, ... pdek, ... en]`

into`[ (true, e1), ..., pde1, ... pdek, ... (true,en) ]`

`array[...] of T`

into`tuple(bool, array [...] of T`

and change`[ e1, ..., (b1, pde1), ... (bk, pdek), ... en]`

into`(b1 /\ ... /\ bk, [e1, pde1, ... pdek, ... en])`

- Array comprehensions
- Partially defined generators are not permitted (static type error).
- Partially defined generated expressions are fine. The resulting type changes from
`array[...] of T`

into`tuple(bool, array[...] of T)`

(like array literals). May need to create`array [...] of tuple(bool, T)`

first, then extract the definedness from that.**** - Partially defined where clauses are fine (they are their own Boolean context)
- These examples show why it would be a bad idea to allow partial generators. - par comprehensions
`[ pde | i in 0..10, j in x[i] ]`

`[ pde | i in 0..10, (b,e)=x[i] where b, j in e ]`

- var generator comprehensions:`var 0..10: x`

`[ pde | i in 0..10, j in i div x..100]`

`[ let { any: (b,t) = i div x..100; any: (eb, et) = pde } in if eb /\ b /\ j in t..100 then (true,et) else (b,<>) endif) | i in 0..10, j in ub(i div x..100) ]`

- Set comprehensions
These are transformed into array comprehensions and
`array2set`

in a previous compiler phase. - Array access

`var`

array access turns into`element()`

which has the right semantics.`function tuple(bool, any $T): element(array [int, ...] of any $T: x, int: i, ...)`

where the boolean is `if then else endif`

Can't use a normal function since the arguments would escape into the boolean context outside, so instead define the function which returns the pair:

`function tuple(var bool, var $T): if_then_else(array [int] of var bool: c, array [int] of tuple(var bool, var $T): r)`

- Tuple field access

Same as for arrays, so undefined inside a tuple makes the whole tuple undefined - Calls Transformed to return a tuple if not known to be total
`let { ... } in`

If not in`::promise_total`

/root context and non-boolean then the conjunction of the constraints and the variable definedness becomes the let's definedness

becomes`let { var int: x = e1; constraint c; } in e2`

`let { tuple(var bool, var int): x' = (de1, e1'); var bool: c' = c; } in (de1 /\ c' /\ de2, e2')`

- Annotations Annotations are compiled in the root context.
- Output
The expression in an output statement must be total. It is a static type error if it isn't. Users can use
`default`

to make all expressions total.