3
$\begingroup$

This is a related question to

Is there a consolidated or partial list noting the use of quasiquotation with provers?

for which it seems there is no answer. However as there might be an answer some day am leaving that question and asking this question that others are dancing with in the comments of that question.

As this will be an open ended list type question, do not expect an accept vote on any answer. If you know of a prover (proof assistants, theorem provers, interactive theorem prover) that is making use of a system of quoting that derives from Lisp quote then just add an answer.

If you do not know what

  • Lisp quote
    or
  • quasiquotation

are please do not answer. It took me a few years before I really understood quasiquotations and a few more to learn much of the heredity.

$\endgroup$
13
  • 1
    $\begingroup$ As some of the comments in the other question are valid answers for this question, do NOT steal those from the person who made the comment. $\endgroup$
    – Guy Coder
    Mar 15 at 14:22
  • 1
    $\begingroup$ "If you do not know what Lisp quote or quasiquotation are do not answer." - why? What does this have to do with Lisp? You should add explanation if this is critical in that case. $\endgroup$
    – Wno-all
    Mar 16 at 0:14
  • 1
    $\begingroup$ Are you referring to some features exclusive to Lisp? It is entirely possible that someone is proficient in quotation and quasiquotation without learning Lisp at all. $\endgroup$
    – Trebor
    Mar 16 at 3:26
  • $\begingroup$ @Wno-all What does this have to do with Lisp? The origin of quote and its heredity started from Lisp. $\endgroup$
    – Guy Coder
    Mar 16 at 7:46
  • 2
    $\begingroup$ Perhaps write it the other way round. I parsed it as “Lisp {quote or quasiquotation}”, when I guess you intended “{Lisp quote} or quasiquotation”. $\endgroup$
    – mudri
    Mar 16 at 19:23

4 Answers 4

6
$\begingroup$

HOL Light-QE, source available from github. QE = quote-and-eval.

$\endgroup$
4
  • 1
    $\begingroup$ Could you give a simple example of what an expression using quasiquotations would look like in HOL Light-QE? $\endgroup$
    – Couchy
    Mar 16 at 16:29
  • $\begingroup$ @Couchy see the various examples in the directory github.com/JacquesCarette/hol-light-qe/tree/master/… . $\endgroup$ Mar 16 at 17:09
  • $\begingroup$ @JacquesCarette Thanks, I was not sure where to look. Although a simple example would still help as someone not familiar with HOL Light. $\endgroup$
    – Couchy
    Mar 16 at 17:48
  • 1
    $\begingroup$ The follow-up paper we were writing that would have contained many simple examples got stalled. $\endgroup$ Mar 17 at 18:39
3
$\begingroup$

quasi-quote

A quasi-quoting library for Agda, supporting automatic de Bruijn management. Very much work-in-progress. Requires the experimental branch of the standard library at commit bee4f912f or later.

$\endgroup$
1
  • $\begingroup$ It's quite likely that the bit about version requirements is out of date, given that the last commit was back in October 2020. $\endgroup$
    – mudri
    Mar 16 at 19:26
3
$\begingroup$

Lean 4 has an extensive quasiquoting notation into Lean.Syntax, Lean 4's concrete syntax tree type:

`(fun $discrs* =>
    match $[$discrs:ident],* with
    | $ps1,* => $rhs1
    $alts:matchAlt*)

The "extended" antiquotation syntax displayed here is directly inspired by that in Rust. The details are described in §4.1 of Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. As Lean 4 is implemented in Lean, syntax quotations are used pervasively throughout its implementation.


People familiar with Lean 3 might be surprised to hear that unlike in Lean 3, there is no built-in quotation support for the kernel term type Lean.Expr in Lean 4. The simple reason for that is that the need for it did not come up during development, as the terms that need to be synthesized in the core system usually consist of a single application of a certain constant to some arguments or similarly simple structures. The Lean 3 implementation was also limited by the lack of type information for the quoted expression. Gabriel Ebner's library quote4 for type-safe expression quoting fixes this issue.

def betterApp {α : Q(Sort u)} {β : Q($α → Sort v)}
  (f : Q((a : α) → $β a)) (a : Q($α)) : Q($β $a) :=
q($f $a)

#eval betterApp q(Int.toNat) q(42)
$\endgroup$
2
$\begingroup$

ACL2 supports quasiquotations entirely derived from lisp:

(defun app (binop args)
   (if args
      (if (cdr args)
          `(,binop ,(car args) ,(app binop (cdr args)))
          (car args))
      0))
      
(defmacro add (&rest rst)
   (app 'binary-+ rst))

For example we get

ACL2 !> (app 'binary-+ '(1 2 3))
(BINARY-+ 1 (BINARY-+ 2 3))

ACL2 !> (add 1 2 3)
6
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.