- Need to define cellular automata, stack, queue, tape, PDA, Turing machines, etc.
- index N & S if diff below:
N::lexeme= "S"...
- Use a formally derived lexical analyzer to recognize terms and
link them to their definitions.
- Use a formally derived parser to distinguish formal from informal statements
- Implement the MATHS->diagram mapping algorithm to produce GIFs from formulae
- Link formulae to their GIFs
- (PM *35.354)|-For R:@(X,Y), A:@Y, S:@(Y,Z), (R; A); S = R; (A; S)
- Expand and correct intro*mth...pages. Link to other pages.
- Add Bernstein's lemma?
- create sample/logic_base and link to intro_logic and logic_*: university perhaps?? or Roman Relations?? Base on Leech's ontologies?
- Include a diagram of domain with sets/types/functions.
- Perhaps include Prolog and Java code?
- Expand notes on probability and give some examples -- penguins in urns?
Bayesian Busses.
- Check and revize notes on matching partitions.
- Add notes on reducing data sets: Given A:#Sets, R:@ (>< (A)), for a in A(f[a]:A(a)->B(a), find structure of R/f???
also image of data set under equivalences on attributes, or deleting certain attributes (rough sets).
- Check and revize notes on rough sets.
- Extract subsections, "nets", proofs on this web site into separate pages.
- Note use of "lexeme'' as a type.
- Formalize the relation between variables and expressions
Net
- Define variables as a map :expression->#(id, {free, bound }, type ( | , value))
- free::expression->@id,
- free::LPC.wff->@id,...
(End of Net)
- Strengthen GRAMMAR so that we can refer to newbib.section(N).paragraph(i).
State idea that unambiguous syntax determines default parsing and logical
structure. eg. if A:=#B then a part of type A has parts B(1), B(2), ...
B(|B|). If A:= B C B D then there four parts numbered 1,2,3,4 and also
parts called B(1), C(1), B(2), D(1). Hence part B=(B(1), B(2)).
- Can add explicit parsers as functions:
- parse(b1 c b2 d)::=(b1, c, b2, d)
- Strengthen formal DOM . In general, syntax determines DOM. Provide access to sections indexed by section header: document[header]. Do NOT index by number! Note:only if header not unique, number the occurences(how?).
- DOM: doc->%piece, piece=... | para. para->#sentence->#item->#word->#char.
- d.piece[3].item[2].word[1]
Net
- section = headline #paragraph
- section::= | [h:header] (headline(h) #paragraph(h) | openline(h) #paragraph(h) closeline(h) ),
- headline(h)::= ". " h eoln.
- M::syntax ->semantics, M(h ps)= h+> ><[p:ps]M(p).
(End of Net)
- Don't parse into a tree but into a data base!
- Define a 3NF data base for storing MATHS.
- Define a standard mapping into XML.
- Clumsy!!.
- Model checking??.
- proof checking.
- how to [sub] & ^(sup) in *formula only*.
- Inconsistent nets and undefinitions
- how to express in syntax that a string in the object language should be
used as an identifier for a part. For example bibliography uses headers to
label items and may want to refer (and change them by label).
- Defining extensions to the parsing of MATHS
But
This may introduce paradoxes -- review Frank Plumpton Ramsey! F(F)
(Close But )
- When to move to F/OSS, SourceForge or GitHub??
- Elementary nets = Net{v: T} & Combining nets. Use in data normalization
and design.
- add .[ and .] . How to escape in sed RegExs?
- Semantics of .{...} and .[ ... .]?
- Sell as a tool for: mathematics vs ADA, EMail, and RFCs.
- Distinguish: subtypes, extensions, & subsets
- Include YAML??
- Explore !? Notation for OO design.
- Should records be partial maps: (a=>1, b=>2) =~= ("a"+>1 | "b"+>2),
- Towards a UnifiedPC!
- LPC is generic for objects of a single type. But MATHS needs expressions that involve objects of many types. Therefore
Net
- extend LPC syntax to allow types.
- For all T x, P(x) (Q(x))
- For some T x, P(x) (Q(x)).
- Each T has an ontology. Sets @T. ==>,&,~, | . T is one of \coPi[i:I]S[i],
- or tuples ><[i:I]S[i], or T/eqrela'.
- Use Nets to define new Types.
- Model Typed/unified PC in LPC??
(End of Net)
- Universes of discourse do not overlap.
- Don't define a domain as a universe of discourse that is co-product.
?? (s.l !=n) ::= (s'=s~l|(l ! n)
- Perhaps need a loose match, find and replace:
- bib.id'=bib.id~{x:bib.id. "Duck" substring x}|"Dick Botting".
??for P:@S, (s.P'=n) ::= (s'=s~P|n)
- ?? newbib.id."Duck" .substring ' ="Dick Botting".
- Suppose set s is a partial map Id(0..)-(0..1)Data
and i:Id, and we want to change s(i) to value v:
- s.{ (i,d). for some d}' = (i,v).
- s.(i><Data)' = (i,v).
OR s[i]' = v.
- See
[ blog.html ]
Previous Changes
- Implement an algorithm to search relevant documentation for definitions
of terms that are not in the current document.
- ASCII to HTML converter
- UNIX script to do rough mapping from MATHS to HTML
- Added contents list and index for document
- Added Cross reference and citation handling
- Added Images
- added standard header
- included logo in header
- Recognizes axioms, theorems and definitions with partial cross linking
- Links theorems to their proofs
- add .{
. . . . . . . . . ( end of section MATHS To Do List) <<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.