Email Gateway (Aug 22 2022 at 21:08): Email Gateway (Aug 22 2022 at 21:08):From: Alex Meyer <alex153@outlook.lv>
Are there some thoughts, efforts and ideas about implementing Isabelle/HOL (or part of it) on quantum computer? I am novice in quantum computing, but I can not find any guidance about quantum algorithms that are designed especially for the type theory of any kind or first-order/higher-order logic. Does quantum community call those algorithms somehow differently or have different perspective? Or maybe quantum speedup is not available for the type of reasoning that is done by Isabelle/HOL?
Alex
Email Gateway (Aug 22 2022 at 21:09):From: Thomas Sewell <sewell@chalmers.se>
A friend of mine was interested in using FPGAs to accelerate various computational tasks, and asked about Isabelle.
I think that, for these purposes, Isabelle is a functional program that does a lot of pointer chasing (searching through pointer-linked data structures). It has a lot of binary search trees and similar in its memory. There's not a lot of interesting numerical calculations. This is challenging to optimise. Existing CPUs and cache architectures are fairly well tuned for pointer chasing. I don't think that quantum or FPGAs or GPUs would be good for this workload as is: too much state and not enough computation. I'm no expert, perhaps I'll turn out to be dead wrong.
It might be possible to do surgery on Isabelle to speed up some of its common calculations, but be warned about correctness. A change which sped up the Isabelle kernel but made it less obviously correct would probably be rejected.
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 21:09):From: Dominique Unruh <unruh@ut.ee>
I think implementing Isabelle/HOL (as a whole) on a quantum computer is
not a very meaningful task. (Quantum computers shine at very specific
computational tasks but one would not write a whole application on it.)
However, I think it would be conceivable to use a quantum computer in
the implementation of certain tactics. For example, a tactic for solving
SAT (not SMT) problems could be implemented by outsourcing to a quantum
SAT solver to get a polynomial speedup. (See
https://quantumalgorithmzoo.org/, section on "Algorithm: Constraint
Satisfaction".) There exist also quantum algorithms for speeding up
backtracking (see same section), this could, hypothetically, be used to
reimplement some tactics that backtrack a lot (I think auto, simp,
blast, force, ... all do). I say hypothetically because a naïve approach
of implementing them on a quantum computer would work only in the QRAM
model (which assumes a random access in superposition of many different
memory locations) which I think is not a realistic cost model even for
long-term quantum computers. (This is because of the "pointer chasing"
that Thomas mentioned.) But maybe there are some cases where even a more
realistic memory model can be used. But this is far from obvious (at
least to me).
One note: Quantum computers tend to be noisy (i.e., make errors). But at
least for the ideas I'm mentioning above, this would not be a problem
for the soundness of Isabelle because the tactics would produce
classically checkable certificates.
Other note: I was here taking a long-term view on quantum computation.
If we are talking about NISQ (near-term), then I don't think there are
any speedups useful for Isabelle (but I would be curious to be proven
wrong on this point).
Best wishes,
Dominique.
Last updated: Apr 25 2024 at 20:15 UTC