next up previous contents
Next: 16. Syntax: Parsing and Up: 2. User's Guide Previous: 14. Macetes

Subsections

15. The Iota Constructor

15.1 Motivation

The iota or $\iota$ constructor is a definite description operator for objects of kind $\iota$. Given a variable x of sort $\alpha$ of kind $\iota$ and a unary predicate $\varphi$,

\begin{displaymath}\iota{x\mbox{:}\alpha},\varphi(x)\end{displaymath}

denotes the unique x that satisfies $\varphi$ if there is such an x and is undefined otherwise. For example,

\begin{displaymath}\iota{x\mbox{:}\alpha},0\leq x \wedge x\ast
x=2\end{displaymath}

denotes $\sqrt{2}$ but

\begin{displaymath}\iota{x\mbox{:}\alpha},x\ast x=2\end{displaymath}

is undefined.

The iota constructor is very useful for specifying functions, especially partial functions. For example, ordinary division of sort $[{\bf R},{\bf R},{\bf R}]$ (which is undefined whenever its second argument is 0) can be defined from the times function $\ast$ by the lambda-expression

\begin{displaymath}\lambda{x,y\mbox{:}{\bf
R}},\iota{z\mbox{:}{\bf R}}, x \ast z = y.\end{displaymath}

Of course, this kind of definite description operator is only possible in a logic that admits undefined expressions.

15.2 Reasoning with Iota

An iota-expression is any expression which begins with the iota constructor (without any abbreviations by quasi-constructors). Proving a sequent with an assertion containing an iota-expression can be tricky. The key idea is to reduce the sequent to a new sequent with one less iota-expression. This is called ``eliminating iota.'' There are two commands and one macete for eliminating iota, each of which is discussed below in a separate subsection.

15.2.1 eliminate-defined-iota-expression

This command, which is described in Chapter 18, is the best iota-elimination tool in IMPS. Generally, you should use it whenever you want to eliminate an iota-expression whose definedness is implied by the sequent's context. It can also be used effectively in some cases on an iota-expression E whose definedness is not implied by the sequent's context. This is done by applying case-split with $E\!\!\downarrow\vee \neg(E\!\!\downarrow)$, followed by applying eliminate-defined-iota-expression on the $E\!\!\downarrow$ case.

The eliminate-defined-iota-expression command is multi-inference; it adds about 20 new sequent nodes to a deduction graph.

15.2.2 eliminate-iota

This command is also described in Chapter 18. It is a single-inference command that is applicable to just atomic and negated atomic formulas. You should use it when you want to eliminate an iota-expression whose definedness is not implied by the sequent's context.

15.2.3 eliminate-iota-macete

This is a compound macete with built-in abstraction specified by:

   (def-compound-macete ELIMINATE-IOTA-MACETE
     (sequential
      iota-abstraction-macete
      (series
       tr%defined-iota-expression-elimination
       tr%negated-defined-iota-expression-elimination
       tr%left-iota-expression-equation-elimination
       tr%right-iota-expression-equation-elimination)
      beta-reduce))
The four elimination theorems are in the file $IMPS/theories/generic-theories/iota.t. You should try eliminate-iota-macete when the assertion has one of the following forms:
1.
$(\iota{x\mbox{:}\alpha},\varphi(x))\!\!\downarrow$
2.
$\neg((\iota{x\mbox{:}\alpha},\varphi(x))\!\!\downarrow)$
3.
$(\iota{x\mbox{:}\alpha},\varphi(x))=E$
4.
$(\iota{x\mbox{:}\alpha},\varphi(x))\not=E$
5.
$E=(\iota{x\mbox{:}\alpha},\varphi(x))$
6.
$E\not=(\iota{x\mbox{:}\alpha},\varphi(x))$
7.
$(\iota{x\mbox{:}\alpha},\varphi(x)) \simeq E$
8.
$E \simeq (\iota{x\mbox{:}\alpha},\varphi(x))$
For forms (1)-(6), the macete can be applied immediately, but for forms (7) and (8), the command insistent-direct-inference must be applied first. Beware that, for various reasons, eliminate-iota-macete may fail to do anything, in which case you should use one of the two iota-elimination commands.

15.3 Hints and Cautions

1.
Suppose E is an expression of sort $\alpha$. Sometimes it is convenient to have a new expression E' of sort $\beta$ (where $\tau(\beta) = \tau(\alpha)$ but $\beta \not= \alpha$) such that Eand E' have the same denotation. Such an expression can be easily constructed from E and $\beta$ using iota: $\iota
x\mbox{:}\beta,x=E$ is quasi-equal to E and is of sort $\beta$. For example, $\iota x\mbox{:}{\bf N},x=2$ denotes the natural number 2. It is important to mention here that the IMPS simplifier reduces an iota-expression of the form $\iota
x\mbox{:}\beta,x=E$ to the conditional $\mbox{\rm if}\,(E\downarrow\beta,E,\bot_\beta)$, and further to E or $\bot_\beta$ if it can decide the formula $E\downarrow\beta$.

2.
Suppose f is a function constant defined to be

\begin{displaymath}\lambda{x\mbox{:}\alpha}, \iota y\mbox{:}\beta, \varphi(x,y)\end{displaymath}

such that the following ``existence implies uniqueness'' theorem holds for $\varphi$:

\begin{displaymath}\forall{x\mbox{:}\alpha},(\exists{y\mbox{:}\beta}, \varphi(x,y))
\supset (\exists!{y\mbox{:}\beta}, \varphi(x,y)).\end{displaymath}

By virtue of this theorem, there is an ``iota-free characterization'' of f,

\begin{displaymath}\forall{x\mbox{:}\alpha,y\mbox{:}\beta}, f(x)=y \equiv
\varphi(x,y),\end{displaymath}

which enables one to prove a formula f(a)=b by showing only existence--without employing any of the aforementioned tools for eliminating iota.

As an example, consider the limit operator lim%rr on sequences of reals defined by:

   (def-constant LIM%RR
     "lambda(s:[zz,rr], iota(x:rr, forall(eps:rr,
        0<eps 
         implies 
        forsome(n:zz, forall(p:zz, 
          n<=p implies abs(x-s(p))<=eps)))))"
     (theory h-o-real-arithmetic))
Since a sequence always has at most one limit point, there is an iota-free characterization of lim%rr:
   (def-theorem CHARACTERIZATION-OF-REAL-LIMIT
     "forall(s:[zz,rr],
        x:rr,lim%rr(s)=x 
         iff 
        forall(eps:rr,
          0<eps 
           implies 
          forsome(n:zz, forall(p:zz, 
            n<=p implies abs(x-s(p))<=eps))))"
     (theory h-o-real-arithmetic))

3.
It is rarely a good idea to unfold a constant defined as an iota-expression, if it has an iota-free characterization. Instead, the following steps are suggested. For concreteness, let us assume the constant we are unfolding is a function constant f as in the previous item. Our aim is to reduce all occurrences of f to occurrences of the form f(a)=b,

4.
The iota-p constructor is a definite description operator for objects of kind $\ast$. It has a different semantics than iota: if there is no unique x of sort $\alpha$ satisfying a unary predicate $\varphi$, then $\iota_{\rm p}{x\mbox{:}\alpha},\varphi$ is defined (like all expressions of kind $\ast$) but has the value $\mbox{$\mbox{\sc f}_{\tau(\alpha)}$ }$. There is currently no support in IMPS for reasoning about the iota-p. This should not cause you any concern because iota-p has little practical value.


next up previous contents
Next: 16. Syntax: Parsing and Up: 2. User's Guide Previous: 14. Macetes
System Administrator
2000-07-23