22
votes
Accepted
When should I use De Bruijn levels instead of indices?
If we want to do evaluation in the presence of free variables ("open" evaluation), then De Bruijn levels are essential, precisely because of their support for cost-free weakening.
Generally, ...
- 2,077
18
votes
Accepted
What difficulties are there in basing a proof assistant on the $\lambda\mu$-calculus and has any proof assistant tried?
TL; DR: There are. But there are also severe difficulties that only have unsatisfactory solutions.
Let's see what bad things will happen, so we can attempt to fix it. The first thing when trying to ...
- 4,087
16
votes
Accepted
Easy ways to introduce inductive types
In principle, every indexed inductive type can be defined from $\bot$, $\top$, $\mathsf{Bool}$, $\Pi$, $\Sigma$, $\mathsf{W}$, $\mathsf{Id}$ and universes, with exactly the expected eliminators and ...
- 2,077
15
votes
What difficulties are there in basing a proof assistant on the $\lambda\mu$-calculus and has any proof assistant tried?
I think that the first question can be generalized to "What difficulties are there in adding side-effects to a proof assistant based on dependent type theory."
First-class continuations are ...
- 2,353
14
votes
Accepted
What are "fibration/cofibration" in type theory and what are their intuitions?
So, first, the origin of this term in the context of cubical type theory comes from its intended semantics, which are in turn inspired by the model-categorical semantics of homotopy type theory. Let's ...
- 516
13
votes
Tutorial implementations of NbE
Daniel Gratzer has written two tutorial implementations of normalization by evaluation in OCaml:
https://github.com/jozefg/nbe-for-mltt: plain MLTT with universes
https://github.com/jozefg/blott: a ...
10
votes
What are "fibration/cofibration" in type theory and what are their intuitions?
Let me provide a slightly watered up supplement of Gratzer's answer.
In the beginning, mathematicians need to study spaces by considering how other spaces cover(*) them. For example, if you have a ...
- 4,087
10
votes
Accepted
What is a neutral term?
A neutral term is a variable, or an eliminator stuck on a neutral term. Basically a stack of eliminators applied to a variable.
These terms are called neutral, and distinguished from other normal ...
- 376
9
votes
Accepted
How to implement a visual proof assistant?
Your question is pretty broad.
How would I implement and reason about a graphical calculus or proof assistant?
First (almost tautologically) I think you need to carefully consider two questions:
...
- 9,663
9
votes
Can a proof engine be built based on graphs?
Your question is quite vague, but can be answered positively when taken literally. Indeed, most implementations of a deductive system are actually already using graphs internally.
When phrased ...
- 2,353
7
votes
What is the state of recompilation avoidance in proof assistants?
Lean (in any version) at the time of writing does not really implement any sort of recompilation avoidance beyond the make approach. In particular, the produced <...
- 1,682
7
votes
Accepted
Normalization by evaluation for extensional type theories
For many partial languages, although conversion is undecidable, we can decide conversion up to non-termination. For example, in pure LC, conversion is decidable for the
$\beta$-normalizing terms.
In ...
- 2,077
7
votes
Binding variables to terms involving later variables
Great question Mike!
Since Thierry Coquand's talk at the 1991 TYPES meeting in Edinburgh, and reading Martin Löf's "Mathematics of infinity" paper, and various things by Thierry subsequently,...
6
votes
Algorithm for the locally nameless representation used by Lean
I implemented the spartan type theory as an educational tool for people who are interested in implementing their own formal systems. If you look at how the type of expressions ...
- 10.1k
6
votes
Accepted
Do implementations of a PA and of ATP have overlap?
Unfortunately there is much less code reuse possible than one would hope.
There three levels to consider:
Differences between mathematical foundations (and implementations) between proof assistants.
...
6
votes
Accepted
Comparison of normal forms in Normalization by Evaluation
I will present the conversion procedure that is used in András Kovács' Elaboration zoo and its extension to the η-rule for the unit type. It is based on Coquand's type-checking algorithm.
In ...
5
votes
Accepted
Can a proof engine be built based on graphs?
Well, a proof engine is built atop a proof calculus, right? And natural deduction basically amounts to using a specific set of possible labeled edges in graphs for proofs (namely, introduction and ...
- 1,574
5
votes
What is the state of recompilation avoidance in proof assistants?
For metamath, we store a detailed set of proof steps for each theorem or lemma along with what we are proving. As you describe in your discussion of systems which don't export their proofs, it is the ...
- 231
5
votes
What is the state of recompilation avoidance in proof assistants?
Agda has a very rudimentary form of caching of the current file, where it does not have to recheck the initial part of a file that has not changed since the last reload. See https://github.com/agda/...
- 506
5
votes
How to implement a visual proof assistant?
A graphical proof assistant for higher categories under active development is homotopy.io, which follows the tradition of Globular. The underlying notion of higher structure used by homotopy.io is ...
- 665
5
votes
Accepted
Tutorial implementation of analytic tableaux
As far as I'm aware, leanTAP was written in just a few lines of Prolog, and it works with first-order formulas in Skolem normal forms. There's a tutorial implementation in OCaml which looks similar to ...
5
votes
Binding variables to terms involving later variables
Coq (and probably Lean too):
The answer for (vanilla) Coq is simple: it does not. Nothing is done to n to remember its relation to the pattern in the branch. The ...
- 5,645
5
votes
Accepted
A $\mu$-recursive function converges at an input, how to find the output?
You are lucky: this should be provable, entirely axiom-free! Albeit with some sweat.
The core idea is that while the general axiom of constructive indefinite description you mention is not provable in ...
- 5,645
4
votes
Accepted
How to implement the type checking of `transp` in de Morgan cubical type theory?
For example, if $i∧j∨k∧(¬l)=1$, then what? What should I do to $A$?
As Trebor said, for $ i_1 ∧ i_2 ∧ … ∧ i_n = 1 $ we should perform n substitutions and check that $ A(i_1/1, i_2/1, …, i_n/1) = A(...
- 272
4
votes
Accepted
How does substitution on partial elements/systems (in terms of cubical) work?
In other words, does substitution on partial elements create more clauses?
Do they share the same clause body?
Yes, you may check both in Cubical Agda:
...
- 272
4
votes
What makes a proof assistant a proof assistant?
Since this question made it back up to the top, let me take a stab. In short, there is going to be no air-tight definition of a "proof assistant" just like there is no air-tight definition ...
- 9,663
4
votes
How to elaborate with dependent records present?
You can:
Complain that not enough typing information has been given, the same way that you would complain if the input is just a bare λ x → x. Bidirectional type ...
- 10.1k
4
votes
Accepted
Architecture of Isabelle: What parts are written in SML? What parts are written in Scala? What does the boundary look like?
Scala appears to use the JVM, and this has been marketed as a feature, not a bug.
According to Isabelle/Scala:
Isabelle/ML is for ‹mathematics›, to develop tools within the context of symbolic logic, ...
- 1,574
3
votes
Tutorial implementations of NbE
Does code in paper format count? In which case I would throw in
Danvy, Keller, and Puech's Typeful Normalization by Evaluation
You get an intro to deep vs. shallow, an analogy with printf, and an ...
- 1,264
3
votes
Creating a proof assistant for first order logic in Haskell
I am planning to implement a FOL proof assistant in Haskell. What are some useful libraries and implementations I should be looking at?
Does this do the Haskell part of what you need? I ask because ...
- 2,846
Only top scored, non community-wiki answers of a minimum length are eligible