Introduction
This page contains supplementary material of the FSCD paper A verified algorithm for deciding pattern completeness.Formalization
The formalization can be inspected in a web-browser (compiled with Isabelle 2024 and AFP 2024).Section 5.1
- theory file of formalization of sorted sets
- theory file of formalization of sorted terms
- theory file of formalization of sorted contexts
Section 5.2
- theory file of formalization of set layer
- definition of →s
- definition of mp-fail
- main partial correctness result
Section 5.3
- theory file of formalization of multiset layer
- new duplicate rule
- Theorem 13: strong normalization
- Theorem 13: partial correctness
Section 5.4
- theory file of formalization of list layer
- auxiliary algorithms for non-empty sorts and finite/infinite sort detection
- correctness of decision procedure for arbitrary pattern problems
- theory file of wrapper functions that use generic decision procedure
- correctness of wrapper functions for pattern completeness of lhss
- correctness of wrapper functions for strong quasi-reducibility of lhss
Experiments
All tests have been executed using a MacStudio (Apple M2 Max processor) running MacOS 14.3.1. 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.4.7 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 are displayed in this table. In the table, you can click on each experiment to see the input. The timing information is provided in seconds (wall-clock time measurement).Sources
The submitted sources (Isabelle / Haskell / SML) are available in this archive. The archive also contains instructions how to rerun the experiments. Rerunning OUR / GHC / CO / TA should be possible using Macos or Linux.The Isabelle theories are part of the AFP, in entries Sorted Terms and Verifying a Decision Procedure for Pattern Completeness.