The Glasgow Haskell Compiler (GHC) allows programmers to use rewrite rules to optimize Haskell programs during compilation. Currently, GHC does not check the termination of the user-defined rewrite rules. If the rewrite rules are not terminating, the simplification process in the compilation goes into infinite loop. Therefore, checking the termination of rewrite rules is important. We present an automatic (non-)termination checker GSOL for GHC’s rewrite rules. We develop a general syntactic criterion for proving strong normalisation of rewrite rules based on computability predicates, and implement it using a GHC plugin mechanism. We applied GSOL to 300 existing real-world Haskell programs in Hackage. GSOL was able to check the termination of the rewrite systems in 70% of examples.
Program Display Configuration
Sun 11 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Praguechange