[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ ] / math_74_Games
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sun Oct 2 14:36:33 PDT 2011

Games

1. GAME::=
Net{
N person game.
1. Players::Sets=given. Some Players.
2. No_of_players::=|Players|.
3. N::=No_of_players.
4. Position::Sets.
5. moves::Position->@Position.
6. moves::@Position->@Position=map[P:@Positions]{q:Position|| for some p:P, q in moves(p)}.
7. State::Sets. win, loose,draw,undecided::State.
8. value::Position->State.
9. Won::=win./value.
10. Lost::=loose./value.
11. Drawn::=draw./value.
12. For all p:Position ( p in Won|Lost|Draw iff moves(p)={}).

Winning, Loosing::@Position.

13. Won==>Winning. Lost==>Loosing.
14. No Winning & Loosing.
15. Initial::@Position.
16. loops::@= some p:positions( p in moves;do(moves) ).

}=::GAME.

2. SOLITAIRE::={ A game with one player were there may be a chance of winning and one initial state
3. GAME and No_of_players=1.
4. For all p:Loosing, p.moves==>Loosing.
5. Draw={}.
6. possible::@= Initial==>Winning and for all p:Winning, some p.moves & Winning.
7. Rubik's cube is a patience game with loops. Solitare card games have no loops.
8. Rubik's cube has no Loosing positions, a single Won position, and a finite but large set of Winning positions.
9. Call such a game a maze:
10. maze::@= Winning=finite Position and |Won|=1.

}=::SOLITAIRE.

1. 2_PERSON_GAME::=
Net{

1. |-GAME and No_of_players=2. black,white::Players.
2. Winning::=
3. { p:Position
4. || p in Won
5. or p.moves==>Lost
6. or for all q:p.moves, some r:q.moves (r in Winning)
7. }.
8. Loosing::= { p:Position || p in Lost or some p.moves & Winning or for some q:p.moves, all r:q.moves (r in Loosing) }.
9. play_alternately::@= For some State:Sets ( Position = Players >< State )
10. and for all p:Position, q:moves(p) ( p.1st<>q.1st ).

}=::2_PERSON_GAME.

2. BOARD_GAME::=
Net{

1. |-GAME.
2. Board::Sets.
3. Type_of_piece::Sets.
4. |-Position=Board->{empty}|Piece.
5. |-Piece=Players><Type_of_piece.

6. For Piece p, Board b,
8. Take(p,b)::=map[x:Position]{x'||x(b)=p and x'(b)=empty},
9. Move(p,b1,b2)::=map[x:Position]
10. {x'||x(b1)=p and x(b2)=empty and x'(b1)=empty and x'(b2)=p}.

}=::BOARD_GAME.

3. tictactoe::=\$
Net{

1. |-BOARDGAME(Position=>Grid).
2. |-2_PERSON_GAME(play_alternately).
3. |-Type_of_piece={mark}.
4. nought::Piece=(black,mark),
5. cross::Piece=(white, mark).

6. |-Board=1..3><1..3.
7. Rows::={ {(r,c):Board||r:1..3}||c:1..3 },
8. Cols::={ {(r,c):Board||c:1..3}||r:1..3 },
9. Diagonals::={ {(1,1),(2,2),(3,3)} , {(1,3),(2,2),(3,1)} }.

10. |-Position=Player><Grid.

11. Won::={p:Position
12. || for some X:Rows|Cols|Diagonals, q:{nought,cross}, all b:X ( Position(b)=q )
13. }.
14. (above)|-Won={p:Position
15. || for some X:Rows|Cols|Diagonals, q:{nought,cross}( X==>q./Position)
16. }.

}=::tictactoe.

. . . . . . . . . ( end of section Games) <<Contents | End>>

Notes on MATHS Notation

Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

For a more rigorous description of the standard notations see

• STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

Glossary

• above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
• given::reason="I've been told that...", used to describe a problem.
• given::variable="I'll be given a value or object like this...", used to describe a problem.
• goal::theorem="The result I'm trying to prove right now".
• goal::variable="The value or object I'm trying to find or construct".
• let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
• hyp::reason="I assumed this in my last Let/Case/Po/...".
• QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
• QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
• RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.