Experiments with context-sensitive TRSs interpreted as lazy ones

53 context-sensitive rewrite systems, taken from the termination problem database, were interpreted as lazy rewrite systems and tested for lazy termination. The context-sensitive TRSs obtained by transforming these lazy systems were checked for termination with AProVE. Two series of tests were performed; one with a time limit of 10 seconds and a second one with a time limit of 120 seconds. Table 1 shows the results of the tests.


Original system Transformed system Proved terminating as context-sensitve system (120 sec) Proved terminating as lazy system (10 sec) Proved terminating as lazy system (120 sec) Aprove output on transformed system
Ex1_2_AEL03.trs Ex1_2_AEL03_lr.trs yes yes yes Ex1_2_AEL03.out
Ex1_2_Luc02c.trs Ex1_2_Luc02c_lr.trs yes yes yes Ex1_2_Luc02c.out
Ex1_GL02a.trs Ex1_GL02a_lr.trs yes no no Ex1_GL02a.out
Ex14_AEGL02.trs Ex14_AEGL02_lr.trs yes no no Ex14_AEGL02.out
Ex14_Luc06.trs Ex14_Luc06_lr.trs no no no Ex14_Luc06.out
Ex15_Luc06.trs Ex15_Luc06_lr.trs yes yes yes Ex15_Luc06.out
Ex15_Luc98.trs Ex15_Luc98_lr.trs yes yes yes Ex15_Luc98.out
Ex16_Luc06.trs Ex16_Luc06_lr.trs yes yes yes Ex16_Luc06.out
Ex18_Luc06.trs Ex18_Luc06_lr.trs yes yes yes Ex18_Luc06.out
Ex1_GM03.trs Ex1_GM03_lr.trs no no no Ex1_GM03.out
Ex1_GM99.trs Ex1_GM99_lr.trs no no no Ex1_GM99.out
Ex1_Luc02b.trs Ex1_Luc02b_lr.trs yes yes yes Ex1_Luc02b.out
Ex1_Luc04b.trs Ex1_Luc04b_lr.trs yes yes yes Ex1_Luc04b.out
Ex1_Zan97.trs Ex1_Zan97_lr.trs yes no no Ex1_Zan97.out
Ex23_Luc06.trs Ex23_Luc06_lr.trs yes yes yes Ex23_Luc06.out
Ex24_GM04.trs Ex24_GM04_lr.trs no no no Ex24_GM04.out
Ex24_Luc06.trs Ex24_Luc06_lr.trs yes no no Ex24_Luc06.out
Ex25_Luc06.trs Ex25_Luc06_lr.trs yes yes yes Ex25_Luc06.out
Ex26_Luc03b.trs Ex26_Luc03b_lr.trs yes yes yes Ex26_Luc03b.out
Ex2_Luc02a.trs Ex2_Luc02a_lr.trs yes yes yes Ex2_Luc02a.out
Ex2_Luc03b.trs Ex2_Luc03b_lr.trs yes yes yes Ex2_Luc03b.out
Ex3_12_Luc96a.trs Ex3_12_Luc96a_lr.trs yes yes yes Ex3_12_Luc96a.out
Ex3_2_Luc97.trs Ex3_2_Luc97_lr.trs no no no Ex3_2_Luc97.out
Ex3_3_25_Bor03.trs Ex3_3_25_Bor03_lr.trs yes yes yes Ex3_3_25_Bor03.out
Ex4_4_Luc96b.trs Ex4_4_Luc96b_lr.trs yes yes yes Ex4_4_Luc96b.out
Ex4_7_15_Bor03.trs Ex4_7_15_Bor03_lr.trs yes yes yes Ex4_7_15_Bor03.out
Ex4_7_37_Bor03.trs Ex4_7_37_Bor03_lr.trs yes yes yes Ex4_7_37_Bor03.out
Ex4_7_56_Bor03.trs Ex4_7_56_Bor03_lr.trs yes yes yes Ex4_7_56_Bor03.out
Ex4_7_77_Bor03.trs Ex4_7_77_Bor03_lr.trs yes yes yes Ex4_7_77_Bor03.out
Ex49_GM04.trs Ex49_GM04_lr.trs yes yes yes Ex49_GM04.out
Ex4_DLMMU04.trs Ex4_DLMMU04_lr.trs no no no Ex4_DLMMU04.out
Ex4_Zan97.trs Ex4_Zan97_lr.trs yes yes yes Ex4_Zan97.out
Ex5_7_Luc97.trs Ex5_7_Luc97_lr.trs no no no Ex5_7_Luc97.out
Ex5_DLMMU04.trs Ex5_DLMMU04_lr.trs yes no yes Ex5_DLMMU04.out
Ex5_Zan97.trs Ex5_Zan97_lr.trs yes yes yes Ex5_Zan97.out
Ex6_15_AEL02.trs Ex6_15_AEL02_lr.trs no no no Ex6_15_AEL02.out
Ex6_9_Luc02c.trs Ex6_9_Luc02c_lr.trs yes yes yes Ex6_9_Luc02c.out
Ex6_GM04.trs Ex6_GM04_lr.trs yes yes yes Ex6_GM04.out
Ex6_Luc98.trs Ex6_Luc98_lr.trs yes yes yes Ex6_Luc98.out
Ex7_BLR02.trs Ex7_BLR02_lr.trs yes yes yes Ex7_BLR02.out
Ex8_BLR02.trs Ex8_BLR02_lr.trs yes yes yes Ex8_BLR02.out
Ex9_BLR02.trs Ex9_BLR02_lr.trs yes yes yes Ex9_BLR02.out
Ex9_Luc04.trs Ex9_Luc04_lr.trs no no no Ex9_Luc04.out
Ex9_Luc06.trs Ex9_Luc06_lr.trs yes no no Ex9_Luc06.out
ExAppendixB_AEL03.trs ExAppendixB_AEL03_lr.trs yes yes yes ExAppendixB_AEL03.out
ExConc_Zan97.trs ExConc_Zan97_lr.trs yes yes yes ExConc_Zan97.out
ExIntrod_GM01.trs ExIntrod_GM01_lr.trs yes no yes ExIntrod_GM01.out
ExIntrod_GM04.trs ExIntrod_GM04_lr.trs yes yes yes ExIntrod_GM04.out
ExIntrod_GM99.trs ExIntrod_GM99_lr.trs no no no ExIntrod_GM99.out
ExIntrod_Zan97.trs ExIntrod_Zan97_lr.trs no no no ExIntrod_Zan97.out
ExProp7_Luc06.trs ExProp7_Luc06_lr.trs yes yes yes ExProp7_Luc06.out
ExSec11_1_Luc02a.trs ExSec11_1_Luc02a_lr.trs yes yes yes ExSec11_1_Luc02a.out
ExSec4_2_DLMMU04.trs ExSec4_2_DLMMU04_lr.trs yes yes yes ExSec4_2_DLMMU04.out

Table 1: Experimental Results using context-sensitive systems of the TPDB


The proofs where conducted with AProVE Version 1.2. The reference results of proving context-sensitive termination of the input systems are taken from the results of the termination competition 2007. Note that there are 5 TRSs that are terminating, if considered context-sensitive, but cannot be proved terminating if considered lazy. At least 4 of them, namely Ex14_AEGL02, Ex1_Zan97, Ex24_Luc06 and Ex9_Luc06, are actually non-terminating in the lazy case.