[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ ] / 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::=
Net{
WIDTH_DEPTH.

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))

}=::PATTERN.

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

19. RECTANGLE::=
Net{
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}

}=::RECTANGLE.

20. GRAPHIC::=
Net{
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 if you can fill this hole]

}=::GRAPHIC.

21. graphics::@\$ GRAPHIC.

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

23. LINE::=
Net{
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,...}.

}=::LINE.

24. BOX::=
Net{
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}.

}=::BOX.

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.

. . . . . . . . . ( 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

# Glossary

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.