• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Mutual-recursion
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
          • Lambda
          • Warrant
          • Defwarrant
          • Badge
          • Lambda$
          • Tame
          • Defbadge
          • Print-cl-cache
          • Introduction-to-apply$
            • Well-formed-lambda-objectp
            • Rewriting-calls-of-apply$-ev$-and-loop$-scions
            • Mixed-mode-functions
            • Explain-giant-lambda-object
            • Gratuitous-lambda-object-restrictions
            • Scion
            • Ilk
            • Ev$
            • Translam
            • Fn-equal
            • Apply$-guard
            • L<
            • Apply$-lambda-guard
            • Apply$-userfn
            • Badge-userfn
            • Defun$
            • Apply$-lambda
          • Loop$
          • Programming-with-state
          • Arrays
          • Characters
          • Time$
          • Defconst
          • Defmacro
          • Loop$-primer
          • Fast-alists
          • Evaluation
          • Guard
          • Equality-variants
          • Compilation
          • Hons
          • ACL2-built-ins
            • Let
            • Declare
            • Mbe
            • Apply$
              • Lambda
              • Warrant
              • Defwarrant
              • Badge
              • Lambda$
              • Tame
              • Defbadge
              • Print-cl-cache
              • Introduction-to-apply$
                • Well-formed-lambda-objectp
                • Rewriting-calls-of-apply$-ev$-and-loop$-scions
                • Mixed-mode-functions
                • Explain-giant-lambda-object
                • Gratuitous-lambda-object-restrictions
                • Scion
                • Ilk
                • Ev$
                • Translam
                • Fn-equal
                • Apply$-guard
                • L<
                • Apply$-lambda-guard
                • Apply$-userfn
                • Badge-userfn
                • Defun$
                • Apply$-lambda
              • Fmt
              • Loop$
              • Return-last
              • Mv-let
              • Df
              • Pseudo-termp
              • Defwarrant
              • Time$
              • Mbt
              • Ec-call
              • Mv-nth
              • Sys-call
              • Msg
              • Er
              • Value-triple
              • O-p
              • Comp
              • Member
              • O<
              • Cw
              • Flet
              • Or
              • Hons
              • Cbd
              • Mv
              • Defbadge
              • Append
              • *ACL2-exports*
              • Comment
              • Eql
              • List
              • Unsigned-byte-p
              • Posp
              • Natp
              • The
              • Nth
              • And
              • Len
              • Time-tracker
              • Term-order
              • True-listp
              • Msgp
              • Booleanp
              • <
              • If
              • Pseudo-term-listp
              • +
              • Not
              • With-global-stobj
              • Bitp
              • Equal
              • Cdr
              • Car
              • String-listp
              • Nat-listp
              • Implies
              • Iff
              • Character-listp
              • Alistp
              • Cons
              • Symbol-listp
              • Macrolet
              • Quote
              • Integerp
              • Consp
              • True-list-listp
              • State-global-let*
              • Compress1
              • Symbolp
              • Stringp
              • *common-lisp-symbols-from-main-lisp-package*
              • Characterp
              • Prog2$
              • *
              • Last-prover-steps
              • Hons-acons
              • Let*
              • Eq
              • With-guard-checking
              • @
              • Length
              • With-local-stobj
              • Hard-error
              • -
              • Zp
              • Search
              • Intersection$
              • Assign
              • Aset1
              • Symbol-name
              • Union$
              • Set-gc-strategy
              • In-tau-intervalp
              • Cons-with-hint
              • Break-on-error
              • Pand
              • Case-match
              • Fast-alist-fork
              • Sys-call+
              • Signed-byte-p
              • ACL2-count
              • Remove-duplicates
              • With-serialize-character
              • Observation
              • Hons-resize
              • Make-tau-interval
              • Assoc
              • Logbitp
              • Termp
              • Position
              • *standard-co*
              • Hons-acons!
              • Update-nth
              • Aref1
              • Symbol-alistp
              • Read-run-time
              • Take
              • Symbol-package-name
              • Hons-wash
              • Keywordp
              • Expt
              • Coerce
              • Get-internal-time
              • Intern
              • Non-exec
              • Case
              • Standard-oi
              • Standard-co
              • Formula
              • Atom
              • Without-evisc
              • Good-bye
              • Ash
              • With-local-state
              • Spec-mv-let
              • Intern-in-package-of-symbol
              • Binary-+
              • <=
              • With-fast-alist
              • Set-difference$
              • Hons-clear
              • Flush-compress
              • Rationalp
              • Por
              • Rassoc
              • Logand
              • Remove-assoc
              • =
              • Nthcdr
              • Pargs
              • Nfix
              • Hons-copy
              • Alphorder
              • Subsetp
              • Floor
              • Remove1-assoc
              • No-duplicatesp
              • Mv-list
              • Canonical-pathname
              • Aset2
              • Serialize-read
              • Random$
              • Fmt-to-comment-window
              • F-put-global
              • Compress2
              • Concatenate
              • Fast-alist-clean
              • Assert$
              • Remove
              • Remove1
              • Intersectp
              • Endp
              • Put-assoc
              • Princ$
              • Primitive
              • Keyword-value-listp
              • True-list-fix
              • Swap-stobjs
              • Integer-listp
              • Illegal
              • Hons-get
              • With-output-lock
              • Setenv$
              • Open-output-channel!
              • Fast-alist-free
              • Er-progn
              • Cw-print-base-radix
              • Reverse
              • Cond
              • Complex
              • Add-to-set
              • Truncate
              • Digit-char-p
              • Code-char
              • Char-code
              • Set-print-case
              • Set-print-base
              • Read-ACL2-oracle
              • Error1
              • Print-object$
              • Plet
              • Logior
              • Integer-length
              • Zip
              • With-live-state
              • Hons-assoc-equal
              • Extend-pathname
              • In-package
              • With-guard-checking-event
              • Term-listp
              • Print-object$+
              • Fmx-cw
              • String
              • Mod
              • Unary--
              • Set-print-radix
              • Resize-list
              • Pkg-witness
              • Revappend
              • Null
              • Term-list-listp
              • Make-fast-alist
              • Header
              • Boole$
              • Subseq
              • Logxor
              • With-guard-checking-error-triple
              • /
              • Make-list
              • Char-upcase
              • Char-downcase
              • Strip-cars
              • Set-fmt-hard-right-margin
              • Make-ord
              • Ifix
              • Fast-alist-free-on-exit
              • F-get-global
              • Aref2
              • Standard-char-p
              • Lognot
              • Must-be-equal
              • Integer-range-p
              • Getenv$
              • Binary-append
              • Er-hard
              • Eqlablep
              • Cpu-core-count
              • Boolean-listp
              • Allocate-fixnum-range
              • ACL2-numberp
              • Butlast
              • Pairlis$
              • Mod-expt
              • Hons-equal
              • Gc$
              • Substitute
              • Ceiling
              • With-stolen-alist
              • Mv?-let
              • String-upcase
              • String-downcase
              • Round
              • Count
              • Char
              • Sys-call-status
              • Progn$
              • Pprogn
              • Lexorder
              • Hons-summary
              • Break$
              • Assert*
              • Alpha-char-p
              • Strip-cdrs
              • Serialize-write
              • Keyword-listp
              • Upper-case-p
              • Lower-case-p
              • Logeqv
              • List*
              • Last
              • Proofs-co
              • Maximum-length
              • Fix
              • Explode-nonnegative-integer
              • Eqlable-listp
              • Dimensions
              • Default
              • Arity
              • Sublis
              • Max
              • Evenp
              • Explode-atom
              • Change
              • Zerop
              • String<
              • String-equal
              • Abs
              • Set-print-base-radix
              • Print-base-p
              • Nonnegative-integer-quotient
              • Intern$
              • Getprop
              • Binary-*
              • Aset1-trusted
              • Symbol<
              • String-append
              • Rfix
              • Mv?
              • Logic-fns-list-listp
              • Fast-alist-fork!
              • Er-hard?
              • Char-equal
              • 1+
              • *standard-oi*
              • Sys-call*
              • Pos-listp
              • Mbt*
              • Hons-wash!
              • Hons-clear!
              • Signum
              • Rem
              • Real/rationalp
              • Rational-listp
              • O-first-coeff
              • Logic-fnsp
              • Logic-fns-listp
              • Hons-copy-persistent
              • Gc-strategy
              • Fast-alist-summary
              • String>=
              • String<=
              • Acons
              • O-first-expt
              • Fast-alist-clean!
              • >=
              • >
              • Subst
              • Logcount
              • Getpropc
              • Evens
              • Er-soft
              • Digit-to-char
              • Comp-gcl
              • Atom-listp
              • Arities-okp
              • ACL2-number-listp
              • /=
              • Cadr
              • *standard-ci*
              • Unary-/
              • The-true-list
              • Realfix
              • O-rst
              • Fast-alist-len
              • Complex/complex-rationalp
              • Array2p
              • Array1p
              • Logtest
              • Logandc1
              • Char<
              • Trace-co
              • Putprop
              • Get-real-time
              • Eqlable-alistp
              • Count-keys
              • Assoc-string-equal
              • Logorc1
              • Logandc2
              • Denominator
              • 1-
              • Packn
              • Logic-termp
              • Logic-term-list-listp
              • Fmt!
              • Fms
              • Cw!
              • Assoc-keyword
              • String>
              • Numerator
              • Logorc2
              • Lognor
              • Char>=
              • Update-nth-array
              • The-number
              • Odds
              • Makunbound-global
              • Make-character-list
              • Make
              • List$
              • Int=
              • Get-cpu-time
              • Fmt-to-comment-window!
              • Fms!
              • F-boundp-global
              • Complex-rationalp
              • Alist-to-doublets
              • Access
              • Min
              • Lognand
              • Listp
              • Identity
              • Char>
              • Char<=
              • Zpf
              • Standard-char-listp
              • O-finp
              • Number-subtrees
              • Logic-term-listp
              • Last-cdr
              • Fmt1!
              • Fmt-to-comment-window!+
              • Character-alistp
              • Oddp
              • Minusp
              • Imagpart
              • Conjugate
              • Xor
              • Unquote
              • String-alistp
              • Packn-pos
              • Maybe-flush-and-compress1
              • Kwote
              • Fmt1
              • Fmt-to-comment-window+
              • Cw-print-base-radix!
              • Alist-keys-subsetp
              • Realpart
              • Plusp
              • First
              • Symbol-name-lst
              • R-symbol-alistp
              • R-eqlable-alistp
              • Fmx
              • Cw!+
              • Cons-subtrees
              • Cons-count-bounded
              • Cddr
              • Caar
              • Proper-consp
              • Kwote-lst
              • Improper-consp
              • Cw+
              • Rest
              • Standard-char-p+
              • Mbe1
              • Caddr
              • Pairlis-x2
              • Pairlis-x1
              • O>=
              • O<=
              • O-infp
              • Merge-sort-lexorder
              • Fix-true-list
              • Cdddr
              • Set-fmt-soft-right-margin
              • Real-listp
              • O>
              • Cddar
              • Cdar
              • Cdadr
              • Cdaar
              • Cadar
              • Caadr
              • Caaar
              • Cadddr
              • Caddar
              • Third
              • Tenth
              • Sixth
              • Seventh
              • Second
              • Ninth
              • Fourth
              • Fifth
              • Eighth
              • Cddddr
              • Cdddar
              • Cddadr
              • Cddaar
              • Cdaddr
              • Cdadar
              • Cdaadr
              • Cdaaar
              • Cadadr
              • Cadaar
              • Caaddr
              • Caadar
              • Caaadr
              • Caaaar
              • Hons-shrink-alist!
              • Hons-shrink-alist
              • Flush-hons-get-hash-table-link
              • Delete-assoc
            • Developers-guide
            • System-attachments
            • Advanced-features
            • Set-check-invariant-risk
            • Numbers
            • Efficiency
            • Irrelevant-formals
            • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
            • Redefining-programs
            • Lists
            • Invariant-risk
            • Errors
            • Defabbrev
            • Conses
            • Alists
            • Set-register-invariant-risk
            • Strings
            • Program-wrapper
            • Get-internal-time
            • Basics
            • Packages
            • Oracle-eval
            • Defmacro-untouchable
            • <<
            • Primitive
            • Revert-world
            • Unmemoize
            • Set-duplicate-keys-action
            • Symbols
            • Def-list-constructor
            • Easy-simplify-term
            • Defiteration
            • Fake-oracle-eval
            • Defopen
            • Sleep
          • Operational-semantics
          • Real
          • Start-here
          • Debugging
          • Miscellaneous
          • Output-controls
          • Macros
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Apply$

      Introduction-to-apply$

      Background knowledge on how to use apply$, defwarrant, etc.

      Background and Organization

      Apply$ is the ACL2 version of LISP's apply function. It takes a ``function'' and a list of argument values, applies the function to the arguments, and returns the result. For example, (apply$ 'expt (list 2 8)) returns 256.

      A good introduction to the basic ideas and challenges of adding apply$ to ACL2 is the paper ``Limited Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann and J Strother Moore, Journal of Automated Reasoning, Springer, 64, pp 391-422, 2018. We refer to the paper simply as ``the paper.'' Some aspects of the paper are no longer accurate because the implementation of apply$ has matured since 2018. But as a basic introduction, rather than a reference guide or user's manual, the paper is a good place to start. It provides motivations and challenges, succinct and precise definitions of relevant concepts, lots of examples, a model and meta-level proof that the extended theory is consistent, and a discussion of the limitations and of related work. The model described in the paper is illustrated concretely in the certified books under books/projects/apply-model/. See the README file there.

      The current documentation topic takes a slightly more informal approach but covers much of the same ground. In particular, after some preliminary remarks we coach you through a few simple simple exercises involving apply$ and related concepts. During these exercises we draw your attention to some basic lessons to keep in mind. At the end of this topic we list some simple challenge problems.

      This topic links to reference-level documentation for apply$ and those other concepts. But if you are just getting started with apply$ we recommend that you work your way through this topic, including doing the examples described below, without following all the links.

      Challenges and Basic Solutions

      The unreachable goal of this work is to allow the ACL2 user to pass `functions' as objects and to apply them. That goal is unreachable because ACL2 remains a first order system. However, we can identify a certain syntactic class of ordinary ACL2 objects, called the `tame functions' (which are in fact not functions but are merely symbols and list expressions) and we can allow names of functions with certain tameness properties to be passed around and used as functions.

      By the way, in this documentation topic we tend to display certain symbols sometimes in uppercase and sometimes in lowercase. They denote the same symbol. But we use uppercase when we're using the symbol as a quoted constant to be passed to apply$ and we use lowercase when we're using the symbol as a function symbol in a term.

      ``Tameness'' imposes strict rules on how functional arguments are used. We'll discuss it further below.

      The fundamental question raised by apply$ is ``How can apply$ know the correspondence between an ordinary ACL2 object, like a symbol or a list, and the ACL2 function the user means to apply?'' For example, if the user defines the function my-append, how can apply$ know that (apply$ 'MY-APPEND (list a b)) should expand to (my-append a b)?

      The ACL2 primitives can be built in. The logical definition of apply$ includes a big case split that recognizes about 800 ACL2 primitives, so that for example:

      (apply$ 'car (list a)) = (car a)

      and

      (apply$ 'assoc-equal (list a b)) = (assoc-equal a b).

      But user-defined functions are problematic because once apply$ has been defined in the ACL2 sources it cannot be extended to handle new symbols.

      Intuitively, if you have defined the n-ary function foo then you would expect (apply$ 'foo (list a1...an)) to be (foo a1...an). One way to arrange that might be to leave apply$ undefined on the symbol foo but to assume, as by a new axiom or hypothesis,

      forall a1...an : (apply$ 'foo (list a1...an)) = (foo a1...an).

      It will turn out that using new axioms for this purpose is a bad idea. Hiding the link between apply$ and new symbols in axioms raises a problem with ACL2's notion of local. This is called ``the LOCAL problem'' and we illustrate it later in this doc topic. But for that reason, the suppositions extending apply$ will take the form of hypotheses to be added to conjectures in which the behavior of apply$ on new symbols is important. These hypotheses are called ``warrants.''

      Warrant (Merriam-Webster): (noun) a commission or document giving authority to do something....

      In our case, a warrant for fn gives apply$ permission to apply fn under some circumstances, by asserting a universally quantified conditional equality about apply$'s behavior on 'fn. It also tells apply$ and the tameness predicates things like how many arguments fn takes and how it uses them by asserting the badge of 'fn. The badge of fn is an ACL2 object that contains various tokens interpretable by apply$ and the tameness predicates.

      But there is a fundamental logical problem: it is not always possible to satisfy such suppositions. There may be no way that apply$ could handle fn. An example of a fn for which that hypothesis is unsatisfiable is

      (defun russell (x y) (not (apply$ x (list y y)))).

      This definition of russell is not recursive: it does not call itself. So this definition is admissible. But if we had a warrant for apply$ and that warrant were as simple as

      forall x,y : (apply$ 'russell (list x y)) = (russell x y)

      then we would have this classical problem with self-reference:

      (russell 'russell 'russell)
      =                                      {def russell}
      (not (apply$ 'russell (list 'russell 'russell)))
      =                                      {warrant russell}
      (not (russell 'russell 'russell))

      which is contradictory.

      This problem is addressed by introducing the notion of ``tameness.'' Tameness is a syntactic property of terms and functions that implies that it is ok to ``extend'' apply$ to handle them.

      It should be pretty clear that if the user defines an ACL2 function that in no way depends on apply$, e.g., a function like:

      (defun sq (x) (* x x))

      then the hypothesis

      forall x : (apply$ 'SQ (list x)) = (sq x)

      is satisfiable: we could have introduced sq before apply$ and then defined apply$ in the first place to handle that particular symbol.

      Sq is a particularly simple example of a tame function. One challenge in this work has been to extend the notion of tameness so that it includes a lot of what a normal ACL2 programmer might want in apply$ while maintaining the soundness of the resulting theory.

      For example, consider the following function, which maps a given function over a list and collects the results.

      (defun my-collect$ (fn lst)
        (if (endp lst)
            nil
            (cons (apply$ fn (list (car lst)))
                  (my-collect$ fn (cdr lst)))))

      Our definition of tameness considers (my-collect$ 'SQ lst) to be a tame expression, even though my-collect$ calls apply$. The reason we can allow this is that in this particular call of my-collect$ the function to be applied is itself tame. But if (my-collect$ 'SQ lst) is a tame expression, then '(LAMBDA (LST) (MY-COLLECT$ 'SQ LST)) is a tame function and thus

      (my-collect$ '(LAMBDA (LST) (MY-COLLECT$ 'SQ LST)) z)

      is a tame expression. So, for example, at the top-level of ACL2 one can do this:

      ACL2 !>(my-collect$ '(LAMBDA (LST) (MY-COLLECT$ 'SQ LST))
                       '((1 2 3) (4 5 6) (7 8 9)))
      ((1 4 9) (16 25 36) (49 64 81))

      Of course, this presumes we have defined sq and my-collect$ and have analyzed them to make sure they have the appropriate tameness properties. (Note that my-collect$ is not tame, but the way it uses its ``functional'' argument is crucial to the tameness of (my-collect$ 'SQ lst).) To use apply$ to full advantage we need to have analyzed every relevant function definition so we know which arguments are treated like functions and whether they are used in accordance with our restrictions. So if you're defining a function you intend to apply$ it is convenient to define it with the new command defun$, which is just an ordinary defun followed by a defwarrant command. If you've already defined the function and then realize you wish to apply$ it, you can call defwarrant yourself.

      Defwarrant analyzes a :logic mode definition and produces a badge and a warrant, if possible. Also relevant is the defbadge command which issues a badge for a function (if possible) but does not issue a warrant. Its primary purpose is to allow :program mode functions to be analyzed and badged so they can be safely executed by apply$ at the top-level ACL2 loop. But the present discussion focuses primarily on the logical machinery, which requires warrants.

      We explain further via an annotated example, starting from scratch but from the basic background just sketched. For many additional examples, see community-books books/projects/apply/report.lisp which is a certified book containing the examples in the paper.

      Note carefully: the directory books/projects/apply-model/, mentioned earlier in conjunction with the paper, is different from the directory books/projects/apply/ just mentioned! The former directory concerns the logical foundations of apply$ as they stood when the paper was written. The latter is more directly relevant to ACL2 users and provides useful lemmas about apply$ as it is axiomatized and implemented today. It also includes many example theorems.

      Exercises and Lessons

      To get started, fire up your ACL2 and define two ordinary ACL2 functions, one that squares its argument and the other that reverses its argument. We show the ACL2 prompt below in front of each form we expect you to execute.

      ACL2 !>(defun sq (x) (* x x))
      
      ACL2 !>(defun rev (x)
               (if (endp x)
                   nil
                   (append (rev (cdr x)) (list (car x)))))

      Lesson 0: Learn about apply$ by reading this tutorial introduction. But this tutorial mentions many undefined concepts: tameness, warrants, badges, ilks. These concepts are intertwined with apply$ and warrants through mutual recursion, constraints, rewrite rules, etc.. So we decided not to try to define them here as we go along, though the links provided do provide definitive descriptions. So please tolerate the use of undefined words here — we'll try to give you a sense of what they mean.

      Lesson 1: To use apply$, be sure to include the following book of lemmas. These lemmas are important not just to proving theorems about apply$ but to defining functions that use apply$.

      ACL2 !>(include-book "projects/apply/top" :dir :system)

      Lesson 2: To allow apply$ to ``work'' on a function symbol the symbol must be ``warranted.'' Actually, of course, you can pass anything to apply$ and the axioms will reduce it to some value: ACL2 is untyped and all functions are total! But apply$ won't work in the logic as you expect if the first argument to apply$ is not warranted! (And apply$ won't work as you expect for top-level evaluation if its first argument is not at least badged.) To issue warrants (and badges) for sq and rev do:

      ACL2 !>(defwarrant sq)
      
      ACL2 !>(defwarrant rev)

      Defwarrant checks that its argument, fn, is a defined function symbol that satisfies certain restrictions on how it uses its arguments, restrictions that enable us to define the tameness predicates and that allow apply$ to ``work'' without causing logical contradictions. Defwarrant causes an error if fn does not obey our rules. But if defwarrant does not cause an error it produces a ``badge'' for fn that describes which formals are treated as ``functions.'' Henceforth, we'll say such formals have ``ilk'' :FN. In addition to computing a badge, non-erroneous calls of defwarrant introduce a “warrant function” for fn. The warrant function for fn is a 0-ary function named apply$-warrant-fn. A call of the warrant function, i.e., the term (apply$-warrant-fn) is called the “warrant” for fn and if the warrant for fn is included among the hypotheses of a conjecture then (apply$ 'fn (list a1 ... an)) can expand to (fn a1 ... an), provided the ai meet the tameness requirements required by fn's badge.

      Lesson 3: We'll say more about tameness, badges, and warrants later. You already know that warrants can only be issued for :logic mode functions because the function symbol is used as a function in the logical definition of the warrant. But you might as well learn four major limitations of apply$: (i) Apply$ does not take state or stobj arguments and so cannot call any function that takes STATE or stobj arguments. (ii) Apply$ cannot call a function whose measure, well-founded relation, or domain predicate depends on apply$. (iii) Apply$ cannot call a function that itself uses apply$ unless that function's measure is a natural number or a lexicographic combination of naturals formed with llist as defined in the Community Books at books/ordinals/. (iv) Apply$ cannot call a function that itself uses apply$ if that function was defined mutually recursively. Another way of saying all this is that defwarrant will cause an error if you try to warrant a function violating (i), (ii), (iii) or (iv).

      Lesson 4: If you want to define a function and immediately call defwarrant on it you can use the handy macro defun$. We'll use defun$ freely below.

      Lesson 5: You can define functions that take warranted ``functions'' as arguments and apply$ them. Here is a function that applies its first argument to every element of its second argument and collects the results. We sometimes call functions like my-collect$ ``mapping functions'' because they map another function over some range. We would call them ``functionals'' except that suggests ACL2 is higher-order and it is not! So we most often call them scions of apply$. In ordinary English usage, a ``scion'' is a descendent of an important family or individual; our scions are ``descendents'' of apply$ and inherit its power and restrictions.

      ACL2 !>(defun$ my-collect$ (fn lst)
               (if (endp lst)
                   nil
                   (cons (apply$ fn (list (car lst)))
                         (my-collect$ fn (cdr lst)))))

      In this definition, the first argument has ilk :FN because it is used exclusively as a ``function:'' it reaches the first argument of apply$ and is untouched otherwise. The second argument has ilk NIL and we say it's ``ordinary.'' It is never used as a function.

      Note: We define my-collect$ with defun$ simply to illustrate defun$. Unless we mean to pass my-collect$ to apply$ or to some scion in the future, there is no reason to have a warrant for my-collect$. Had we defined my-collect$ with the ordinary defun and realized later that we want to pass 'MY-COLLECT$ into a slot of ilk :FN, we could get a warrant for my-collect$ by calling (defwarrant my-collect$).

      Actually, the function collect$ is pre-defined in ACL2 and behaves like my-collect$. We chose to introduce my-collect$ simply to illustrate that new scions can be introduced and used. Here's another useful pre-defined scion. You won't need to define it in your ACL2 session to use it.

      (defun$ always$ (fn lst)
        (if (endp lst)
            t
            (and (apply$ fn (list (car lst)))
                 (always$ fn (cdr lst)))))

      It checks that every element of lst satisfies its :FN argument fn.

      The reason that both collect$ and always$ are pre-defined is that they are part of the support for the loop$ statment.

      Lesson 6: You can run scions on warranted function symbols:

      ACL2 !>(my-collect$ 'SQ '(1 -2 3 -4))
      (1 4 9 16)
      
      ACL2 !>(my-collect$ 'rev '((1 2 3) (4 5 6) (7 8 9)))
      ((3 2 1) (6 5 4) (9 8 7))

      You might wonder why you can run my-collect$ on 'SQ — which evaluates apply$ on 'SQ — without explicitly acknowledging the warrant that links (apply$ 'SQ (list a)) to (sq a). The reason is that evaluation in ACL2's top-level read-eval-print loop assumes all existing warrants are provided. Warrants only become important when we start dealing with proofs.

      Lesson 7: You can run scions on tame quoted LAMBDA objects. These LAMBDA objects can even include calls of scions, provided they are tame.

      ACL2 !>(my-collect$
                   (lambda$ (x) (CONS 'SQUARES (MY-COLLECT$ 'SQ x)))
                   '((1 2 3) (4 5 6)))
      ((SQUARES 1 4 9) (SQUARES 16 25 36))

      Note that the ``function symbols'' in the ``body'' of a quoted LAMBDA object may reach apply$ as the LAMBDA object is applied.

      LAMBDA objects are just quoted list expressions that start with the symbol LAMBDA and look like lambda-expressions. But quoted LAMBDA objects have to have fully translated bodies and meet other restrictions so apply$ can interpret them. You cannot use macros like + or cond and must you quote all constants. We urge you not to try to type quoted LAMBDA objects by hand! Instead, we provide a macro, lambda$, that allows you to write lambda expressions in untranslated form.

      Lesson 8: There are three very similar looking but very different notions used in this documentation: lambda expressions, LAMBDA objects, and lambda$ expressions. Read carefully! See lambda for some definitions and disambiguation help. The LAMBDA objects reaching apply$ must be fully translated (and tame) to be handled correctly. The special macro lambda$ will translate for you.

      ; Don't type quoted LAMBDA objects like this!
      ACL2 !>(my-collect$ '(LAMBDA (x)
                             (IF (< x '0) (BINARY-* '10 x) (SQ x)))
                          '(1 -2 3 -4))
      (1 -20 9 -40)
      
      ; Type this instead!
      ACL2 !>(my-collect$ (lambda$ (x)
                             (if (< x 0) (* 10 x) (sq x)))
                          '(1 -2 3 -4))
      (1 -20 9 -40)

      Lesson 9: Almost all ACL2 primitives are known to apply$. For a complete list of the built-ins evaluate

      (append '(BADGE TAMEP TAMEP-FUNCTIONP SUITABLY-TAMEP-LISTP
                      APPLY$ EV$)
              (strip-cars *badge-prim-falist*))

      You can freely use these ACL2 primitives with apply$ and in your lambda$ expressions, without warrants.

      Lesson 10: You can prove and use theorems about scions.

      ACL2 !>(defthm my-collect$-append
               (equal (my-collect$ fn (append a b))
                      (append (my-collect$ fn a)
                              (my-collect$ fn b))))
      
      ACL2 !>(thm (equal (my-collect$ (lambda$ (x) (* x x))
                                      (append c d))
                         (append (my-collect$ (lambda$ (x) (* x x)) c)
                                 (my-collect$ (lambda$ (x) (* x x)) d))))

      Notice that the lemma my-collect$-append talks about an arbitrary fn. The definition of apply$ is completely irrelevant to this theorem! Once my-collect$-append has been proved can be instantiated with anything for fn. This is demonstrated when the thm above is proved: the proof is just to rewrite with my-collect$-append. Notice that the only function being apply$'d in the thm above is the primitive multiplication function, which is built into apply$.

      Lesson 11: But when your theorems depend on the behavior of apply$ on particular user-defined functions, you will need to provide hypotheses stipulating the behavior of apply$ on those values. Those hypotheses are the warrants for the (non-primitive) function symbols involved. Here is an example: Recall the function sq defined and warranted above. We might wish to prove that if lst is a list of integers then (my-collect$ 'SQ lst) is a list of natural numbers. We can use always$ to express the notions of ``list of integers'' and ``list of naturals.'' We could try to state the conjecture this way:

      ACL2 !>(thm (implies (always$ 'INTEGERP lst)
                           (always$ 'NATP (my-collect$ 'SQ lst)))).

      But the attempt to prove that formula will fail because it depends on the fact that the sq of an integer is a natural and on the assumption that (apply$ 'SQ (list x)) is (sq x). That assumption is what the warrant for sq tells us. Thus, the warrant for sq is required as a hypothesis! The following theorem can be proved.

      ACL2 !>(defthm all-natp-collect$-sq
               (implies (and (warrant sq)
                             (always$ 'INTEGERP lst))
                        (always$ 'NATP (collect$ 'SQ lst))))

      Note that we don't need to provide warrants for integerp or natp because they are ACL2 primitives and thus built into the behavior of apply$. But we must provide the warrant for sq because we know the proof depends on (apply$ 'sq (list x1 ...)) simplifying to (sq x1).

      The macro form (warrant f1 ... fk) expands to the conjunction of the warrants for the fis. That is

      (warrant f1 ... fk)
      =
      (and (apply$-warrant-f1)
           ...
           (apply$-warrant-fk)).

      If you attempt a proof and it fails, and you see among the checkpoints terms of the form (apply$ 'fn (list a1 ... an)), then you probably forgot to call defwarrant on fn and apply$ doesn't know what to do with that symbol! If, on the other hand, you see a forcing-round checkpoint that is attempting to prove a warrant, like (apply$-warrant-fn), then you probably forgot to add the warrant for fn to the hypotheses of the conjecture you're trying to prove.

      Lesson 12: Warrants solve the ``LOCAL problem.'' Imagine the trouble we'd be in if the theorem above did not require a warrant on sq. We could get away with this:

      (encapsulate nil
        (local (defun sq (x) (* x x)))
        (defthm unwarranted-all-natp-collect$-sq
          (implies (always$ 'INTEGERP lst)
                   (always$ 'NATP (collect$ 'SQ lst)))))
      
      (defun sq (x) (* x x x))
      
      (thm (implies (always$ 'INTEGERP lst)
                    (always$ 'NATP (collect$ 'SQ lst))))

      This would be a disaster because the final thm is invalid since (sq -2) here is -8 and yet the thm is trivially proved by appealing to the unwarranted theorem exported from the encapsulate.

      If we could prove the unwarranted theorem we could export it because it does not mention or depend on the locally defined function sq, it just mentions the constant symbol 'SQ. Fortunately, we cannot actually prove the unwarranted version of the theorem because there is no a priori connection between (apply$ 'SQ (list x)) and (sq x). And if we add the warrant for sq to the defthm in the encapsulate we can prove the theorem but then we cannot export it because the warrant ancestrally depends on locally defined function sq.

      Lesson 13: While we may have given the impression that we've provided a convenient fragment of second-order functionality in ACL2 its limitations will annoy you! For example, when ACL2 tries to use the lemma

      (defthm all-natp-collect$-sq
        (implies (and (warrant sq)
                      (always$ 'INTEGERP lst))
                 (always$ 'NATP (collect$ 'SQ lst))))

      it just employs its usual first-order matching algorithm. Thus, the lemma won't apply to

      (always$ 'NATP (collect$ (lambda$ (x) (* x x)) lst))

      because the constant symbol 'SQ is not the same as the constant list generated by translating lambda$ expression, '(LAMBDA (X) (BINARY-* X X)), even though they are equivalent if understood as functions. See the discussion at fn-equal.

      Lesson 14: Recall Lesson 0! Before you start to use apply$ outside of this simple demo script, we advise you to read the documentation for apply$.

      An Advanced Lesson: We conclude this tutorial by defining one of the most useful scions and proving a couple of theorems illustrating its flexibility: foldr.

      ACL2 !>(defun$ foldr (lst fn init)
               (if (endp lst)
                   init
                   (apply$ fn
                           (list (car lst)
                                 (foldr (cdr lst) fn init)))))

      Note that foldr maps over the list in its first argument, applying its second argument to two things: successive elements of the list and the result of recursively calling itself on the rest of the list. It returns its third argument when the list is empty.

      When its functional argument is CONS foldr is just the concatenation of its other two arguments:

      ACL2 !>(defthm foldr-cons
               (equal (foldr x 'CONS y)
                      (append x y)))

      We do not need a warrant for cons because it is built into apply$. In fact, the built-ins don't have warrants but if you unnecessarily list a primitive in a warrant expression, like (warrant foldr cons), it just ignores the primitives that are built into apply$.

      By supplying a certain lambda expression we can use foldr to reverse its first argument:

      ACL2 !>(defthm foldr-can-be-rev
               (implies (warrant foldr)
                        (equal (foldr x
                                      (lambda$ (x y)
                                         (FOLDR y 'CONS (CONS x nil)))
                                      nil)
                               (rev x))))

      Note that the lambda$ expression calls FOLDR. Because of this, we must provide the warrant for foldr since that inner foldr will be applied by the outer foldr. This illustrates an important point made in Lesson 7 above: scions can apply other scions, including themselves, as long as the applications are tame.

      Some Practice Problems

      There is no better way to learn than to practice. So here are a few challenge problems. The answers can be found in books/projects/apply/answers-to-doc-intro-to-apply.lisp.

      Problem 1: Assume fn is a binary relation. Define (insert$ e lst fn) to insert e into the list lst in front of the first element, d, in lst such that (fn e d) is true.

      Problem 2: Define (sort$ lst fn) to be an insertion sort algorithm for the binary relation fn, e.g., to successively insert each element into the recursively sorted remaining elements. (Note: There is no assurance that sort$ will actually produce a list ordered by fn because we don't know that fn is an ordering relation.)

      Problem 3: Study the four examples below, which illustrate perhaps surprising properties of our ``insertion sort'' function. (If your definitions don't have these properties you should back up and redefine your functions as we vaguely described above!)

      (defthm examples-of-sort$
        (and (equal (sort$ '(1 3 -7 0 23) '<)
                    '(-7 0 1 3 23))
             (equal (sort$ '(1 3 -7 0 23)
                           (lambda$ (x y) t))
                    '(1 3 -7 0 23))
             (equal (sort$ '(1 3 -7 0 23)
                           (lambda$ (x y) nil))
                    '(23 0 -7 3 1))
             (equal (sort$ '(1 a 2 x b 3 4 y c)
                           (lambda$ (x y) (symbolp x)))
                    '(a x b y c 4 3 2 1)))
        :rule-classes nil)

      Problem 4: Prove the following theorem suggested especially by the last example above. To state this theorem we first introduce the familiar reverse function, rev.

      (defun rev (x)
        (if (endp x)
            nil
            (append (rev (cdr x))
                    (list (car x)))))

      and we use the pre-defined function (when$ fn lst) which computes the elements of lst satisfying the unary-function fn, in the order in which they occur, e.g., (when$ '(1 a 2 b) 'symbolp) is '(a b).

      Prove

      (defthm sort$-lambda-symbolp
        (implies (true-listp lst)
                 (equal (sort$ lst (lambda$ (x y) (symbolp x)))
                        (append (when$ 'symbolp lst)
                                (rev
                                  (when$
                                    (lambda$ (x y) (not (symbolp x)))
                                    lst))))))

      Lemmas will be needed.

      Problem 5: Define (orderedp$ lst fn) to check whether fn holds between each adjacent pair of elements in lst. Test your function with

      (defthm examples-of-orderedp$
        (and (orderedp$ '(1 3 5 7) '<)
             (not (orderedp '(1 3 3 5 7) '<)))
        :rule-classes nil)

      Problem 6: You might hope that (orderedp$ (sort$ lst fn) fn) is a theorem. But it is not as is easily shown by the example (orderedp$ (sort$ '(3 1 5 3 7) '<) '<). If you try to prove the conjecture and inspect the output you'll see that the proof fails because we do not know that (or (fn x y) (fn y x)) is true. That is, we don't know that fn is Strongly Connected. How could we, since the conjecture is claimed for all fn?

      Unfortunately, it is awkward to state that fn is a strongly connected relation in ACL2's first-order quantifier-free language. This is a good example of the limitations of ACL2's support for second-order functions!

      But we can prove versions of the conjecture for concrete strongly connected fns. The relation named before-dayp, below, is strongly connected, as demonstrated by the events following its definition.

      Carry out these events.

      (defun beforep (x y lst)
        (if (and (member x lst)
                 (member y lst))
            (member y (member x lst))
            t))
      
      (defun before-dayp (x y)
        (beforep x y '(mon tue wed thu fri sat sun)))
      
      (defthm before-dayp-strongly-connected
        (implies (not (before-dayp x y))
                 (before-dayp y x)))
      
      (in-theory (disable before-dayp))

      Now, prove the version of (orderedp$ (sort$ lst fn) fn) for the instance in which fn is 'before-dayp.