Download Ontic: Language Specification and User`s Manual Robert Givan

The operator double is a possible value of (an-operator-from (an-integer)
to (an-integer)). Consider the operator an-integer-greater-than which
takes an integer and returns an integer x and returns an integer greater
than x. The operator an-integer-greater-than is also a possible value of
(an-operator-from (an-integer) to (an-integer)).
The primitive an-operator-from can take more than one domain type.
For example, the operator + which takes two integers and returns an integer
is a possible value of (an-operator-from (an-integer) (an-integer) to
(an-integer)). In general, the possible values of an expression of the form
(an-operator-from τ1 . . . τn to σ) are all the operators f whose domain
sets are the sets of possible values of τ1 , . . ., τn and such that for any possible
values x1 , . . ., xn of τ1 , . . ., τn respectively, we have that every possible value
of (f x1 . . . xn ) is a possible value of σ. Because all Ontic operators are
Curried, the expressions (an-operator-from τ1 τ2 to σ) is equivalent to
the expression (an-operator-from τ1 to (an-operator-from τ2 to σ)).
The axiom of choice is incorporated into Ontic by including the primitive
construct a-choice-function-from. The primitive a-choice-function-from
is similar to the primitive an-operator-from except that it introduce bound
variables to represent elements of the domain types and it always returns a
function rather than an arbitrary operator. For example, the possible values
of the expression
(a-choice-function-from (x (an-integer))
to (an-integer-greater-than x))
are all operators f such that for any integer x there is exactly one possible value of (f x) and that value is an integer greater than x. Note
that the value f must be a function, i.e., for any element x of the domain
type (f x) must have exactly one possible value. The function successor
which takes an integer x and return x + 1 is a possible value of the above
a-choice-function-from expression. A function such as successor is
called a “choice function” because it selects a possible value of the expression
(an-integer-greater-than x). The operator an-integer-greater-than
is not a possible value of the above a-choice-function-from expression be-
20