- POSITION::=Net{ x,y:Nat0 },
- 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.
- 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}.
- For p,q: pixels, p next_to q::@=q in neighbours(p).
- (above)|- (g0): next_to in Reflexive(pixels) & Symmetric(pixels)~transitive(pixels).
Reflexive and Symmetric follow by substitution of definitions and rearrangement.
Lack of transitivity comes form considering pixels (0,1),(0,2),(0,3).
- For S:@pixels,
- outside(S)::@pixels=pixels~S,
- close(S)::@pixels= |neighbours(S),
- inside(S)::@pixels= outside(close(outside(S))),
- edge(S)::@pixels=close(S)~inside(S).
- colors::={white, black, ...}.
- pictures::=pixels->colors
For o:{+,-, div, mod, *, /}, o::infix(pixels) = (x=>(1st).x o (2nd).x, y=>(1st).y o (2nd).y).
- (above)|- (g1): For a,b:pixels, o:{+,-, div, mod, *, /}, a o b = (x=>a.x o b.x, y=>a.y o b.y).
- For a:pixels, n:Real, n * a::pixels= (x=> round(n * a.x), y=> round(n * a.y) ).
- (above)|- (g2): MODULE(M=>pixels, Ring=>Reals).
- WIDTH_DEPTH::=Net{ w, d:Numbers&positive, width:=w, depth:=d. wd:=(x=>w,y=>d)}.
- PATTERN::=
Net{
WIDTH_DEPTH.
- basis::$ POSITION and {0<=x<=w, 0<=y<=d} ->colors.
- cycle::=(x=>w+1, y=>d+1).
- color::points->colors=map[p:points](basis(p mod cycle))
}=::
PATTERN.
- pattern::={none} \/ $ PATTERN.
- RECTANGLE::=
Net{
WIDTH_DEPTH.
tl, tr, br, bl, c::pixels,
- top_left::=tl,
- top_right::=tr,
- bottom_right::=br,
- bottom_left::=tr,
- center::=c.
- centre::=center.
- br=tl+wd.
- c = tl + 0.5*wd.
l:=left::=tl.x, l=bl.x,
r:=right::=tr.x, r=br.x,
- t:=top:=tl.y, t=tr.y,
b:=bottom::=bl.y, b=br.y.
- coverage::={p:pixels || tl.x<=p.x<=tr.x and tl.y<=p.y<=br.y}
}=::
RECTANGLE.
- GRAPHIC::=
Net{
- coverage::@pixels, - part filled with pattern
- contacts::@coverage, - pixels where it can touch another graphic.
- shape::Sets,
fill, pen::pattern,
- type::{line,box,...}.
- (gt1): type=line iff LINE.
- (gt2): type = box iff BOX.
[click here if you can fill this hole]
}=::
GRAPHIC.
- graphics::@$ GRAPHIC.
- THIN::=Net{ GRAPHIC. inside={}}.
- LINE::=
Net{
start, end::pixels.
- |- (gl0): GRAPHIC and Net{type=line}.
- |- (gl1): contacts={start, end}.
- |- (gl2): for all p,q in coverage. p do(next_to) q.
- |- (gl3): shape={horizontal, vertical, straight, curved,...}.
- |- (gl4): pen=fill.
- arrow_heads::@{start,finish,middle}><{open,closed}><{hollow, thin, thick,...}.
}=::
LINE.
- BOX::=
Net{
RECTANGLE. Assume that there are no holes or projections.
- Boxes are supposed to cover a rectangular area.
- |- (gb0): GRAPHIC and Net{type=box}.
- |- (gb1): contacts=edge(coverage).
- |- (gb2): shape={rectangle, text, char, blob}.
}=::
BOX.
- touches::Reflexive(graphics).
- |- (g4): PART_WHOLE(graphics, is_part_of).
- |- (g5): for all g1,g2:graphics, if g1 touches g2 then not g1 is_part_of g2.
- |- (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)).
- |- (g8): for all g1,g2:graphics, if not g1 (is_part_of | /is_part_of) g2 then not g1 overlaps g2 ).
- |- (g9): for all g1,g2:graphics, if g1 touches g2 then some close contacts(g1) & close contacts(g2).
- above::@(qraphics,graphics)=rel[a,b](b.l<=a.l and a.r<=b.r and a.c.y>b.c.y),
- below::@(qraphics,graphics)= /above.
- left::@(graphics,graphics)=rel[a,b](a.t<=b.t and a.b>=b.b and a.c.x<b.c.x),
- right::@(qraphics,graphics)= /left.
[ logic_8_Natural_Language.html ]
. . . . . . . . . ( end of section Simple Graphics) <<Contents | End>>
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 ]
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
- 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.