Introduction
This page contains supplementary material of the JLAMP submission "A verified algorithm for deciding pattern completeness in non-deterministic polynomial time".
Formalization
The formalization can be inspected in a web-browser (compiled with Isabelle 2025 and AFP 2025).
Section 6.1
Section 6.2
Section 6.3
Section 6.4
Section 6.5
Experiments
All tests have been executed using a MacStudio (Apple M2 Max processor)
running MacOS 15.3.2.
First, we use Isabelle's code generator to obtain our
verified decision procedure as Haskell code.
Next, both the decision procedure and the tree automata tests via FORT-h 2.0 have been
compiled using the Haskell compiler ghc version 9.12.1 with -O2.
For testing the pattern completeness test within GHC tests, ghc was invoked without -O2.
Finally, for the complement algorithm we used AGCP v0.02 which was compiled
using SML New Jersey v110.99.4.
The execution time of all experiments for pattern problems are displayed in these two tables.
In each table, you can click on each experiment to see the input.
The timing information is provided in seconds (wall-clock time measurement).
Sources
The sources (Isabelle / Haskell / SML) are available in this archive.
The archive also contains instructions how to rerun the experiments.
Rerunning OUR / GHC / CO / TA / FSCD / NEW should be possible using Macos or Linux.
The Isabelle theories are partly present in the AFP, in entries Sorted Terms
and Verifying a Decision Procedure for Pattern Completeness.
These entries do not contain the theories of the new decision procedure of Section 5. We plan to submit the extended formalization as a
new AFP entry, after integration of potential reviewer comments.