It is currently Thu Mar 28, 2024 1:40 pm

All times are UTC - 8 hours [ DST ]




Post new topic Reply to topic  [ 7 posts ] 
Author Message
Offline
 Post subject: Research Summary
Post #1 Posted: Sat Jul 03, 2010 12:27 am 
Judan

Posts: 6087
Liked others: 0
Was liked: 786
Chris Dams's proof:

From: Chris Dams <chr...@wn5.nospamplease.nl>
Newsgroups: rec.games.go
Subject: Re: Model for the World Amateur Go Championship Rules
Date: Wed, 12 Apr 2006 20:56:06 +0000 (UTC)
Message-ID: <e1jph6$13q$1@wnnews.sci.kun.nl>
References: <p67q32p0mo82bm1c2h5gpolhs93hncpu52@4ax.com> <e1j9jn$pla$1@wnnews.sci.kun.nl> <27gq32p0vhdvn6j0e5o1fneud7erkaas4a@4ax.com>


Dear Robert,

Robert Jasiek <jas...@snafu.de> writes:

>On Wed, 12 Apr 2006 16:24:23 +0000 (UTC), Chris Dams
><chr...@wn5.nospamplease.nl> wrote:
>>> In a position, a string of a player is _two-eye-alive_ if the
>>>opponent cannot force no intersection of the string with a
>>>two-eye-formation on.
>>
>>> _J2003-alive_ is defined like in J2003 as either uncapturable,
>>>capturable-1, or capturable-2.
>>
>>> In a position, a string is _WAGC-alive-in-seki_ if it is
>>>J2003-alive and not two-eye-alive.
>>
>>> In a position, a string is _WAGC-alive_ if it is either
>>>two-eye-alive or WAGC-alive-in-seki.
>>
>>From these definitions it follows that WAGC-alive is identical to
>>J2003-alive.

>I doubt this. If you claim it, then please present a formal proof!

I have to admit that I, at first, interpreted "either" as "or" in the definition of WAGC-alive. However, I think the identity of J2003-alive and WAGC-alive is still provable. Proof is given below.

Let us denote

> In a position, a string is _WAGC-alive-in-seki_ if it is
> J2003-alive and not two-eye-alive.

as

WAGC-alive-in-seki == J2003-alive && (!two-eye-alive)

In the same notation we also have from

> In a position, a string is _WAGC-alive_ if it is either
> two-eye-alive or WAGC-alive-in-seki.

WAGC-alive == two-eye-alive ^^ WAGC-alive-in-seki.

Substituting the former into the latter expression, we find

WAGC-alive == two-eye-alive ^^ (J2003-alive && (!two-eye-alive)).

In propositional calculus this reduces to

WAGC-alive == J2003-alive || two-eye-alive.

If we now also have the implication two-eye-alive -> J2003-alive if follows that

WAGC-alive == J2003-alive.

For the implication two-eye-alive->J2003-alive, imagine that a string is two-eye-alive. The string can either be uncapturable or not uncapturable.
(1) The string is uncapturable -> It is J2003-alive
(2) It is not uncapturable -> The string is either capturable-1 or not capturable-1
(2a) It is capturable-1 -> It is J2003-alive
(2b) It is not capturable-1 -> Because the string is two-eye-alive there is in every hypothetical-strategy of its opponent a hypothetical-sequence in which we reach a two-eye-formation that includes one of its intersections. For every hypothetical-strategy H of the opponent, we choose a hypothetical-sequence S(H) in it where the oponent reaches a two-eye-formation and subsequently only passes. Because the two-eye-formation cannot be capture by only moves of its opponent, it consists of permanent stones. In S(H) the two-eye-formation that is formed on the captured string has either a stone on local-1 of the string or it does not have a stone on local-1 of the string
(2b1) If it has a stone on local-1 of the string, it is also on local-2.
(2b2) If it does not have a stone on local-1 of the string, then local-1 of the string consists of the one or both of the empty intersections of the two-eye-formation. Actually, it consists of one of the intersections since if it would consist of both, these would have to be adjacent to each other which contradicts the definition of a two-eye-formation. So, local-1 of the string consists of one intersection and during S(H) it becomes one of the the empty points of a two-eye-formation. This implies that this two-eye formation includes strings that occupy the intersections adjacent to local-1. Because local-1 consists of one intersections these adjacent intersections where empty or occupied by opposing stones. Hence, these intersections belong to local-2 of the string.
In both (2b1) and (2b2) we see that the two-eye-formation that is formed in S(H) has permanent stones on local-2 of the string. Hence, if every hypothetical-strategy of the opponent of the string there is a hypothetical-sequence where a permanent-stone is played on local-2. Hence, the opponent cannot force both caputre of the string and no local-2 permanent stone. Hence, the string is capturable-2.
Hence, it is J2003-alive.
Hence, under the assumption that the string is two-eye-alive, we find that it is J2003-alive. QED.

Best,
Chris






Start of Chris Dams's proof written down differently (Jasiek):

Proposition:

In a position, let X be an arbitrary, fixed string.

X is WAGC-alive <==> X is J2003-alive.


Start of a Proof:

"X is WAGC-alive <==> X is J2003-alive"
<==>
"X is two-eye-alive XOR X is WAGC-alive-in-seki <==> X is J2003-alive"
<==>
"X is two-eye-alive XOR (X is J2003-alive AND NOT (X is two-eye-alive) <==> X is J2003-alive"
<==>
"
Case 1: X is two-eye-alive:
X is two-eye-alive <==> X is J2003-alive
Case 2: NOT (X is two-eye-alive):
X is J2003-alive <==> X is J2003-alive
"

Up to here, Case 2 is proven. To prove all, what remains to be proven is is Case 1. This is to be done below.

"X is two-eye-alive <==> X is J2003-alive"
<==>
"X is two-eye-alive <==> X is uncapturable XOR X is capturable-1 XOR X is capturable-2"

This is still to be proven in this proof scheme. See Chris Dams's proof for that.






Presuppositions for WAGC-alive == J2003-alive (Jasiek):

These terms are defined in the following extract of J2003/35a:

position, string(s), player, (opponent, by "player" and standard context), intersection(s), adjacent, force

"Axioms [...] A player can force something if there is at least one hypothetical-strategy of his so that each compatible hypothetical-sequence fulfils that something."


These terms are defined in the following extract of J2003/35a:

uncapturable, capturable-1, capturable-2

"Axioms [...] A player's final-string is capturable-2 if
* it is neither uncapturable nor capturable-1 and
* the opponent cannot - with the same hypothetical-strategy - force both capture of the string's stones and no local-2 permanent-stone of the player."


J2003's alive is defined by the aforementioned extrat and this citation:

"A final-string is alive if it is either
* uncapturable,
* capturable-1, or
* capturable-2."


The WAGCmod page simply gives this an alias: J2003-alive.


"two-eye-formation" and "two-eye-alive", using more basic terms, are defined on WAGCmod.


"WAGC-alive-in-seki" is defined on WAGCmod, uses "two-eye-alive", which is defined on WAGCmod, and uses J2003-alive, which is defined in J2003/35a under a different alias. See above.


"WAGC-alive" is defined on WAGCmod and uses "two-eye-alive" and "WAGC-alive-in-seki", see above.


Furthermore, as explained earlier, "WAGC-alive equals J2003-alive" relies on a particular, presumed position and a arbitrary, fixed string.







Proposition (Jasiek):

Given a string in a position, the set-intersection of two-eye-alive and WAGC-alive equals the set-intersection of two-eye-alive and J2003-alive.

Proof:

This follows immediately from the definitions and Chris Dams's proof. QED.

Note:

If you don't see it immediately for J2003-alive=>WAGC-alive, write down these two assumption cases: 1) The string is J2003-alive and two-eye-alive. 2) The string is J2003-alive and not two-eye-alive. Prove it for each case.






Example (Cassandra):

Click Here To Show Diagram Code
[go]$$
$$ -----------------
$$ | X X X . X X X |
$$ | X O O O O O X |
$$ | X O . O . O X |
$$ | X O O O O O X |
$$ | O X X X X X O |
$$ | O X . X . X O |
$$ | O X X X X X O |
$$ | O O O . O O O |
$$ -----------------[/go]








Definitions (Cassandra, Jasiek):

A string is "capturable" unless it is uncapturable.

For a player's final-string, "local-2\1" is local-2 without local-1.

A player's neither uncapturable nor capturable-1 final-string is capturable-2\1 if the player moving second can force at least one permanent-stone of his on local-2\1.






Proposition (Jasiek):

The player cannot force a local-2 permanent-stone.

=>

The player cannot force a local-1 permanent-stone
AND
The player cannot force a local-2\1 permanent-stone

Proof:

Trivial.





The second part of Chris Dams's proof for "WAGC-alive equals J2003-alive" is done in an alternative way by Cassandra with help from Jasiek:


For the implication two-eye-alive -> J2003-alive, imagine that a string is two-eye-alive. Either the opponent cannot force capture of the string or he can force capture of the string.

(1) The opponent cannot force capture of the string -> It is uncapturable. -> It is J2003-alive.

(2) The opponent can force capture of the string. -> Because the string is two-eye-alive there is in every hypothetical-strategy of its opponent a hypothetical-sequence in which we reach the player's two-eye-formation that includes one of its intersections. For every hypothetical-strategy H of the opponent, we choose a hypothetical-sequence S(H) in it where the player reaches such a two-eye-formation and subsequently only passes. Because the two-eye-formation cannot be captured by only moves of its opponent, it consists of permanent-stones. -> In S(H) the two-eye-formation that is formed on at least one intersection of the captured string has either a stone on local-1 of the string or it does not have a stone on local-1 of the string.

(2a) The two-eye-formation has a stone on local-1 of the string -> the string is capturable-1 -> It is J2003-alive.

(2b) The two-eye-formation has no stone on local-1 of the string -> Local-1 of the string consists of one or both of the empty intersections of the two-eye-formation. Actually, it consists of one of the intersections since if it would consist of both, these would have to be adjacent to each other which contradicts the definition of a two-eye-formation. So, local-1 of the string consists of one intersection and during S(H) it becomes one of the empty points of a two-eye-formation. This implies that this two-eye-formation includes strings that occupy the intersections adjacent to local-1. Because local-1 consists of one intersection these adjacent intersections were empty or occupied by opposing stones. Hence, these intersections belong to local-2\1 of the string. We see that the two-eye-formation that is formed in S(H) has permanent-stones on local-2\1 of the string. Hence, in every hypothetical-strategy of the opponent of the string there is a hypothetical-sequence where a permanent-stone is played on local-2\1. Hence, the opponent cannot force both capture of the string and no local-2\1 permanent-stone. Hence, the string is capturable-2\1. Hence it is capturable-2. Hence, it is J2003-alive.

Hence, under the assumption that the string is two-eye-alive, we find that it is J2003-alive. QED.





WAGC-alive-2\1 equals J2003-alive-2\1

Given a final-position, a string in it, and the definitions of local-2\1, capturable-2\1, J2003-alive-2\1, WAGC-alive-in-seki-2\1, WAGC-alive-2/1.

Proposition (Jasiek):

The string is WAGC-alive-2\1 equals the string is J2003-alive-2\1.

Proof:

Part 1 of the proof is analogue to part 1 of Chris Dams's proof.

Part 2 of the proof is as follows:

For the implication two-eye-alive -> J2003-alive-2\1, imagine that a string is two-eye-alive. Either the opponent cannot force capture of the string or he can force capture of the string.

(1) The opponent cannot force capture of the string -> It is uncapturable. -> It is J2003-alive-2\1.

(2) The opponent can force capture of the string. -> Because the string is two-eye-alive there is in every hypothetical-strategy of its opponent a hypothetical-sequence in which we reach the player's two-eye-formation that includes one of its intersections. For every hypothetical-strategy H of the opponent, we choose a hypothetical-sequence S(H) in it where the player reaches such a two-eye-formation and subsequently only passes. Because the two-eye-formation cannot be captured by only moves of its opponent, it consists of permanent-stones. -> In S(H) the two-eye-formation that is formed on at least one intersection of the captured string has either a stone on local-1 of the string or it does not have a stone on local-1 of the string.

(2a) The two-eye-formation has a stone on local-1 of the string -> the string is capturable-1 -> It is J2003-alive-2\1.

(2b) The two-eye-formation has no stone on local-1 of the string -> Local-1 of the string consists of one or both of the empty intersections of the two-eye-formation. Actually, it consists of one of the intersections since if it would consist of both, these would have to be adjacent to each other which contradicts the definition of a two-eye-formation. So, local-1 of the string consists of one intersection and during S(H) it becomes one of the empty points of a two-eye-formation. This implies that this two-eye-formation includes strings that occupy the intersections adjacent to local-1. Because local-1 consists of one intersection these adjacent intersections were empty or occupied by opposing stones. Hence, these intersections belong to local-2\1 of the string. We see that the two-eye-formation that is formed in S(H) has permanent-stones on local-2\1 of the string. Hence, in every hypothetical-strategy of the opponent of the string there is a hypothetical-sequence where a permanent-stone is played on local-2\1. Hence, the opponent cannot force both capture of the string and no local-2\1 permanent-stone. Hence, the string is capturable-2\1. Hence, it is J2003-alive-2\1.

Hence, under the assumption that the string is two-eye-alive, we find that it is J2003-alive-2\1. QED.





Proposition (Jasiek):

The set of capturable-2\1 strings is a subset of the set of capturable-2 strings.

Proof:

"Trivial."

Top
 Profile  
 
Offline
 Post subject: Re: Research Summary
Post #2 Posted: Sat Jul 03, 2010 12:42 am 
Judan

Posts: 6087
Liked others: 0
Was liked: 786
List of Proven Propositions


Proposition 1:

In a position, let X be an arbitrary, fixed string.

X is WAGC-alive <==> X is J2003-alive.


Remark:

This can be proven using local-2 or instead using local-2\1.


Proposition 2:

Given a string in a position, the set-intersection of two-eye-alive and WAGC-alive equals the set-intersection of two-eye-alive and J2003-alive.


Definitions:

A string is "capturable" unless it is uncapturable.

For a player's final-string, "local-2\1" is local-2 without local-1.

A player's neither uncapturable nor capturable-1 final-string is capturable-2\1 if the player moving second can force at least one permanent-stone of his on local-2\1.


Proposition 3:

The player cannot force a local-2 permanent-stone.

=>

The player cannot force a local-1 permanent-stone
AND
The player cannot force a local-2\1 permanent-stone


Proposition 4:

Given a final-position, a string in it, and the definitions of local-2\1, capturable-2\1, J2003-alive-2\1, WAGC-alive-in-seki-2\1, WAGC-alive-2\1.

The string is WAGC-alive-2\1 equals the string is J2003-alive-2\1.


Proposition 5:

The set of capturable-2\1 strings is a subset of the set of capturable-2 strings.

Top
 Profile  
 
Offline
 Post subject: Re: Research Summary
Post #3 Posted: Fri Jul 09, 2010 11:12 pm 
Lives in gote
User avatar

Posts: 581
Location: Shanghai, China
Liked others: 96
Was liked: 100
Rank: IGS 2 dan
Is there anyone out there who can offer an executive summary of this research summary?

Top
 Profile  
 
Offline
 Post subject: Re: Research Summary
Post #4 Posted: Fri Jul 09, 2010 11:30 pm 
Judan

Posts: 6087
Liked others: 0
Was liked: 786
Sure, but what exactly would you like to get? An informal translation summary of what the results mean in ordinary English and how they could be used?

Top
 Profile  
 
Offline
 Post subject: Re: Research Summary
Post #5 Posted: Sat Jul 10, 2010 2:36 am 
Judan

Posts: 6087
Liked others: 0
Was liked: 786
The following is not an executive summary yet but a preparation:


********************************************************************************************

Background knowledge:


Terms:
- force
- two-eye-formation
- permanent-stone
- uncapturable (cannot be captured)
- local-1
- capturable-1 (capturable of the type "Under the String")
- local-2
- capturable-2 (capturable of the type "Local to the String")

One must understand why the second capturable type is also necessary.

Links:
http://senseis.xmp.net/?ForceMathematics
http://senseis.xmp.net/?TwoEyeFormation
http://home.snafu.de/jasiek/sj.html
http://home.snafu.de/jasiek/wagcmod.html
http://home.snafu.de/jasiek/j2003.html
http://home.snafu.de/jasiek/j2003inf.html
http://home.snafu.de/jasiek/j2003com.html
http://home.snafu.de/jasiek/j1989c.html
http://home.snafu.de/jasiek/rules.html

Abbreviation:
Pn = see Proposition n

********************************************************************************************

New terms:


"local-2\1" is local-2 without local-1.

"capturable-2\1" is defined like capturable-2 but a permanent-stone occurs on local-2\1.

********************************************************************************************

There are two major descriptions of life of a string:


1) The string is either uncapturable, capturable-1 or capturable-2.

2) The string either can be transformed into a two-eye-formation or is defined as in (1).


In abbreviations, (1) is also called J2003-alive because this kind of life was first defined in the Japanese 2003 Rules. (2) is also called WAGC-alive because this kind of life follows the idea tried but not yet described correctly by the World Amateur Go Championship Rules.


There are two alternative, slightly different descriptions of life of a string:


1A) The string is either uncapturable, capturable-1 or capturable-2\1.

2A) The string either can be transformed into a two-eye-formation or is defined as in (1A).


********************************************************************************************

Important research results:


- The descriptions (1) and (2) define the same life! (P1)
- The descriptions (1A) and (2A) define the same life! (P4)
- A string can be transformed into a two-eye-formation regardless of which life description (1) or (2) is used. (P2)

********************************************************************************************

Research results for the sake of future research:


(P3) and (P5) are interesting mainly for future researchers. E.g., so far it is an open problem whether the descriptions of (1) and (1A) are the same. (P5) helps but answers only half of this problem.

********************************************************************************************

Top
 Profile  
 
Offline
 Post subject: Re: Research Summary
Post #6 Posted: Sat Jul 10, 2010 3:00 am 
Judan

Posts: 6087
Liked others: 0
Was liked: 786
Executive summary of the research itself (without explaining it specifically for Go players or its relevance for other or future research):


Earlier research gave two possible descriptions of life.

One of the descriptions classifies all alive strings as
a) uncapturable,
b) capturable so that a new then not removed stone is played under the original string,
c) capturable so that a new then not removed stone is played in the string's local environment.

The other of the two descriptions classifies all alive strings as
a) can be transformed into a two-eye-formation,
b) is not (a) but is uncapturable,
c) is not (a) but is capturable so that a new then not removed stone is played under the original string,
d) is not (a) but is capturable so that a new then not removed stone is played in the string's local environment.

The new research reveals:

- The two descriptions of life are equivalent!
- A string can be transformed into a two-eye-formation regardless of which of the two life descriptions is used.
- Further results help future researchers. One such result is: The description of local environment can be varied: The local environment either does or does not include the original string's intersections.

Top
 Profile  
 
Offline
 Post subject: Re: Research Summary
Post #7 Posted: Sun Jul 11, 2010 9:58 pm 
Lives in gote
User avatar

Posts: 581
Location: Shanghai, China
Liked others: 96
Was liked: 100
Rank: IGS 2 dan
Yes Robert, this is what I wanted to read. Thank you very much.

RobertJasiek wrote:
Executive summary of the research itself (without explaining it specifically for Go players or its relevance for other or future research):


Earlier research gave two possible descriptions of life.

One of the descriptions classifies all alive strings as
a) uncapturable,
b) capturable so that a new then not removed stone is played under the original string,
c) capturable so that a new then not removed stone is played in the string's local environment.

The other of the two descriptions classifies all alive strings as
a) can be transformed into a two-eye-formation,
b) is not (a) but is uncapturable,
c) is not (a) but is capturable so that a new then not removed stone is played under the original string,
d) is not (a) but is capturable so that a new then not removed stone is played in the string's local environment.

The new research reveals:

- The two descriptions of life are equivalent!
- A string can be transformed into a two-eye-formation regardless of which of the two life descriptions is used.
- Further results help future researchers. One such result is: The description of local environment can be varied: The local environment either does or does not include the original string's intersections.

Top
 Profile  
 
Display posts from previous:  Sort by  
Post new topic Reply to topic  [ 7 posts ] 

All times are UTC - 8 hours [ DST ]


Who is online

Users browsing this forum: No registered users and 1 guest


You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot post attachments in this forum

Search for:
Jump to:  
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group