[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ ] / todo
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Fri Aug 30 08:54:02 PDT 2013

# MATHS To Do List

1. Need to define cellular automata, stack, queue, tape, PDA, Turing machines, etc.

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

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

(End of Net)

9. Don't parse into a tree but into a data base!
10. Define a 3NF data base for storing MATHS.
11. 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 to move to F/OSS, SourceForge or GitHub??

## Partly Baked Ideas

1. Elementary nets = Net{v: T} & Combining nets. Use in data normalization and design.
2. add .[ and .] . How to escape in sed RegExs?
3. Semantics of .{...} and .[ ... .]?
4. Sell as a tool for: mathematics vs ADA, EMail, and RFCs.
5. Distinguish: subtypes, extensions, & subsets
6. Include YAML??
7. Explore !? Notation for OO design.
8. Should records be partial maps: (a=>1, b=>2) =~= ("a"+>1 | "b"+>2),
9. Towards a UnifiedPC!
10. 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)

11. Universes of discourse do not overlap.
12. Don't define a domain as a universe of discourse that is co-product.

?? (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. ASCII to HTML converter
4. UNIX script to do rough mapping from MATHS to HTML
5. Added contents list and index for document
6. Added Cross reference and citation handling
10. Recognizes axioms, theorems and definitions with partial cross linking
11. Links theorems to their proofs

. . . . . . . . . ( end of section MATHS To Do List) <<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.