6
$\begingroup$

This is obviously a question inspired by can proof assistants reason about the complexity of programs?.

Here, the question involves a degree of meta-programming (or reflection if you'd prefer).

For example, it is obvious that you can't reason about the complexity of 'functions' in any assistant where funext is true. The proper question to ask (as in the title) is about programs that denote functions.

As 'complexity' is a property of programs, this should also give us that reflection is strongly incompatible with funext: if you can show that the denotations two programs p and q are (extensionally) equivalent (as functions, say $f = [\![ p ]\!]$ and $g = [\![ q ]\!]$) and you can recover p from f and q from g by reflection, you've just gotten a property that "tells apart" f and g.

$\endgroup$
4
  • $\begingroup$ Maybe Idris 2 with linear types? $\endgroup$ Commented Mar 2, 2023 at 19:08
  • $\begingroup$ Are you asking if one can say reason about the programs denoted by expressions in say Coq or Lean. So you say give me a Lean4 object p of type Expr which represents a function and I prove that the complexity of running p is such and such relative to a formal model of how p is turned into an executable in Lean? Or alternately, p is the x86 byte code which Lean generates and I reason about that? $\endgroup$
    – Jason Rute
    Commented Mar 2, 2023 at 23:09
  • 1
    $\begingroup$ The problem is complexity depends on metrics. Sometimes we want multiplication to count as one single operation, and sometimes we don't. A way to specify the metric is using a cost monad, or more practically a cost-aware logical framework. $\endgroup$
    – Trebor
    Commented Mar 3, 2023 at 0:29
  • 1
    $\begingroup$ @JasonRute I purposefully left open the question of "What is a program" to allow for multiple approaches. You could start with a data-structure Expr that denotes programs, but then you have to prove that they really do - and that your cost function is a proper model. That's hard. $\endgroup$ Commented Mar 3, 2023 at 12:36

3 Answers 3

5
$\begingroup$

I guess the answer on the question depends exactly on what you want to do.

If you want to reason solely on the complexity of functions of your language, you do not necessarily need full reflection. You can try and use cost-aware type theories, such as linear type systems. You might not even have to sacrifice function extensionality entirely, see the recent paper by Niu, Sterling, Grodin and Harper, A cost-aware logical framework which separates two "phases", one where functions are considered intentionally and bear complexity information, and one where they are considered extensionally.

If you want to go further and actually be able to reason and manipulate programs (in the sense of "object of a type Prog internal to your language representing source code of functions"), then most mature proof assistants out there have some sort of reflection available: Agda has a reflection API, Lean builds in very deeply in their philosophy to use Lean to (meta)-program Lean tactics, and Coq has the very lively MetaCoq project. However, the first two give access to reflection mainly as a tool for meta-programming, while MetaCoq explicitly aims at reasoning about programs internally to the language, although I guess you could build on both Agda's and Lean's reflection API and type of terms to reason about programs, including their complexity. Note that this would however need a lot of work, including first and foremost building a cost model for a fancy dependent type theory, which is not an easy question, already in the case of λ-calculus.

Still, all these are unsatisfactory, in the sense that they are "meta"-features: in all these systems, reflection is not a primitive of the type-theory, and so the type theory is not aware of the relation between quoted and unquoted terms. There is no way to state, let alone prove, that quote and unquote relate to each other, being in some sense inverse to one another. To be able to do that, you need to internalize them, ie turn them into proper functions of your type theory. This is deeply linked with what is called synthetic computability, an approach on computability which uses function of the ambient type theory as model of computation, relying on an axiom usually called "Church Thesis", which asserts that every function of type nat -> nat can be turned into a program. This is in fact exactly quoting, albeit restricted to the type nat -> nat! On this subject you can go look at Forster's work, for instance Church’s Thesis and Related Axioms in Coq’s Type Theory. Still, Church Thesis is only an axiom, not a proper function which computes. But as far as I know, giving a computational content to Church Thesis, and thus showing its consistency with a (dependent) type theory is the next step of the work by Forster.

$\endgroup$
2
  • 1
    $\begingroup$ Just to say, the authors of that paper are Yue Niu and Harrison Grodin in addition to Bob and myself $\endgroup$ Commented Apr 4, 2023 at 7:25
  • 1
    $\begingroup$ Thanks for pointing it out, it's corrected now $\endgroup$ Commented Apr 4, 2023 at 8:40
3
$\begingroup$

Turns out that I had completely forgotten one piece of work where this can be done: HOL Light QE, where "QE" stands for 'quote and eval'. Bill Farmer designed the logic ($\mathbf{CTT}_{qe}$), and we documented the joint work in this paper published at ITP. That's kind of embarassing, since the whole point of this logic is to know the exact relation between quote and eval as well as having them in the logic!

$\endgroup$
2
$\begingroup$

See MetaCoq: https://metacoq.github.io/.

In Coq, it allows you to parse and manipulate a Coq AST. It also includes PCUIC, a (slightly different but semantically-equivalent) variant of Coq's term language and type system (including its evaluation and reduction semantics). MetaCoq is used to auto-generate new Coq terms, but also to reason about existing terms, including about their complexity.

This paper is an example of using MetaCoq to prove time bounds of Coq functions extracted into call-by-value λ-calculus: https://www.ps.uni-saarland.de/Publications/documents/ForsterKunze_2019_Certifying-extraction.pdf.

Not complexity, but related: people have also used it to develop meta-theories around Coq's type theory (https://theowinterhalter.github.io/#phd) and verify Coq's verification (https://metacoq.github.io/coqcoqcorrect).

$\endgroup$
2
  • 1
    $\begingroup$ As far as I can tell, MetaCoq does not exactly fit the bill: the reflection features are meta-functions, not proper primitives of the language. So Coq does not "know" anything about the relation between a term obtained using MetaCoq Quote or MetaCoq Unquote and the original one. For instance, there is no way to state, let alone prove, that these should in some sense be inverse to each other. $\endgroup$ Commented Mar 3, 2023 at 9:55
  • $\begingroup$ This is a nice answer with lots of links, but I accepted @MevenLennon-Bertrand 's answer because it 1) covered a broader range of systems, and 2) discussed the fact that it is quite subtle. $\endgroup$ Commented Mar 4, 2023 at 13:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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