		Search-engine friendly clone of the ACL2 documentation.

Schemalg

APT schematic algorithm transformation: refine a specification by constraining a function to have a certain algorithmic form.

Introduction

This transformation operates on a specification expressed as a second-order predicate that constrains a function to be synthesized, according to the shallow pop-refinement approach described in the ACL2-2015 paper on SOFT. Currently, the second-order predicate must be expressed in SOFT. In the future, this transformation may be extended to operate also on second-order predicates expressed via the built-in apply$.

This transformation generates a refined specification that constrains the specification's function variable to be equal to a specified second-order function that captures an algorithmic structure. This introduces additional function variables, the ones that the second-order function depends on. The specified second-order function is accompanied by a theorem asserting the correctness of the algorithm given assumptions on these function variables. The transformation generates additional specifications corresponding to these assumptions. This way, once solutions for these specifications are synthesized, they can be composed into a solution for the original specification.

This transformation supports a number of algorithm schemas, each of which is described by the second-order function that defines it, the second-order theorem that states its correctness, and the forms of specifications that the schema applies to. This manual page provides the general reference for the transformation; there are separate manual pages that describe the specifics of the supported algorithm schemas. Support for additional schemas may be added in the future.

The schemalg design notes, which use this notation, provide the mathematical concepts and template proofs upon which this transformation is based along with all the supported algorithm schemas. These design notes should be read alongside this reference documentation, which refers to them in some places. These design notes also refer to the `Specifications and Refinements' design notes, which therefore should be also read as needed.

General Form

(schemalg old
          :schema             ; no default
          :...                ; schema-specific defaults
          :fvar-...-name      ; default :auto
          :algo-name          ; default :auto
          :algo-enable        ; default nil
          :spec-...-name      ; default :auto
          :spec-...-enable    ; default nil
          :equal-algo-name    ; default :auto
          :equal-algo-enable  ; default nil
          :new-name           ; default :auto
          :new-enable         ; default :auto
          :old-if-new-name    ; default from table
          :old-if-new-enable  ; default from table
          :verify-guards      ; default :auto
          :print              ; default :result
          :show-only          ; default nil
  )

Inputs

old

Denotes the target function to transform.
It must be the name of a function, or a numbered name with a wildcard index that resolves to the name of a function. In the rest of this documentation page, for expository convenience, it is assumed that old is the name of the denoted function.
old must be a SOFT function that has no parameters and that depends on one function variable. Let this function variable be ?f.
If the :verify-guardsinput is t, old must be guard-verified.
Additional requirements on the body of old are stated in the documentation page for the chosen algorithm schema.
In the schemalg design notes, old is denoted by S, ?f is denoted by f, and the body of old is denoted by \Phi[f]. Since currently SOFT function variables always return single values, it is always the case that m=1, in the codomain of f.

:schema — no default

Indicates the algorithm schema to use.
It must be one of the following:
:divconq-list-0-1
:divconq-list-0-1-2
:divconq-oset-0-1
(More may be added in the future.)
See the respective documentation pages for details.

:... — schema-specific defaults.

For each choice of the :schema input, this transformation may take additional inputs that are specific to the schema. These are described in the schema-specific documentation pages.

:fvar-...-name — default :auto.

For each choice of the :schema input, there are one or more :fvar-...-name inputs, which determine the names of the generate function variables that the algorithm schema's second-order function depends on. The number and names of these inputs are described in the schema-specific documentation page.
Each must be one of the following:
:auto, to use a symbol constructed as described in the schema-specific documentation page.
Any other symbol, to use as the name.
In the rest of this documentation page, let ?f1, ..., ?fp be these names.

:algo-name — default :auto

Determines the name of the generated second-order function for the algorithm schema.
It must be one of the following:
:auto, to use the name of ?f, without the ? if it starts with one, followed by the name of ?f1 between square brackets, ..., followed by the name of ?fp between square brackets, with the resulting name in the same package as ?f.
Any other symbol, to use as the name.
In the rest of this documentation page, let algo[?f1]...[?fp] be this name.

:algo-enable — default nil

Determines whether algo[?f1]...[?fp] is enabled.
It must be one of the following:
t, to enable.
nil, to disable.

:spec-...-name — default :auto

For each choice of the :schema input, there are one or more :spec-...-name inputs, which determine the names of the generated second-order predicates for the sub-specifications derived from the schema. The number and names of these inputs are described in the schema-specific documentation page.
Each must be one of the following:
:auto, to use a symbol constructed as described in the schema-specific documentation page.
Any other symbol, to use as the name.
In the rest of this documentation page, let spec1[?f1]...[?fp], ..., specq[?f1]...[?fp] be these names.

:spec-...-enable — default nil

For each choice of the :schema input, there are one or more :spec-...-enable inputs, one for each :spec-...-name inputs, which determine whether the corresponding predicate among spec1[?f1]...[?fp], ..., specq[?f1]...[?fp] is enabled or not.
It must be one of the following:
t, to enable the predicate.
nil, to disable the predicate.

:equal-algo-name — default :auto

Determines the name of the generated second-order equality between ?f and algo[?f1]...[?fp].
It must be one of the following:
:auto, to use the symbol equal, followed by the name of ?f between square brackets, followed by the name of algo[?f1]...[?fp] between square brackets, with the resulting name in the same package as ?f.
Any other symbol, to use as the name.
In the rest of this documentation page, let equal[?f][algo[?f1]...[?fp]] be this name.

:equal-algo-enable — default nil

Determines whether equal[?f][algo[?f1]...[?fp]] (along its associated defun-sk rewrite rule) is enabled.
It must be one of the following:
t, to enable.
nil, to disable.

:new-name — default :auto

Determines the name of the generated new function.
It must be one of the following:
:auto, to generate the name automatically as described in function-name-generation.
Any other symbol, to use as the name of the function.
In the rest of this documentation page, let new be the name of this function.

:new-enable — default :auto

Determines whether new is enabled.
It must be one of the following:
t, to enable it.
nil, to disable it.
:auto, to enable it iff old is enabled.

:old-if-new-name — default from table

Determines the name of the theorem asserting that the old function is implied by the old function.
It must be one of the following:
A keyword, to use as separator between the names of old and new. A keyword :kwd specifies the theorem name oldkwdnew, in the same package as new.
Any other symbol, to use as the name of the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-old-if-new-name.
In the rest of this documentation page, let old-if-new be the name of this theorem.

:old-if-new-enable — default from table

Determines whether the old-if-new theorem is enabled.
It must be one of the following:
t, to enable the theorem.
nil, to disable the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-old-if-new-enable.
If this input is t, the :new-to-old-enable input must be nil. At most one of these two inputs may be t at any time.

:verify-guards — default :auto

Determines whether the guards of the generated functions are verified or not.
It must be one of the following:
t, to verify the guards.
nil, to not verify guards.
:auto, to verify the guards if and only if the guards of the target function old are verified.

:print — default :result

Specifies what is printed on the screen (see screen printing).
It must be one of the following:
nil, to print nothing (not even error output).
:error, to print only error output (if any).
:result, to print, besides any error output, also the results of schemalg. This is the default value of the :print input.
:info, to print, besides any error output and the results, also some additional information about the internal operations of schemalg.
:all, to print, besides any error output, the results, and the additional information, also ACL2's output in response to all the submitted events.
If the call of schemalg is redundant, an indication to that effect is printed on the screen, unless :print is nil.

:show-only — default nil

Determines whether the event expansion of schemalg is submitted to ACL2 or just printed on the screen:
nil, to submit it.
t, to just print it. In this case: the event expansion is printed even if :print is nil (because the user has explicitly asked to show the event expansion); the resulting events are not re-printed separately (other than their appearance in the printed event expansion) even if :print is :result or :info or :all; no ACL2 output is printed for the event expansion even if :print is :all (because the event expansion is not submitted). If the call of schemalg is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

Generated Events

?f1
...
?fp

Function variables that algo[?f1]...[?fp] depends on:
(soft::defunvar ?f1 (* ... *) => *)
...
(soft::defunvar ?fp (* ... *) => *)
whose exact number and arities are described in the schema-specific documentation page.
In the schemalg design notes, ?f1, ..., ?fp are denoted by f_1,\ldots,f_p.

algo[?f1]...[?fp]

Second-order function for the algorithm schema:
(soft::defun2 algo[?f1]...[?fp] ...)
whose exact form is described in the schema-specific documentation page.
In the schemalg design notes, algo[?f1]...[?fp] is denoted by A(f_1,\ldots,f_p), whose correctness theorem formula is denoted by $\Psi_1[f_1,\ldots,f_p] \wedge \cdots \wedge \Psi_q[f_1,\ldots,f_p] \Longrightarrow \Psi[f_1,\ldots,f_p]$.

spec1[?f1]...[?fp]
...
specq[?f1]...[?fp]

Second-order predicates for the sub-specifications:
(soft::defun-sk2 spec1[?f1]...[?fp] ...)
...
(soft::defun-sk2 specq[?f1]...[?fp] ...)
whose exact form is described in the schema-specific documentation page.
In the schemalg design notes, spec1[?f1]...[?fp], ..., specq[?f1]...[?fp] are denoted by S_1,\ldots,S_q), and their bodies are denoted by \sigma(\Psi_1[f_1,\ldots,f_p]), \ldots, \sigma(\Psi_q[f_1,\ldots,f_p]), where sigma(\Psi[f]) = Phi[f].

equal[?f][algo[?f1]...[?fp]]

Equality between ?f and algo[?f1]...[?fp]:
(soft::defequal equal[?f][algo[?f1]...[?fp]]
  :left ?f
  :right algo[?f1]...[?fp]
  :vars ...)
whose specific :vars variables are described in the schema-specific documentation page.
In the schemalg design notes, this equality is denoted by f = A(f_1,\ldots,f_p).

new

Specification strengthened by choosing the algorithm schema:
(soft::defun2 new ()
  (and (equal[?f][algo[?f1]...[?fp]])
       (spec1[?f1]...[?fp])
       ...
       (specq[?f1]...[?fp])))
In the schemalg design notes, new is denoted by S'.

old-if-new

Theorem asserting that new implies old (i.e. a refinement relation):
(defthm old-if-new
  (implies (new)
           (old))
In the schemalg design notes, old-if-new is denoted by SS'.

Redundancy

A call of schemalg is redundant if and only if it is identical to a previous successful call of schemalg whose :show-only input is not t, except that the two calls may differ in their :print and :show-only inputs. These inputs do not affect the generated events, and thus they are ignored for the purpose of redundancy.

A call of schemalg whose :show-only input is t does not generate any event. Thus, no successive call may be redundant with such a call.

Subtopics

Schemalg-implementation: Implementation of schemalg.
Schemalg-divconq-oset-0-1: APT schematic algorithm tranformation: specifics for the divide-and-conquer oset 0-1 schema.
Schemalg-divconq-list-0-1: APT schematic algorithm tranformation: specifics for the divide-and-conquer list 0-1 schema.