Complexity:Rules - Revision history

Georg.moser at 11:58, 8 June 2012

2012-06-08T11:58:09Z

← 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].

Georg.moser at 11:57, 8 June 2012

2012-06-08T11:57:53Z

← Older revision		Revision as of 11:57, 8 June 2012
Line 1:		Line 1:
	<pre>		<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.
			</pre>

			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/].
	~~</pre>~~

			----

	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

Georg.moser at 11:38, 8 June 2012

2012-06-08T11:38:47Z

← Older revision		Revision as of 11:38, 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].		<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/].
			</pre>

	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

Georg.moser at 11:34, 8 June 2012

2012-06-08T11:34:00Z

← 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.

Zini: /* Problem Sets and Problem Selection */

2011-03-01T15:13:59Z

Problem Sets and Problem Selection

← Older revision		Revision as of 15:13, 1 March 2011
Line 104:		Line 104:

	=== Problem Sets and Problem Selection ===		=== Problem Sets and Problem Selection ===
	* We propose to run subcategories DC and iDC on the following families from TPDB, after		==== Testbeds ====
	~~the selection function defined below has been applied. (Note that this is essentially the~~
	~~current TPDB minus the families with "innermost" annotations.)~~
	~~These families were already successfully applied for the 2009 competition.~~

	~~<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
			decided on
			two separate testbeds for derivational and runtime complexity
			analysis. The testbeds
			are described below in detail, additionally a list of
			problems for TPDB version 8.0 is provided for [[File:RC-8.0.txt\|RC]] and [[File:DC-8.0.txt\|DC]]. For the
			individual
			subcategories RC, RCi, DC and DCi all strategy and start-term
			annotations should be overwritten
			appropriately. Thus we simply ignore for instance
			context-sensitive strategies.

	* 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:
	~~2009 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]].
			# remove all problems with relative, theory or conditional annotations. The reason for this is that none of the tools can handle those problems currently.

	* 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
			## admit only 0-ary defined function symbols, or
			## admit only rules with nested defined function symbols on left-hand sides, thus all basic terms are normal forms.
			# remove higher-order examples from following folder, as here the notion of runtime complexity is inapropriate:
			## AotoYamada_05,
			## Applicative_05,
			## Applicative_AG01_innermost,
			## Applicative_first_order_05, and
			## Mixed_HO_10.

	==== Selection function ====		==== 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.
			Here we denote by ''select'' the function that relates
	each family from the TPDB to the number of randomly chosen examples within this family as defined		each family from the TPDB to the number of randomly chosen examples within this family as defined
	for the termination competition.		for the termination competition.
Line 131:		Line 148:
	aware of different difficulties of proving complexity bounds. We do so by		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'':		# 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		#:*:(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'').		#:*:(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''.
	#: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.		# From each partition ''F_i'' of a family ''F'', we randomly select ''select_comp(F,i)'' examples.

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

2010-06-22T14:25:13Z

Problem Sets and Problem Selection

← Older revision		Revision as of 14:25, 22 June 2010
Line 104:		Line 104:

	=== Problem Sets and Problem Selection ===		=== Problem Sets and Problem Selection ===
	We propose to run subcategories DC and iDC on the following families from TPDB, after		* We propose to run subcategories DC and iDC on the following families from TPDB, after
	the selection function defined below has been applied. (Note that this is essentially the		the selection function defined below has been applied. (Note that this is essentially the
	current TPDB minus the families with "innermost" annotations.)		current TPDB minus the families with "innermost" annotations.)
Line 112:		Line 112:
	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;		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;
	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;		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;
	Strategy_removed_mixed_05; 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		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
	</pre>		</pre>

	For categories RC and iRC, we propose to run the competition on the above families		* For categories RC and iRC, we propose to run the competition on the above families
	minus the SRS related families. These families were already successfully applied for the		minus the SRS related families. These families were already successfully applied for the
	2009 competition.		2009 competition.

			* Family "TCT_09" should be replaced by two (much larger) families DC and RC, collected problems for derivational and runtime complexity
			analyis, respectively.

			* GM: Please indicate wishes for additional families till 27. 6. 2010

	==== Selection function ====		==== Selection function ====

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

2010-06-22T14:21:38Z

Problem Sets and Problem Selection

← Older revision		Revision as of 14:21, 22 June 2010
Line 110:		Line 110:

	<pre>		<pre>
	AG01; AotoYamada_05; Applicative_05; Applicative_first_order_05; AProVE_04; AProVE_06; AProVE_07;		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;
	AProVE_08; Beerendonk_07; Bouchare_06; CiME_04; Der95; Endrullis_06; Gebhardt_06; GTSSK07;		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;
	HirokawaMiddeldorp_04; Mixed_SRS; Mixed_TRS; Rubio_04; Secret_05_SRS; Secret_05_TRS; Secret_06_SRS;		Strategy_removed_mixed_05; 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
	Secret_06_TRS; Secret_07_SRS; Secret_07_TRS; SK90; Strategy_removed_AG01; Strategy_removed_CSR_05;
	Strategy_removed_mixed_05; 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
	</pre>		</pre>

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

2010-06-22T14:19:15Z

Problem Sets and Problem Selection

← Older revision		Revision as of 14:19, 22 June 2010
Line 104:		Line 104:

	=== Problem Sets and Problem Selection ===		=== 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:~~
			<pre>
			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;
			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;
			Strategy_removed_mixed_05; 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
			</pre>

			For categories RC and iRC, we propose to run the competition on the above families
			minus the SRS related families. These families were already successfully applied for the
			2009 competition.

	==== Selection function ====		==== 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''.		#: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.		# From each partition ''F_i'' of a family ''F'', we randomly select ''select_comp(F,i)'' examples.


	== Test Cases ==		== Test Cases ==

Georg.moser: /* Concrete syntax */

2010-06-22T14:09:53Z

Concrete syntax

← Older revision		Revision as of 14:09, 22 June 2010
Line 39:		Line 39:
	Here "POLY(k)" abbreviates "O(n^k)" and "POLY(?)" denotes an unspecified		Here "POLY(k)" abbreviates "O(n^k)" and "POLY(?)" denotes an unspecified
	polynomial.<br>		polynomial.<br>

	~~<em>resolved</em>~~

	* 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)		* 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)		bound and INF for the upper bound. [[User:Noschinski\|Noschinski]] 13:26, 13 February 2010 (UTC)

			* GM: I don't like the format "POLY(k)" mainly due to presentation reasons: Our first format used exactly this and in presentations I immediately got the question
			what "POLY(k)" should mean. Since "O(k)" is used I don't get this question. With respect to the lower-bound: I agree that "O(k)" should be replaced by
			"Omega(k)". So let's do that. But I don't see a chance to change this for the upcoming competition ...

	== Rules of the Competition ==		== Rules of the Competition ==

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

2010-06-22T14:05:10Z

Scoring (proposals)

← Older revision		Revision as of 14:05, 22 June 2010
Line 28:		Line 28:
	Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -		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.		so anyone who gives a better answer, gets at least one point.

			* GM: For clarification: I suppose you want to use the following order: POLY >= O(n^7) >= O(n^6) etc. to name an example. And I would insist
			on the use of a virtual prover: getting 0 points although an answer has been given I don't like

	=== Concrete syntax ===		=== Concrete syntax ===