[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_93_Graphics
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Dec 13 14:24:14 PST 2010


    Simple Graphics

    1. POSITION::=Net{ x,y:Nat0 },
    2. pixels::=$ POSITION. To make this treatment simpler, assume that we can work with a logical window that is unlimitted and delay tackling problems of graphics leaving the physical screen or display. There exist well techniques for doing this any way.

    3. For p: pixels, neighbours(p)::@pixels={n:pixels || p.x-1<=n.x<=p.x+1 and p.y-1<=n.y<=p.y+1}.

    4. For p,q: pixels, p next_to q::@=q in neighbours(p).
    5. (above)|- (g0): next_to in Reflexive(pixels) & Symmetric(pixels)~transitive(pixels).

      Proof of g0

      Reflexive and Symmetric follow by substitution of definitions and rearrangement. Lack of transitivity comes form considering pixels (0,1),(0,2),(0,3).

    6. For S:@pixels,
    7. outside(S)::@pixels=pixels~S,
    8. close(S)::@pixels= |neighbours(S),
    9. inside(S)::@pixels= outside(close(outside(S))),
    10. edge(S)::@pixels=close(S)~inside(S).

    11. colors::={white, black, ...}.

    12. pictures::=pixels->colors

      For o:{+,-, div, mod, *, /}, o::infix(pixels) = (x=>(1st).x o (2nd).x, y=>(1st).y o (2nd).y).

    13. (above)|- (g1): For a,b:pixels, o:{+,-, div, mod, *, /}, a o b = (x=>a.x o b.x, y=>a.y o b.y).
    14. For a:pixels, n:Real, n * a::pixels= (x=> round(n * a.x), y=> round(n * a.y) ).

    15. (above)|- (g2): MODULE(M=>pixels, Ring=>Reals).

    16. WIDTH_DEPTH::=Net{ w, d:Numbers&positive, width:=w, depth:=d. wd:=(x=>w,y=>d)}.

    17. PATTERN::=

      1. basis::$ POSITION and {0<=x<=w, 0<=y<=d} ->colors.
      2. cycle::=(x=>w+1, y=>d+1).

      3. color::points->colors=map[p:points](basis(p mod cycle))


    18. pattern::={none} \/ $ PATTERN.

    19. RECTANGLE::=
        WIDTH_DEPTH. tl, tr, br, bl, c::pixels,
      1. top_left::=tl,
      2. top_right::=tr,
      3. bottom_right::=br,
      4. bottom_left::=tr,
      5. center::=c.
      6. centre::=center.

      7. br=tl+wd.
      8. c = tl + 0.5*wd. l:=left::=tl.x, l=bl.x, r:=right::=tr.x, r=br.x,
      9. t:=top:=tl.y, t=tr.y, b:=bottom::=bl.y, b=br.y.

      10. coverage::={p:pixels || tl.x<=p.x<=tr.x and tl.y<=p.y<=br.y}


    20. GRAPHIC::=
      1. coverage::@pixels, - part filled with pattern
      2. contacts::@coverage, - pixels where it can touch another graphic.
      3. shape::Sets, fill, pen::pattern,
      4. type::{line,box,...}.
      5. (gt1): type=line iff LINE.
      6. (gt2): type = box iff BOX.

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


    21. graphics::@$ GRAPHIC.

    22. THIN::=Net{ GRAPHIC. inside={}}.

    23. LINE::=
        start, end::pixels.
      1. |- (gl0): GRAPHIC and Net{type=line}.
      2. |- (gl1): contacts={start, end}.
      3. |- (gl2): for all p,q in coverage. p do(next_to) q.
      4. |- (gl3): shape={horizontal, vertical, straight, curved,...}.
      5. |- (gl4): pen=fill.
      6. arrow_heads::@{start,finish,middle}><{open,closed}><{hollow, thin, thick,...}.


    24. BOX::=
        RECTANGLE. Assume that there are no holes or projections.
      1. Boxes are supposed to cover a rectangular area.
      2. |- (gb0): GRAPHIC and Net{type=box}.

      3. |- (gb1): contacts=edge(coverage).
      4. |- (gb2): shape={rectangle, text, char, blob}.


    25. touches::Reflexive(graphics).

    26. |- (g4): PART_WHOLE(graphics, is_part_of).

    27. |- (g5): for all g1,g2:graphics, if g1 touches g2 then not g1 is_part_of g2.
    28. |- (g6): for all g1,g2:graphics, if g1 is_part_of g2 then coverage(g1)==>coverage(g2)).

      |-(g7): for all g1,g2:graphics, g1 overlaps g2::@ =some coverage(g1)& coverage(g2)).

    29. |- (g8): for all g1,g2:graphics, if not g1 (is_part_of | /is_part_of) g2 then not g1 overlaps g2 ).

    30. |- (g9): for all g1,g2:graphics, if g1 touches g2 then some close contacts(g1) & close contacts(g2).

    31. above::@(qraphics,graphics)=rel[a,b](b.l<=a.l and a.r<=b.r and a.c.y>b.c.y),
    32. below::@(qraphics,graphics)= /above.
    33. left::@(graphics,graphics)=rel[a,b](a.t<=b.t and a.b>=b.b and a.c.x<b.c.x),
    34. right::@(qraphics,graphics)= /left.

      [ logic_8_Natural_Language.html ]

    . . . . . . . . . ( end of section Simple Graphics) <<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

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


  2. 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).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. 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.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.