Any help will be appreciated... [click here if you can fill this hole]

To Be Done to mth2html and m2h

1. index N & S if diff below:

    N::lexeme= "S"...

2. Use a formally derived lexical analyzer to recognize terms and link them to their definitions.
3. Use a formally derived parser to distinguish formal from informal statements
4. Implement the MATHS->diagram mapping algorithm to produce GIFs from formulae
5. Link formulae to their GIFs

To Be Done to Content



1. (PM *35.354)|-For R:@(X,Y), A:@Y, S:@(Y,Z), (R; A); S = R; (A; S)
2. Expand and correct intro*mth...pages. Link to other pages.
3. Add Bernstein's lemma?
4. create sample/logic_base and link to intro_logic and logic_*: university perhaps?? or Roman Relations?? Base on Leech's ontologies?
5. Include a diagram of domain with sets/types/functions.
6. Perhaps include Prolog and Java code?
7. Expand notes on probability and give some examples -- penguins in urns? Bayesian Busses.
8. Check and revize notes on matching partitions.
9. 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).
10. Check and revize notes on rough sets.
11. Extract subsections, "nets", proofs on this web site into separate pages.

To be done to the submission system

1. When POSTed nothing, hole.php should output hole.html OR nothing but a form or a topic ??
2. Create specialized versions for cs375 and samples.

To Be Done to Definition of MATHS

1. Note use of "lexeme'' as a type.
2. Formalize the relation between variables and expressions
   Net
   1. Define variables as a map :expression->#(id, {free, bound }, type ( | , value))
   2. free::expression->@id,
   3. free::LPC.wff->@id,...

   
   (End of Net)
   
   
3. 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:

4. parse(b1 c b2 d)::=(b1, c, b2, d)
5. 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?).
6. DOM: doc->%piece, piece=... | para. para->#sentence->#item->#word->#char.
7. d.piece[3].item[2].word[1]
   Net
   1. section = headline #paragraph
   2. section::= | [h:header] (headline(h) #paragraph(h) | openline(h) #paragraph(h) closeline(h) ),
   3. headline(h)::= ". " h eoln.
   4. M::syntax ->semantics, M(h ps)= h+> ><[p:ps]M(p).

   
   (End of Net)
   
   
8. Don't parse into a tree but into a data base!
9. Define a 3NF data base for storing MATHS.
10. Define a standard mapping into XML.

Problems

1. Clumsy!!.
2. Model checking??.
3. proof checking.
4. how to [sub] & ^(sup) in *formula only*.
5. Inconsistent nets and undefinitions

   The metalinguistic barrier

   1. 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).
   2. Defining extensions to the parsing of MATHS
      But
      This may introduce paradoxes -- review Frank Plumpton Ramsey! F(F)
      
      (Close But )
      
6. When can m2h send to mailing list?
7. When to move to F/OSS, SourceForge??

Partly Baked Ideas

1. Elementary nets = Net{v: T} & Combining nets. Use in data normalization and design.
   add .[ and .] . How to escape in sed RegExs?
2. Semantics of .{...} and .[ ... .]?
3. Sell as a tool for: mathematics vs ADA, EMail, and RFCs.
4. Distinguish: subtypes, extensions, & subsets
5. Include YAML??
6. Explore !? Notation for OO design.
7. Should records be partial maps: (a=>1, b=>2) =~= ("a"+>1 | "b"+>2),
8. Towards a UnifiedPC!
9. LPC is generic for objects of a single type. But MATHS needs expressions that involve objects of many types. Therefore
   Net
   1. extend LPC syntax to allow types.
   2. For all T x, P(x) (Q(x))
   3. For some T x, P(x) (Q(x)).
   4. Each T has an ontology. Sets @T. ==>,&,~, | . T is one of \coPi[i:I]S[i],
   5. or tuples ><[i:I]S[i], or T/eqrela'.
   6. Use Nets to define new Types.
   7. Model Typed/unified PC in LPC??

   
   (End of Net)
   
   
10. Universes of discourse do not overlap.
    Don't define a domain as a universe of discourse that is co-product.

    Add to set

    ?? (s.l !=n) ::= (s'=s~l|(l ! n)
    1. Perhaps need a loose match, find and replace:
    2. bib.id'=bib.id~{x:bib.id. "Duck" substring x}|"Dick Botting". ??for P:@S, (s.P'=n) ::= (s'=s~P|n)
    3. ?? newbib.id."Duck" .substring ' ="Dick Botting".
    4. 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:
    5. s.{ (i,d). for some d}' = (i,v).
    6. s.(i><Data)' = (i,v). OR s[i]' = v.

Done

1. See [ blog.html ]

   Previous Changes

2. Implement an algorithm to search relevant documentation for definitions of terms that are not in the current document.
3. Repair the "mailme.html" form
4. ASCII to HTML converter
5. UNIX script to do rough mapping from MATHS to HTML
6. Added contents list and index for document
7. Added Cross reference and citation handling
8. Added Images
9. added standard header
10. included logo in header
11. Added a link to "mailme.html" form in standard header
12. Recognizes axioms, theorems and definitions with partial cross linking
13. Links theorems to their proofs
14. add .{

. . . . . . . . . ( end of section MATHS To Do List) <<Contents | End>>

Notes on MATHS Notation

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

For a more rigorous description of the standard notations see