Introduction
This page contains supplementary material of the JLAMP article A verified algorithm for deciding pattern completeness with optimal asymptotic complexity.Formalization
The formalization can be inspected in a web-browser (compiled with Isabelle 2025-1 and AFP 2025-1).Section 6.1
- theory file of formalization of sorted sets
- theory file of formalization of sorted terms
- theory file of formalization of sorted contexts
Section 6.2
- theory file of formalization of set layer
- definition of →s
- definition of mp-fail
- definition of ⇒s
- main partial correctness result: P_step_set_pcorrect
Section 6.3
- theory file of formalization of multiset layer
- new duplicate rule
- strong normalization of ⇒nd
- partial correctness of ⇒
- partial correctness of ⇒nd
- strong normalization of ⇛
- partial correctness of ⇛ (Section 4 algorithm)
- partial correctness of ⇛ (Section 5, phase one and two)
Section 6.4
- theory file of formalization of list layer
- auxiliary algorithms for non-empty sorts and finite/infinite sort detection
- correctness of decision procedure for linear pattern problems (Section 3 algorithm)
- correctness of decision procedure for arbitrary pattern problems (Section 4 algorithm)
- correctness of algorithm of phase one and phase in Section 5
- theory file of wrapper functions that use generic decision procedure
- correctness of wrapper function for pattern completeness of linear lhss (Section 3 algorithm)
- correctness of wrapper function for pattern completeness of lhss (Section 4 algorithm)
Section 6.5
- theory file of formalization of phase 3 algorithm of set layer
- theory file of formalization of phase 3 algorithm of multiset layer
- theory file of formalization of phase 3 algorithm of list layer
- theory file of formalization of phase 4 SMT solver for finite integer difference logic
- definition of measure |·|p
- result of phase three: normal forms are in finite variable form
- polynomial complexity of phase three: ⇒s implies a decrease w.r.t. |·|p
- soundness of phase three: given some solver for finite IDL problems, the algorithm is a solver for problems in finite constructor form
- soundness of phase four: the algorithm is a solver for finite IDL problems
- correctness of wrapper function for pattern completeness of lhss (Section 5 algorithm)
- combined complexity result
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 generated programs (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 present in the AFP, in entries Sorted Terms and Verifying a Decision Procedure for Pattern Completeness.