LP, the Larch Prover -- Operators

An operator is a symbol that represents a total function. The signature of the operator specifies the domain and range of the function. Operators can be used with functional, infix, prefix, postfix, bracketed, and conditional notations.

Syntax

<operator>     ::= <opForm> [ : <signature> ]
<opForm>       ::= <functionId> | <simpleOpForm> | <bracketedOp> | <ifOp>
<functionId>   ::= <simpleId>
<simpleOpForm> ::= [ __ ] <simpleOp> [ __ ] | [ __ ] . <simpleId>
<simpleOp>     ::= <opId> | <escapedId>
<bracketedOp>  ::= [ __ ] <openSym> __*, <closeSym> [ __ ]
<openSym>      ::= { | "[" | \( | \<
<closeSym>     ::= } | "]" | \) | \>
<ifOp>         ::= if __ then __ else __
Note: All markers (__) may be omitted from a <simpleOpForm> when there is exactly one declared operator (with the indicated signature) that can be formed by adding some number of markers to the <simpleOpForm>.

Examples

<functionId>       f          0          gcd
<simpleOpForm>     -__        __<=>__    __\in__    __\Post    __.first 
<simpleOp>         -            <=>        \in        \Post
<bracketedOp>      __[__]     {}

Usage

LP automatically declares certain logical, equality, and conditional operators. All other operators must appear in a declare operators command. Case is significant in operator identifiers. Thus f and F are different operators, as are \in and \In.

Identifiers for most operators can be overloaded, that is, they can be used to represent operators with different signatures or with markers in different places. LP uses context to disambiguate overloaded identifiers.

The arity of an operator is the number of its arguments, that is, the number of sorts in its domain. A unary operator has arity 1, a binary operator has arity 2, and a constant has arity 0.

See also