Recent Changes and thoughts about the MATHS Language

For In:Net, Net_to_Z(In)::=with{signature, axioms:Sets} following (
1. (signature, axioms) := ({},{});
2. do (
  1. with{piece:piece_of_documentations} (
    1. piece:?In; (
      1. piece in declaration; signature:|declaration_to_Z(piece)
      2. | piece in wff; axioms:|wff_to_Z(piece)
      3. | piece in definition; signature:|definition_to_Z_declaration(piece); axioms:|definition_to_Z_equality(piece)
      4. | piece in (theorem | comment)
      )
    )
  );
3. end(In);
4. output_Z_schema(signature, axioms);
).
```
  For In:Net, Net_to_Z(In) ::=with{signature, axioms:Sets} following
```
```
 .(
```
```
 	(signature, axioms) := ({},{});
```
```
 	do
```
```
 .(with{piece:piece_of_documentations}
```
```
 .(
```
```
 		piece:?In;
```
```
 .( piece in declaration;  signature:|declaration_to_Z(piece)
```
```
 		|  piece in wff;  axioms:|wff_to_Z(piece)
```
```
 		|  piece in definition;  signature:|definition_to_Z_declaration(piece); axioms:|definition_to_Z_equality(piece)
```
```
 		|  piece in (theorem | comment)
```
```
 .)
```
```
 .)
```
```
 .);
```
```
 	end(In);
```
```
 	output_Z_schema(signature, axioms);
```
```
 .).
```
This idea now goes into a trial use period. Comments would help. I'll either retract the idea or put it into the online m2h tool in a week or two. Watch this blog for the next exciting episode!

2008-11-03 Mon Nov 3 13:11 Worrying about algorithms and expressions
I am disatisfied with the expression of algorithms in MATHS. There is a formal semantics in terms of an extension to the calculus of relations. This makes algorithms a special kind of formula. But to make them readable -- structured even -- is another matter -- basically you need to use the .List and .Set directives to show the block structure. An example is [ notn_14_Docn_Semantics.html#Translation into a Z Schema ] from the description of the meaning of a piece of MATHS documentation.
This morning it occured to me that a natural notation would be to allow directives like: ".(", ".)" and perhaps even ".[", ".{", etc. The sematics is of "(...)". But the rendering should be as an indented subexpression. More on this when I've had a chance to do some more thinking. Any opinions can be sent to me here [ hole.html ] and will get full credit.

2008-11-01 Sat Nov 1 06:11 Working on Types and Duck Typing
Several modern programming languages -- Python and Ruby, for example -- use what is called "Duck Typing". This means that behavior of an object defines its type, rather than an explicit definition.
It turns out, to my surprise, that my MATHS language has a kind of Duck Typing because the type of an object is the universal set in which the object is defined. And the type defined by a Net of variables, axioms, definitions, etc. is the type of the unconstrained objects -- the simple Net associated with the original Net...
Details and changes in [ notn_14_Docn_Semantics.html ] and [ notn_16_Classification.html ]
As always -- click here [click here if you can fill this hole] to submit your thoughts.
2008-10-24 Fri Oct 24 10:10 Small revisions to the A->B notation
Not a real change of meaning.... just cleaned up the definitions and noted that
A->B->C
is not clearly defined and should be avoided.
2008-10-22 Wed Oct 22 16:10 improved notes on the Calculus
Still a long way to go in [ math_94_Calculus.html ] before we have a complete page.
2008-10-07 Tue Oct 7 07:10 Corrected syntax of example database definition
[ math_13_Data_Bases.html#DataBase ]
Which in turn lead to an extension of the notation for discriminated types [ types.html#type_disciminated_union ]
2008-09-29 Mon Sep 29 14:09 Corrected a subtle error in Petri net definition
I had to shuffle the definitions of Node, Places, and Transitions in [ math_76_Concurency.html#PETRI ] so that it is clear that Places and Transitions are the same type of thing and so validating the definition
Arcs::@(Places><Transitions) | @(Transitions><Places)=given.

2008-09-25 Thu Sep 25 10:09 Citation in theory and practice
The bibliography [ ../lab.html ] has evolved a notation for citations that was not a part of my original design for MATHS. Similarly the "hole.php" uses the Source directive in an unexpected way. See [ notn_15_Naming_Documentn.html ] for the kludge. The older BNF syntax may be removed or be replaced in time -- it is now deprecated.
2008-09-10 Wed Sep 10 11:09 Quotes about math and life
The following quotes were sent to me by Sonesh Rawat via the Contact/comment button on this part of my website:
1. He who seeks for methods without having a definite problem in mind seeks for the most part in vain.
2. One should study mathematics because it is only through mathematics that nature can be conceived in harmonious form.
3. Just as a mountaineer climbs a mountain- because it is there,so a good mathematics students studies new material because it is there.
I'd like to cap them with a thought of Sigmund Freud:
Man climbs highest when he doesn't know where he is going.
By the way just fixed the broken link on Systems English below.

2008-09-09 Tue Sep 9 17:09 Added notes on Grammars
[ math_63_Languages.html ]
2008-08-26 Tue Aug 26 13:08 Improved description of Systems English
Systems English is a tiny subset of Basic English designed to describe systems: [ logic_8_Natural_Language.html#Systems English ]
2008-08-11 Mon Aug 11 16:08 What -- no topoi
Somehow I've never gathered any notes of topos theory and topoi. I'm just moting the following link to a simple motivational introduction:
topos::= See http://math.ucr.edu/home/baez/topos.html at the nearby University of California Riverside.
When developed the notes would be in [ math_25_Categories.html ] and I will plant a hole there for future expansion.

2008-08-10 Sun Aug 10 12:08 Corrected error in definition of subspace
[ math 91 Topology.html#Subspaces and relative topologies ]
2008-06-27 Fri Jun 27 08:06 An Expression with Ambiguous type
As a result of thinking about a wikipedia article I tripped over the fact that
/Card(n) -- the sets with cardinallity n, is a typically ambiguous expression. As a result runs the risk of introducing a paradox into the system if not used carefully. So I'm changing the definition from
Card:@T->Nat0= map[X](|X|)
to
For Type T, Card[T]::@T->Nat0= map[X:@T](|X|).
For Type T, X:@T, Card(X)::Nat0= Card[T](X).
For Type T, A:@T, n:Nat0, A@n = { X:@T || Card[T](X) = n }. (Subsets of a given size).
Here are the pages where changes were made as a result [ types.html ] [ math_25_Categories.html ] [ logic_30_Sets.html ] [ intro_sets.html ] [ intro_standard.html ] [ notn_12_Expressions.html ]
I wonder if I need a way to express the idea that some expression is not defined in addition to having a way to define things? [click here undefinitions if you can fill this hole]

2008-06-20 Fri Jun 20 14:06 Rebuttals in MATHS
But me no Buts!
I've decided to introduce a simple way to annotate an argument that attempts to rebut the previous argument. Commonly arguments and proofs in MATHS start ".Let" and end ".Close.Let". A Rebuttal will be an argument that is placed between
```
 .But
```
and
```
 .Close.But
```
For example
Let
1. (let)|-It is raining.
2. (let)|-If it rains then I shall get wet.
3. (-1, -2)|-I shall get wet.
(Close Let )

But
1. I carry an umbrella.
2. (-1)|-I keep dry.
  But
  1. In August,
  2. I forgot the umbrella,
  3. (-1)|-I got wet.
  (Close But )
(Close But )

2008-06-19 Thu Jun 19 07:06 Working on Toulmin Arguments and Rationales
Today I'll be working on [ notn_5_Form.html ] to describe informal argumentation.
This is the result of seeing the same reference in two papers in IEEE Transactions on Software Engineering and in "Wittgenstein's Poker".
More later...
2008-06-14 Sat Jun 14 10:06 Added source and some distributions
[ math_81_Probabillity.html ] (sorry for the mis-spelling in this link).
2008-06-12 Thu Jun 12 05:06 Clarified definitions of prefic union and intersection in Sets
This span off from Principia Mathematica Section *42 (and there is more below).
I added the definition of prefix union and intersection to [ logic_30_Sets.html ] and explicitly linked [ logic_31_Families_of_Sets.html ] back to logic_30.
8:35 Added the (missing) syntax for prefixed union and intersection operators. Also added some quick examples of the syntax.
5:13 pm Added a nonstandard translation of part of PM's Chapter 42: [ logic_30_Sets.html#Chapter_42 ] (enter here at your own risk).

2008-06-11 Wed Jun 11 15:06 Fixed diagram of constructive dilemma
[ constructive_dilemma in logic_25_Proofs ]

2008-06-11 Wed Jun 11 05:06 Stuggling with an ambiguity
Until last night I've never worried about sets of sets of sets. But they are used in Principia Mathematica's section *42 -- definitely not the answer to life's persistent questions.
This lead me to discover an ambiguity in expressions like
+((1,2), (3,4)).
Plus is a SERIAL operator so it means
(1,2) + (3,4).
And + is overloaded to combine maps and lists so that its value is
(1+3, 2+4) = (4,6).
It might be thought that because + is overloaded as a prefix function it should be applied (by a second overloading) to the elements of the list
+((1,2), (3,4)) <> ( +(1,2), +(3,4)) = (3, 7).
I've added notes to [ notn_12_Expressions.html ] that explain that the simplest parsings are used whenever possible.

2008-06-07 Sat Jun 7 07:06 Tidied up overloading of infix operators
Read chapter 38 of Principia Mathematica last night. Made me want to review the equivalent definitions in MATHS. As a result I've tidied up [ math_11_STANDARD.html#Infix operations ] which make the following equations correct:
{1,2,3} * 3 = {3,6,9},
{1,2}*{3,5} = {3,5,6,20},
4*(1,2,3) = {4,8,20),
(3,4,5)*(1,2,3) = (3,8,15).

2008-06-05 Thu Jun 5 07:06 Improved notes on Proofs
I've expanded on the reasons for proving something [ logic_20_Proofs100.html#But Why Prove anything Anyway? ] and what can be concluded after deriving some results from some assumptions in [ logic_25_Proofs.html#Block Structure ] to clarify that you must include all the assumptions and any of the results in the conclusion drawn from an argument.

11:06 Added a note on tables and relational data bases. [ notn_9_Tables.html ]

2008-05-23 Fri May 23 16:05 Initiating a web log of changes and thoughts

I'm planning to record most changes to the files in this directory here.

Here is a quick list of recently changed pages in this part of my site.
Table
Date Page Action
May 5 10:29 math_92_Metric_Spaces.html Added Notes on Hilbert spaces used in Quantum Theory
May 7 17:58 math_81_Probabillity.html Added notes on Expected values, means, variances etc.
May 10 09:02 logic_27_Tableaux.html Added a thought about using a table to express a set of cases
May 13 07:23 intro_records.html Added notes on optional and multiple parts in a record
May 19 14:32 logic_30_Sets.html Added to notes on the Axiom of Choice
May 21 20:10 logic_25_Proofs.html Added an example of using table to document proof by cases.
May 23 06:49 math_41_Two_Operators.html Added definition of a dioid

(Close Table)

Date	Page	Action
May 5 10:29	math_92_Metric_Spaces.html	Added Notes on Hilbert spaces used in Quantum Theory
May 7 17:58	math_81_Probabillity.html	Added notes on Expected values, means, variances etc.
May 10 09:02	logic_27_Tableaux.html	Added a thought about using a table to express a set of cases
May 13 07:23	intro_records.html	Added notes on optional and multiple parts in a record
May 19 14:32	logic_30_Sets.html	Added to notes on the Axiom of Choice
May 21 20:10	logic_25_Proofs.html	Added an example of using table to document proof by cases.
May 23 06:49	math_41_Two_Operators.html	Added definition of a dioid

2008

Latest -- [ math_92_Metric_Spaces.html ] [ math_5_Object_Theory.html ] [ logic_10_PC_LPC.html ] [ intro_records.html ] (optional and multiple parts) [ intro_objects.html ] [ intro_copywrite.html ] [ notn_14_Docn_Semantics.html ] [ notn_13_Docn_Syntax.html ] [ logic_25_Proofs.html ] [ intro_function.html ] [ math_95_Function_Spaces.html ] [ math_45_Three_Operators.html ] (Trying to understand Quantum Theory....) -- Oldest

Changes in 2007

Latest -- [ logic_10_PC_LPC.html ] (linking MATHS to Term Logic and Aristotlean Logic) [ math_21_Order.html ] [ logic_20_Proofs100.html ] [ math_81_Probabillity.html ] (Bayesian Probability matches abductive reasoning), [ intro_objects.html ] (exploring adding OO dynamics to Nets), [ logic_30_Sets.html ] [ logic_2_Proofs.html ] [ intro_ebnf.html ] [ math_21_Order.html ] [ logic_20_Proofs100.html ] -- Oldest

Changes in 2006

Latest -- [ notn_13_Docn_Syntax.html ] [ intro_characters.html ] [ math.lexicon.html ] [ math.syntax.html ] (changing notation to separate formula from bullet points/paragraphs), [ logic_27_Tableaux.html ] (Semantic tableax), [ logic_2_Proofs.html ] is now refactored into [ logic_20_Proofs100.html ] and [ logic_25_Proofs.html ] -- Oldest

Changes in 2005

[ logic_2_Proofs.html ] (added more on semantic tableaux)

Changes in 2004

(2004): Latest -- [ logic_30_Sets.html ] [ logic_8_Natural_Language.html ] [ notn_14_Docn_Semantics.html ] [ notn_12_Expressions.html ] [ notn_16_Classification.html ] [ notn_13_Docn_Syntax.html ] [ notn_3_Conveniences.html ] [ notn_2_Structure.html ] [ notn_11_Names.html ] [ math_77_Enumerations.html ] [ math_25_Categories.html ] -- Oldest

Changes in 2003

(2003): -- Latest [ intro_standard.html ] [ math_73_Process_algebra.html ] [ math_82_MultiSets_and_Bags.html ] [ math_83_Fuzzy_Sets.html ] [ 00_overview.html ] [ math_84_Spectra.html ] [ notn_9_Tables.html ] [ logic_9_Modalities.html ] [ logic_41_HomogenRelations.html ] -- Oldest

Definitions

MATHS::=./index.html

. . . . . . . . . ( end of section Recent Changes and thoughts about the MATHS Language) <<Contents | End>>

Notes on MATHS Notation

intro_characters.html

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

logic_0_Intro.html

For a more rigorous description of the standard notations see

STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
Glossary
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.

Contents

Recent Changes and thoughts about the MATHS Language

2009-11-18 Wed Nov 18 16:03 Changed a symbol for the temporal if-then

2009-11-09 Mon Nov 9 14:56 Started a definition of protocols and messages

2009-06-11 Thu Jun 11 15:55 Improved proposed notation for problem solving

2009-05-19 Tue May 19 06:33 Improved notes on Dynamics

2009-01-31 Sat Jan 31 09:01 Thank you Alejandro

2008-11-12 Wed Nov 12 14:11 Dimensioned Numbers

2008-10-07 Tue Oct 7 07:10 Corrected syntax of example database definition

2008-09-10 Wed Sep 10 11:09 Quotes about math and life

2008-08-26 Tue Aug 26 13:08 Improved description of Systems English

2008-08-11 Mon Aug 11 16:08 What -- no topoi

2008-06-27 Fri Jun 27 08:06 An Expression with Ambiguous type

2008-06-12 Thu Jun 12 05:06 Clarified definitions of prefic union and intersection in Sets

Changes in 2007

Changes in 2006

Changes in 2005

Changes in 2003

Glossary

End