		Search-engine friendly clone of the ACL2 documentation.

Schemalg

Schemalg-divconq-list-0-1

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

Introduction

This is a divide-and-conquer schema over (true or dotted) lists, with one base case for lists of length 0 and one recursive case for list of length 1 or more.

General Form

(schemalg old
          :schema :divconq-list-0-1
          :list-input     ; default :auto
          :cdr-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.

:list-input — default :auto

Specifies the argument of the call of ?f that is treated as the list 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 :list-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.

:cdr-output — default :auto

Specifies the name of the variable to use for the solution (i.e. output) for the cdr of the list, in the generated sub-specification for the recursive case.
It must be one of the following:
:auto, to use the symbol cdr-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 lists of length 0:
(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 lists of length 1 or more:
(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 ((atom x) (?g x z1 ... zm))
        (t (?h (car x)
               z1
               ...
               zm
               (algo[?g][?h] (cdr 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 lists of length 0:

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

old-1[?h]

Sub-specification for lists of length 1 or more:

(soft::defun-sk2 old-1[?h] ()
  (forall (x x1 ... xn y)
          (impliez (and (consp x)
                        iorel<(cdr x),x1,...,xn,y>)
                   iorel<x,x1,...,xn,
                         (?h (car x)
                             a1<x1,...,xn>
                             ...
                             am<x1,...,xn>
                             y))))

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