[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci Dept] / [R J Botting] / [ MATHS ] / math_74_Games
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Sep 18 15:18:42 PDT 2007

Contents

    Games

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

        Winning, Loosing::@Position.

      12. Won==>Winning. Lost==>Loosing.
      13. No Winning & Loosing.
      14. Initial::@Position.
      15. 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=Position is Finite 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,
    7. Add(p,b)::=map[x:Position]{x'||x(b)=empty and x'(b)=p},
    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), cross::Piece=(white, mark).


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


    9. |-Position=Player><Grid.

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

      [click here [socket symbol] if you can fill this hole]


    }=::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 = Net{radius:Positive Real, center:Point}.

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.

    End