Complexity:Rules - Revision history

Georg.moser at 11:58, 8 June 2012

2012-06-08T11:58:09Z

Georg.moser at 11:57, 8 June 2012

2012-06-08T11:57:53Z

Georg.moser at 11:38, 8 June 2012

2012-06-08T11:38:47Z

Georg.moser at 11:34, 8 June 2012

2012-06-08T11:34:00Z

Zini: /* Problem Sets and Problem Selection */

2011-03-01T15:13:59Z

Problem Sets and Problem Selection

Georg.moser: /* Problem Sets and Problem Selection */

2010-06-22T14:25:13Z

Problem Sets and Problem Selection

Georg.moser: /* Problem Sets and Problem Selection */

2010-06-22T14:21:38Z

Problem Sets and Problem Selection

Georg.moser: /* Problem Sets and Problem Selection */

2010-06-22T14:19:15Z

Problem Sets and Problem Selection

Georg.moser: /* Concrete syntax */

2010-06-22T14:09:53Z

Concrete syntax

Georg.moser: /* Scoring (proposals) */

2010-06-22T14:05:10Z

Scoring (proposals)

← Older revision		Revision as of 11:58, 8 June 2012
Line 4:		Line 4:

	An up to date version of the content of this page		An up to date version of the content of this page
−	can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/].	+	can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity competition].

@@ Line 1: / Line 1: @@
 <pre>
-This page is outdated an no longer maintained. An up to date version of the content of this page
+This page is outdated an no longer maintained.
 can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/].
-</pre>
 The purpose of this page is to provide a place for ongoing discussions

@@ Line 1: / Line 1: @@
-This page is outdated, and an updated version of the content of this page can now be found here: [1].
+<pre>
+This page is outdated an no longer maintained. An up to date version of the content of this page
-----
+can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/].
 The purpose of this page is to provide a place for ongoing discussions

← Older revision		Revision as of 11:34, 8 June 2012
Line 1:		Line 1:
		+	This page is outdated, and an updated version of the content of this page can now be found here: [1].
		+
		+	----
		+
	The purpose of this page is to provide a place for ongoing discussions		The purpose of this page is to provide a place for ongoing discussions
	on the rules, and to describe the current rules itself.		on the rules, and to describe the current rules itself.

@@ Line 104: / Line 104: @@
 === Problem Sets and Problem Selection ===
-* We propose to run subcategories DC and iDC on the following families from TPDB, after
+==== Testbeds ====
-<pre>
+All authors of complexity tools that participated in the last
-AG01; AotoYamada_05; Applicative_05; Applicative_first_order_05; AProVE_04; AProVE_06; AProVE_07; AProVE_08; Beerendonk_07; Bouchare_06; CiME_04; Der95; Endrullis_06; Gebhardt_06; GTSSK07;
+complexity competition agreed upon
-HirokawaMiddeldorp_04; Mixed_SRS; Mixed_TRS; Rubio_04; Secret_05_SRS; Secret_05_TRS; Secret_06_SRS; Secret_06_TRS; Secret_07_SRS; Secret_07_TRS; SK90; Strategy_removed_AG01; Strategy_removed_CSR_05;
+the following selection of examples from the TPDB. For simplicity,
-Strategy_removed_mixed_05; TCT_09; Trafo_06; Transformed_CSR_04; Various_04; Waldmann_06; Waldmann_06_SRS; Waldmann_07_size11; Waldmann_07_size12; Zantema_04; Zantema_05; Zantema_06;AProVE_09_Inductive
+we decided on
-</pre>
+using the same testbed for full and innermost rewriting. However, we
-* For categories RC and iRC, we propose to run the competition on the above families
+===== Derivational Complexity =====
-minus the SRS related families. These families were already successfully applied for the
+For derivational complexity analysis we restrict the TPDB as follows:
-competition.
+# keep only one instance of duplicated problems (modulo strategy annotations). A list of the TRSs that appear multiple times in the current TPDB version 8.0 can be found [[File:duplicates-8.0.txt|here]].
-* Family "TCT_09" should be replaced by two (much larger) families DC and RC, collected problems for derivational and runtime complexity
+===== Runtime Complexity =====
-analyis, respectively.
+For runtime complexity analysis, we further restrict the testbed for derivational complexity analysis as follows:
+# remove all examples as determined by the tool Oops that participated in the competition of 2010. A list of these examples for TPDB version 8.0 can be found [[File:Oops-8.0.txt|here]]. This step aims at eliminating trivial problems that
-* GM: Please indicate wishes for additional families till 27. 6. 2010
+## admit only 0-ary constructors, or
 ==== Selection function ====
-In the following, we denote by ''select'' the function that relates
+On the above described testbeds, a randomly chosen subset that is actually used in the competition is determined as follows.
 each family from the TPDB to the number of randomly chosen examples within this family as defined
 for the termination competition.
@@ Line 131: / Line 148: @@
 aware of different difficulties of proving complexity bounds. We do so by
 # partitioning each family ''F'' into ''n'' different sets ''F = F_1 \cup ... \cup F_n'', where the sets ''F_i'' may be seen as collections of TRSs similar in difficulty. For this years competition we propose following partitioning of a family ''F'':
-#:* '''subcategories RC, iRC and iDC:''' we propose to partition each family into
+#:* we propose to partition each family into
 #:*:(i) those upon which a polynomial bound could be shown automatically in last years competition (denoted by ''F_auto'' below) and
 #:*:(ii) those where a polynomial bound could not be shown (''F_nonauto'').
-#:* '''subcategory DC:''' as above, but we split (ii) into duplicating TRS (''F_duplicating'') and non-duplicating TRSs (note that any TRS from (i) is non-duplicating)
+# In accordance to the above described partitioning, we define a probability distribution ''p'' on ''F''. For this year's competition we propose the following distribution:
-# In accordance to the above described partitioning, we define a probability distribution ''p'' on ''F'' such that ''p(F_1) + ... + p(F_n) = 1''. For this year's competition we propose the following distribution:
+#:for all subcategories and families ''F'', we propose ''p(F_auto) = 0.4'' and ''p(F_nonauto) = 0.6''. That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Based on the probability distribution ''p'' we define the extended selection function ''select_comp(F,i) = min(|F_i|, p(i) * select(F))''. Here ''|F_i|'' denotes the size of ''F_i''.
 # From each partition ''F_i'' of a family ''F'', we randomly select ''select_comp(F,i)'' examples.

@@ Line 104: / Line 104: @@
 === Problem Sets and Problem Selection ===
-We propose to run subcategories DC and iDC
+We propose to run subcategories DC and iDC on the following families from TPDB, after
-on all TRS and SRS families from the newly organised TPDB, after
+the selection function defined below has been applied. (Note that this is essentially the
-the selection function defined below has been applied.
+current TPDB minus the families with "innermost" annotations.)
-For categories RC and iRC, we propose to run the competition on all TRS families
+These families were already successfully applied for the  2009 competition.
-after application of the selection function stated below:
 ==== Selection function ====
@@ Line 124: / Line 136: @@
 #:for all subcategories and families ''F'', we propose ''p(F_auto) = 0.4'' and ''p(F_nonauto) = 0.6'' (For the category DC, we additionally set ''p(F_duplicating) = 0.0''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''select_comp(F,i) = min(|F_i|, p(i) * select(F))''. Here ''|F_i|'' denotes the size of ''F_i''.
 # From each partition ''F_i'' of a family ''F'', we randomly select ''select_comp(F,i)'' examples.
 == Test Cases ==

@@ Line 39: / Line 39: @@
 Here "POLY(k)" abbreviates "O(n^k)" and "POLY(?)" denotes an unspecified
 polynomial.<br>
 * JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)
@@ Line 49: / Line 47: @@
 bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)
 == Rules of the Competition ==

@@ Line 28: / Line 28: @@
 Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
 so anyone who gives a better answer, gets at least one point.
 === Concrete syntax ===