		Search-engine friendly clone of the ACL2 documentation.

Schemalg

Schemalg-divconq-oset-0-1

APT schematic algorithm tranformation: specifics for the divide-and-conquer oset 0-1 schema.

Introduction

This is a divide-and-conquer schema over osets, with one base case for osets with 0 elements and one recursive case for osets with 1 or more elements.

General Form

(schemalg old
          :schema :divconq-oset-0-1
          :oset-input     ; default :auto
          :tail-output    ; default :auto
          :fvar-0-name    ; default :auto
          :fvar-1-name    ; default :auto
          :spec-0-name    ; default :auto
          :spec-0-enable  ; default nil
          :spec-1-name    ; default :auto
          :spec-1-enable  ; default nil
          ... ; see :doc schemalg
  )

Inputs

old — additional requirements

old must have the form described in Section `Input/Output Relation with Selected Input and Modified Inputs' of specification-forms. Let ?f, x, x1, ..., xn, a1<x1,...,xn>, ..., am<x1,...,xn>, and (lambda (x x1 ... xn y) iorel<x,x1,...,xn,y>) be as described there.

:oset-input — default :auto

Specifies the argument of the call of ?f that is treated as the oset on which algo[?f1]...[?fp] operates.
It must be one of the following:
:auto, to specify the only argument of the call of ?f, when the call has exactly one argument. It is an error for :oset-input to be :auto when the call has more than one argument.
An argument of the call of ?f that is a symbol, to specify that argument.
This is indicated as x in the description of the old input above.

:tail-output — default :auto

Specifies the name of the variable to use for the solution (i.e. output) for the tail of the oset, in the generated sub-specification for the recursive case.
It must be one of the following:
:auto, to use the symbol tail-output, in the same package as old.
Any other symbol, to use as the name.
In the rest of this documentation page, let y be this name.
In the schemalg design notes, y is denoted by y.

:fvar-0-name — additional information

If this input is :auto, we use the name of ?f, followed by `-0', with the resulting name in the same package as ?f.
In the rest of this documentation page, let ?g be the name determined by this input (whether it is :auto or not).

:fvar-1-name — additional information

If this input is :auto, we use the name of ?f, followed by `-1', with the resulting name in the same package as ?f.
In the rest of this documentation page, let ?h be the name determined by this input (whether it is :auto or not).

:spec-0-name — additional information

If this input is :auto, we use the name of old, followed by `-0', followed by ?g between square brackets, with the resulting name in the same package as old.
In the rest of this documentation page, let old-0[?g] be the name determined by this input (whether it is :auto or not).

:spec-1-name — additional information

If this input is :auto, we use the name of old, followed by `-1', followed by ?h between square brackets, with the resulting name in the same package as old.
In the rest of this documentation page, let old-1[?h] be the name determined by this input (whether it is :auto or not).

See schemalg for the rest of the description of the inputs.

Generated Events

Function variable used for osets with 0 elements:
(soft::defunvar ?g (* * ... *) => *)
where the number of arguments is m+1, i.e. the same as ?f.
In the schemalg design notes, ?g is denoted by g.

Function variable used for osets with 1 or more elements:
(soft::defunvar ?h (* * ... * *) => *)
where the number of arguments is m+2, i.e. the same as ?f plus one.
In the schemalg design notes, ?h is denoted by h.

algo[?g][?h]

Algorithm schema:
(soft::defun2 algo[?g][?h] (x z1 ... zm)
  (cond ((or (not (set::setp x)) (set::empty x)) (?g x z1 ... zm))
        (t (?h (set::head x)
               z1
               ...
               zm
               (algo[?g][?h] (set::tail x) z1 ... zm)))))
In the schemalg design notes, algo[?g][?h] is denoted by A(g,h) and z1, ..., zm are denoted by \overline{z}.

old-0[?g]

Sub-specification for osets with 0 elements:

(soft::defun-sk2 old-0[?g] ()
  (forall (x x1 ... xn)
          (impliez (or (not (set::setp x)) (set::empty x))
                   iorel<x,x1,...,xn,
                         (?g x a1<x1,...,xn> ... am<x1,...,xn>))))

old-1[?h]

Sub-specification for osets with 1 or more elements:

(soft::defun-sk2 old-1[?h] ()
  (forall (x x1 ... xn y)
          (impliez (and (set::setp x)
                        (not (set::empty x))
                        iorel<(set::tail x),x1,...,xn,y>)
                   iorel<x,x1,...,xn,
                         (?h (set::head x)
                             a1<x1,...,xn>
                             ...
                             am<x1,...,xn>
                             y))))

See schemalg for the rest of the description of the generated events.