.Open Recent Changes and thoughts about the MATHS Language . 2009-11-18 Wed Nov 18 16:03 Changed a symbol for the temporal if-then Becuase "~>" was overloaded ofr relations and temporal logic, and this might be confusing.... I've chosen to change "~>" to "~~>" in .See ./logic_9_Modalities.html#SIMPLE_TEMPORAL_LOGIC and I hope this doesn't cause any problems.... Let me know if it does. . 2009-11-16 Mon Nov 16 14:39 Late spring cleaning .See ./log.txt for a series of small changes linking different pages. STREAMS->STRINGS->STANDARD. . 2009-11-13 Fri Nov 13 13:05 Structured Automata I've recovered some definitions of automata (acceptors, generators, and filters) from an old project: .See ./math_71_Auto...Systems.html#Structured Automata . 2009-11-09 Mon Nov 9 14:56 Started a definition of protocols and messages .See ./math_71_Auto...Systems.html#Protocols . 2009-11-04 Wed Nov 4 15:43 Improved notes on handling natural language tenses .See ./logic_8_Natural_Language.html#Tenses, Time, and Temporal modalities . 2009-11-02 Mon Nov 2 17:54 do and iterate Rediscovered the need for a more obvious, if longer word for repetition: .See ./logic_41_HomogenRelations.html#iterate .See ./intro_relation.html#do . 2009-09-28 Mon Sep 28 13:35 Semantics of subsets I've added some notes on modelling subsets of sets -- example `tall people` vs `short people`: .See ./notn_16_Classification.html . 2009-09-22 Tue Sep 22 15:37 Defined xor and derived inequality of propositions .See ./logic_10_PC_LPC.html I hadn't noticed the '<>' was implicitly defined for propositions as the 'xor' or non-equivalent operator. Also add a table summarizing the commonest propositional operators. . 2009-08-19 Wed Aug 19 14:39 Corrected an error Noticed and corrected an error in .See ./logic_20_Proofs100.html where I had miscalculated some elementary algebra. More evidence for the need of a proof checker. . 2009-07-13 Mon Jul 13 15:07 Improved notes on using relational calculus to shorten proofs .See ./intro_relation.html .See ./logic_25_Proofs.html . 2009-06-11 Thu Jun 11 15:55 Improved proposed notation for problem solving .See ./math_10_Intro.html .See ./notn_13_Docn_Syntax.html . 2009-05-19 Tue May 19 06:33 Improved notes on Dynamics .See ./intro_dynamics.html .See ./math_14_Dynamics.html .See ./math_75_Programs.html Added notation ?? (s.l'=n) ::= (s'=s~l|n) from .See ./todo.html my "to do" list .See ./notn_11_Expressions.html .See ./notn_12_Expressions.html#Free Variables . 2009-04-17 Fri Apr 17 06:49 Small change to Process Algebras .See ./math_73_Process_algebra.html . 2009-01-31 Sat Jan 31 09:01 Thank you Alejandro Alejandro has found an omission in .See ./logic_9_Modalities.html#AW describing the Computational Tree Logic. I fixed it and left a Footnote.... . . 2009-01-14 Wed Jan 14 20:01 Added references to the Tree of Porphyry .See ./logic_8_Natural_Language.html#Stuff . 2009-01-09 Fri Jan 9 10:01 Improved notes on Modal Logic .See ./logic_9_Modalities.html . 2009 . 2008-12-03 Wed Dec 3 11:12 Transfered my unpublished To Do List for MATHS I've taken my personal notes of Problems, Partly Baked Ideas, and To Be Dones from my old Palm Pilot and into .See ./todo.html so I can refer to it from my new iPod.... . 2008-11-12 Wed Nov 12 14:11 Dimensioned Numbers Tidied up the back references in .See ./math_49_Dimensioned_numbers.html and made some small improvements. I also extend my `mth2html` to recognize and render ".{" and ".}" as well as ".(" and ".)". More in the item below. . 2008-11-06 Thu Nov 6 10:11 Possible improved rendering for algorithms etc I've hacked my personal copy of `mth2html` to translate ".(" and ".)" directives into Ordered Lists with class="Formula", and added this rule to my standard style sheet .As_is OL .Formula{ .As_is list-style-type : none; .As_is } I think the effect is quite pleasing. Here is the formula .See ./notn_14_Docn_Semantics.html#Translation into a Z Schema rewritten using this convention -- first rendered and second as source 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); .). .As_is For In:Net, Net_to_Z(In) ::=with{signature, axioms:Sets} following .As_is .( .As_is (signature, axioms) := ({},{}); .As_is do .As_is .(with{piece:piece_of_documentations} .As_is .( .As_is piece:?In; .As_is .( piece in declaration; signature:|declaration_to_Z(piece) .As_is | piece in wff; axioms:|wff_to_Z(piece) .As_is | piece in definition; signature:|definition_to_Z_declaration(piece); axioms:|definition_to_Z_equality(piece) .As_is | piece in (theorem | comment) .As_is .) .As_is .) .As_is .); .As_is end(In); .As_is output_Z_schema(signature, axioms); .As_is .). 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 .See ./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 .See ./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 .See ./notn_14_Docn_Semantics.html and .See ./notn_16_Classification.html As always -- click here .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 .See ./math_94_Calculus.html before we have a complete page. . 2008-10-07 Tue Oct 7 07:10 Corrected syntax of example database definition .See ./math_13_Data_Bases.html#DataBase Which in turn lead to an extension of the notation for discriminated types .See ./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 .See ./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>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 .See ./types.html .See ./math_25_Categories.html .See ./logic_30_Sets.html .See ./intro_sets.html .See ./intro_standard.html .See ./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? .Hole undefinitions . 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 .As_is .But and .As_is .Close.But For example .Let (let)|-It is raining. (let)|-If it rains then I shall get wet. (-1,-2)|- I shall get wet. .Close.Let .But I carry an umbrella. (-1)|- I keep dry. .But In August, I forgot the umbrella, (-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 .See ./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 .See ./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 .See ./logic_30_Sets.html and explicitly linked .See ./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: .See ./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 .See http://csci.csusb.edu/dick/maths/logic_25_Proofs.html#constructive_dilemma . 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 .See 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 .See ./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 .See ./logic_20_Proofs100.html#But Why Prove anything Anyway? and what can be concluded after deriving some results from some assumptions in .See ./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. .See ./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 .Row May 5 10:29 math_92_Metric_Spaces.html .Item Added Notes on Hilbert spaces used in Quantum Theory .Row May 7 17:58 math_81_Probabillity.html .Item Added notes on Expected values, means, variances etc. .Row May 10 09:02 logic_27_Tableaux.html .Item Added a thought about using a table to express a set of cases .Row May 13 07:23 intro_records.html .Item Added notes on optional and multiple parts in a record .Row May 19 14:32 logic_30_Sets.html .Item Added to notes on the Axiom of Choice .Row May 21 20:10 logic_25_Proofs.html .Item Added an example of using table to document proof by cases. .Row May 23 06:49 math_41_Two_Operators.html .Item Added definition of a dioid .Close.Table . 2008 Latest -- .See ./math_92_Metric_Spaces.html .See ./math_5_Object_Theory.html .See ./logic_10_PC_LPC.html .See ./intro_records.html (optional and multiple parts) .See ./intro_objects.html .See ./intro_copywrite.html .See ./notn_14_Docn_Semantics.html .See ./notn_13_Docn_Syntax.html .See ./logic_25_Proofs.html .See ./intro_function.html .See ./math_95_Function_Spaces.html .See ./math_45_Three_Operators.html (Trying to understand Quantum Theory....) -- Oldest . Changes in 2007 Latest -- .See ./logic_10_PC_LPC.html (linking MATHS to Term Logic and Aristotlean Logic) .See ./math_21_Order.html .See ./logic_20_Proofs100.html .See ./math_81_Probabillity.html (Bayesian Probability matches abductive reasoning), .See ./intro_objects.html (exploring adding OO dynamics to Nets), .See ./logic_30_Sets.html .See ./logic_2_Proofs.html .See ./intro_ebnf.html .See ./math_21_Order.html .See ./logic_20_Proofs100.html -- Oldest . Changes in 2006 Latest -- .See ./notn_13_Docn_Syntax.html .See ./intro_characters.html .See ./math.lexicon.html .See ./math.syntax.html (changing notation to separate formula from bullet points/paragraphs), .See ./logic_27_Tableaux.html (Semantic tableax), .See ./logic_2_Proofs.html is now refactored into .See ./logic_20_Proofs100.html and .See ./logic_25_Proofs.html -- Oldest . Changes in 2005 .See ./logic_2_Proofs.html (added more on semantic tableaux) . Changes in 2004 (2004): Latest -- .See http://www/dick/maths/logic_30_Sets.html .See http://www/dick/maths/logic_8_Natural_Language.html .See http://www/dick/maths/notn_14_Docn_Semantics.html .See http://www/dick/maths/notn_12_Expressions.html .See http://www/dick/maths/notn_16_Classification.html .See http://www/dick/maths/notn_13_Docn_Syntax.html .See http://www/dick/maths/notn_3_Conveniences.html .See http://www/dick/maths/notn_2_Structure.html .See http://www/dick/maths/notn_11_Names.html .See http://www.csci.csusb.edu/dick/maths/math_77_Enumerations.html .See http://www/dick/maths/math_25_Categories.html -- Oldest . Changes in 2003 (2003): -- Latest .See http://www/dick/maths/intro_standard.html .See http://www/dick/maths/math_73_Process_algebra.html .See http://www/dick/maths/math_82_MultiSets_and_Bags.html .See http://www/dick/maths/math_83_Fuzzy_Sets.html .See http://www/dick/maths/00_overview.html .See http://www/dick/maths/math_84_Spectra.html .See http://www/dick/maths/notn_9_Tables.html .See http://www/dick/maths/logic_9_Modalities.html .See http://www/dick/maths/logic_41_HomogenRelations.html -- Oldest . Definitions MATHS::=./index.html .Close Recent Changes and thoughts about the MATHS Language