Closed Position Set - Revision history

Polygon: grammar

2026-04-02T17:26:19Z

grammar

← Older revision		Revision as of 17:26, 2 April 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Closed Position Set''' (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "[[NGram CPS\|ngram CPS]]" which was used in the [[Coq-BB5]] proof. It creates a set of tape configurations, if the set is shown to be closed without containing any halting configurations, the TM has been proven non-halting.		'''Closed Position Set''' (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "[[NGram CPS\|ngram CPS]]" which was used in the [[Coq-BB5]] proof. It creates a set of tape configurations and, if the set is shown to be closed without containing any halting configurations, the TM has been proven non-halting.

	== Method ==		== Method ==

Polygon: added Method

2026-04-02T17:22:02Z

added Method

← Older revision		Revision as of 17:22, 2 April 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Closed Position Set''' (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "[[NGram CPS\|ngram CPS]]" which was used in the [[Coq-BB5]] proof. It creates a set of tape configurations, if the set is shown to be closed without containing any halting configurations, the TM has been proven non-halting.		'''Closed Position Set''' (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "[[NGram CPS\|ngram CPS]]" which was used in the [[Coq-BB5]] proof. It creates a set of tape configurations, if the set is shown to be closed without containing any halting configurations, the TM has been proven non-halting.

			== Method ==
			CPS splits the tape into three separate regions: a left chain of segments of some length <math>L</math>, a right chain of segments of length <math>R</math> and a central segment. The segments themselves are of some fixed width <math>w</math>. The head is always between segments, pointing either left or right. During simulation, only a three segment wide window is considered. Valid positions are windows where the head is either between the left and central segments and is pointing to the left, or is between the central and right segment and is pointing to the right. The decider begins the simulation from the blank tape, simulating from one valid position to the next. If the simulation leaves the window (the head ends up at one of the edges), the window must be shifted to the side where it left, creating an unknown segment in the process. What segments can be substituted into the unknown is determined by two graphs (one for the left edge, one for the right).

			These graphs are constructed in the following way: For both graphs, vertices are segments, and edges between vertices (segments) mean that they can appear adjacent to each other. Initially both only contain the edge <math>0^{w}</math> <-- / --> <math>0^{w}</math> (<-- for the left side graph, --> for the right side graph) where <math>w</math> is the chosen segment size. When a window is shifted, one side will become too short (where the unknown segment is generated) and the other side will become too long (containing too many segments). On the graph for the side with too many segments, an edge is added from the second outermost segment to the outermost segment of the window. If the initial segment on the corresponding side (before the simulation which left too many segments) was adjacent to some segment XXXX in that sides graph, an edge must be added from it to all such segments XXXX.

			The unknown segment can be substituted by all segments on the same side as the unknown segment which are connected by an edge with the original outermost segment on that side. CPS also generates a Position Set which is formatted as a graph, where the beginning of an edge is a position, and the end of an edge is the window after simulating the machine till it runs over window's edge.

			If, during this simulation, the decider enters a loop or encounters an undefined transition, it will leave the machine undecided. A TM is decided to be non-halting by CPS if the adjacency graphs and the position set stop growing (are closed).<ref>https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f The closed position set decider, reverse-engineered from Skelet's program</ref>

	== See also ==		== See also ==
Line 20:		Line 29:
	* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps bb-simple-n-gram-cps] in Rust by Nathan Fenner		* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps bb-simple-n-gram-cps] in Rust by Nathan Fenner
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v Decider_NGramCPS.v] in Rocq by mxdys		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v Decider_NGramCPS.v] in Rocq by mxdys

			== References ==

	[[Category:Deciders]]		[[Category:Deciders]]

Polygon: Added a general description of the method

2026-04-02T16:23:42Z

Added a general description of the method

← Older revision		Revision as of 16:23, 2 April 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Closed Position Set''' (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "[[NGram CPS\|ngram CPS]]" which was used in the [[Coq-BB5]] proof.		'''Closed Position Set''' (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "[[NGram CPS\|ngram CPS]]" which was used in the [[Coq-BB5]] proof. It creates a set of tape configurations, if the set is shown to be closed without containing any halting configurations, the TM has been proven non-halting.

	== See also ==		== See also ==

Polygon: Information --> See also

2026-04-02T16:17:53Z

Information --> See also

← Older revision		Revision as of 16:17, 2 April 2026
Line 2:		Line 2:
	'''Closed Position Set''' (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "[[NGram CPS\|ngram CPS]]" which was used in the [[Coq-BB5]] proof.		'''Closed Position Set''' (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "[[NGram CPS\|ngram CPS]]" which was used in the [[Coq-BB5]] proof.

	== ~~Information~~ ==		== See also ==

	* [https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f The closed position set decider, reverse-engineered from Skelet's program]: savask's Oct 2022 Haskell implementation of CPS with extensive descriptive comments.		* [https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f The closed position set decider, reverse-engineered from Skelet's program]: savask's Oct 2022 Haskell implementation of CPS with extensive descriptive comments.

Polygon: better placement for the link

2026-03-31T21:11:04Z

better placement for the link

← Older revision		Revision as of 21:11, 31 March 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Closed Position Set''' (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "ngram CPS" which was used in the [[Coq-BB5]] proof.		'''Closed Position Set''' (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "[[NGram CPS\|ngram CPS]]" which was used in the [[Coq-BB5]] proof.

	== Information ==		== Information ==
Line 16:		Line 16:
	* [https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc skeletcps.py] in Python by Mateon1		* [https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc skeletcps.py] in Python by Mateon1

	~~[[NGram CPS\|~~n-gram CPS]]:		n-gram CPS:

	* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps bb-simple-n-gram-cps] in Rust by Nathan Fenner		* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps bb-simple-n-gram-cps] in Rust by Nathan Fenner

Polygon: /* Implementations */ linked NGram CPS

2026-03-31T21:08:38Z

Implementations: linked NGram CPS

← Older revision		Revision as of 21:08, 31 March 2026
Line 16:		Line 16:
	* [https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc skeletcps.py] in Python by Mateon1		* [https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc skeletcps.py] in Python by Mateon1

	n-gram CPS:		[[NGram CPS\|n-gram CPS]]:

	* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps bb-simple-n-gram-cps] in Rust by Nathan Fenner		* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps bb-simple-n-gram-cps] in Rust by Nathan Fenner

Int-y1: coq -> rocq

2025-08-25T09:03:22Z

coq -> rocq

← Older revision		Revision as of 09:03, 25 August 2025
Line 19:		Line 19:

	* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps bb-simple-n-gram-cps] in Rust by Nathan Fenner		* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps bb-simple-n-gram-cps] in Rust by Nathan Fenner
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/Deciders/Decider_NGramCPS.v Decider_NGramCPS.v] in ~~Coq~~ by mxdys		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v Decider_NGramCPS.v] in Rocq by mxdys

	[[Category:Deciders]]		[[Category:Deciders]]

Int-y1: Int-y1 moved page Closed Position Set (CPS) to Closed Position Set: remove acronym

2025-08-25T08:25:50Z

Int-y1 moved page Closed Position Set (CPS) to Closed Position Set: remove acronym

← Older revision		Revision as of 08:25, 25 August 2025
(No difference)

Int-y1: bold name

2025-08-25T07:05:25Z

bold name

← Older revision		Revision as of 07:05, 25 August 2025
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	Closed Position Set (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "ngram CPS" which was used in the [[Coq-BB5]] proof.		'''Closed Position Set''' (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "ngram CPS" which was used in the [[Coq-BB5]] proof.

	== Information ==		== Information ==

Polygon: Used Template:Stub

2025-08-10T22:30:23Z

Used Template:Stub

← Older revision		Revision as of 22:30, 10 August 2025
Line 1:		Line 1:
			{{Stub}}
	Closed Position Set (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "ngram CPS" which was used in the [[Coq-BB5]] proof.		Closed Position Set (CPS) is a [[Closed Set]] [[decider]] invented by [[Skelet]] and introduced to the [[bbchallenge.org]] community by savask. Since that introduction, there are many variations of the decider that have been used, notably "ngram CPS" which was used in the [[Coq-BB5]] proof.

Line 21:		Line 22:

	[[Category:Deciders]]		[[Category:Deciders]]
	~~[[Category:Stub]]~~