MATHEMATICS
Views include:
- Arithmetic (Egypt - numbers), geometry (Greece - shape), calculus (Europe - 17th century - motion, change, space).
- Counting (arithmetic - number theory - primes), reasoning and communication (logic, Venn diagrams, set theory, grammar), motion and change (series, functions, calculus, differentials, integration, analytic number theory), shape (geometry), symmetry (symmetry groups, sphere packing), position (topology, surfaces, knots, elliptic curves)
- mathematica (...)
High level
Overview
Associations
Universities
Mathematics Subject Classification
Problem hardness
- P versus NP - Wikipedia
- The P versus NP problem is a major unsolved problem in theoretical computer science. In informal terms, it asks whether every problem whose solution can be quickly verified can also be quickly solved.
- Polynomial time - Wikipedia
- An algorithm is said to be of polynomial time if its running time is upper bounded by a polynomial expression in the size of the input for the algorithm, that is, T(n) = O(n^k) for some positive constant k.
- Problems for which a deterministic polynomial-time algorithm exists belong to the complexity class P, which is central in the field of computational complexity theory.
- Cobham's thesis states that polynomial time is a synonym for "tractable", "feasible", "efficient", or "fast".
- Non-deterministic Polynomial time - Wikipedia
- Have proofs verifiable in polynomial time.
- It is easy to see that the complexity class P (all problems solvable, deterministically, in polynomial time) is contained in NP (problems where solutions can be verified in polynomial time), because if a problem is solvable in polynomial time, then a solution is also verifiable in polynomial time by simply solving the problem.
- NP-completeness - short for "nondeterministic polynomial-time complete - Wikipedia
- Although a solution to an NP-complete problem can be verified "quickly", there is no known way to find a solution quickly.
- P versus NP problem - Wikipedia
- Computational complexity - Wikipedia
- Computational complexity theory - Wikipedia
- Complexity classes
- Deterministic time/space: f(n), log(n), poly(n), exponential i.e. 2^poly(n)
- Non-deterministic time/space: non-deterministic version of f(n), log(n), poly(n), exponential i.e. 2^poly(n)
- Computational complexity of mathematical operations - Wikipedia
- Time complexity - Wikipedia
- Time complexity is the computational complexity that describes the amount of computer time it takes to run an algorithm.
- Time complexity is commonly estimated by counting the number of elementary operations performed by the algorithm, supposing that each elementary operation takes a fixed amount of time to perform.
- Thus, the amount of time taken and the number of elementary operations performed by the algorithm are taken to be related by a constant factor.
- Since an algorithm's running time may vary among different inputs of the same size, one commonly considers the worst-case time complexity, which is the maximum amount of time required for inputs of a given size.
- the time complexity is commonly expressed using big O notation, typically O(n), O(log n), O(n^a), etc., where n is the size in units of bits needed to represent the input.
- Algorithmic complexities are classified according to the type of function appearing in the big O notation. For example, an algorithm with time complexity O(n) is a linear time algorithm and an algorithm with time complexity O(n^a) for some constant a > 1 is a polynomial time algorithm.
- Big O notation - Wikipedia
- Subset Sum Problem - Wikipedia
- There is a multiset S of integers and a target-sum T, and the question is to decide whether any subset of the integers sum to precisely T.
- The problem is known to be NP-hard. Moreover, some restricted variants of it are NP-complete.
Arithmetic and Algebra
Arithmetic is the study of the properties of the traditional operations on numbers—addition, subtraction, multiplication, division, exponentiation, and extraction of roots. In the 19th century, Italian mathematician Giuseppe Peano formalized arithmetic with his Peano axioms, which are important to the field of mathematical logic today.
Algebra is the study of variables and the rules for manipulating these variables in formulas; it is a unifying thread of almost all of mathematics.
Algebra began with computations similar to those of arithmetic, with letters standing for numbers. This allowed proofs of properties that are true no matter which numbers are involved. For example, in the quadratic equation ax^{2}+bx+c=0, where a, b, c can be any numbers whatsoever (except that a cannot be 0 and the quadratic formula can be used to quickly and easily find the values of the unknown quantity x which satisfy the equation. That is to say, to find all the solutions of the equation.
- Arithmetic - Wikipedia
- Modular arithmetic developed by Carl Friedrich Gauss in his book Disquisitiones Arithmeticae, 1801
- The modulo operation: the notation b mod n (without parentheses) refers to the modulo operation. Indeed, b mod n denotes the unique integer a such that 0 ≤ a < n and a ≡ b (mod n)(that is, the remainder of b when divided by n
li>The congruence equation: the notation a ≡ b (mod n), where the parentheses mean that (mod n) applies to the entire equation, not just to the right-hand side (here, b).
- Given an integer n > 1, called a modulus, a ≡ b (mod n) if n is a divisor of their difference (if there is an integer k such that a − b = k.n)
- Reduction: 9 (mod 2) ≡ 1 (mod 2) (there is an integer k(=4) such that 9-1 = k.2
- Reduction: 8 (mod 2) ≡ 0 (mod 2) (there is an integer k(=4) such that 8-0 = k.2
- Observation: 7-5=2, 5-7=-2 7 ≡ 5 (mod 2) because 7-5=2, (2 mod 2) = -4 | 2
- In modulus 12, one can assert that 38 ≡ 14 (mod 12) because 38 − 14 = 24 (a multiple of 12, with k=2). Alternatively, 14 ≡ 38 (mod 12) because 14 − 38 = -24 (also a multiple of 12, with k=-2).
- Another way to express this is to say that both 38 and 14 have the same remainder 2, when divided by 12.
- More examples: 8 mod 4 ≡ 0, 7 mod 2 ≡ 1
- The definition of congruence also applies to negative values. For example:
- 2 ≡ − 3 (mod 5) because -3 -2 | 5 (the notation (mod 5) at the end of the expression means mod 5 applies to both sides of the equation)
- − 8 ≡ 7 (mod 5) because 7 - (-8) = 15 | 5
- − 3 ≡ − 8 (mod 5) because -8 - (-3) = 5 | 5
- 1 ≡ − 3 (mod 2) because -3 -1 = -4 | 2
- 330 ≡ -1 (mod 331) because -1 - 330 = -331 | 331
- Modular arithmetic calculator and quite a few other calculators
- Algebra - Wikipedia
- Elementary algebra deals with the manipulation of variables as if they were numbers.
- Abstract algebra is the name given to the study of algebraic structures such as groups, rings, and fields.
- Abstract Algebra - great overview + Sage exercises
- Groups - a group is a set and an operation that combines any two elements of the set to produce a third element of the set, in such a way that the operation is associative, an identity element exists and every element has an inverse
- For example, the integers together with the addition operation form a group.
- Given an integer n > 1, called a modulus, two integers a and b are said to be congruent modulo n, if n is a divisor of their difference (that is, if there is an integer k such that a − b = kn).
- Linear algebra, which deals with linear equations and linear mappings, is used for modern presentations of geometry, and has many practical applications (in weather forecasting, for example).
- There are many areas of mathematics that belong to algebra, some having "algebra" in their name, such as commutative algebra, and some not, such as Galois theory.
Logic
Reasoning
- Inductive reasoning
- A method of reasoning in which the premises are viewed as supplying some evidence, but not full assurance, of the truth of the conclusion.
- It is also described as a method where one's experiences and observations, including what are learned from others, are synthesized to come up with a general truth.
- Many dictionaries define inductive reasoning as the derivation of general principles from specific observations (arguing from specific to general), although there are many inductive arguments that do not have that form
- Conclusions from inductive reasoning are probably, not certain
- Deductive reasoning
- Is the process of reasoning from one or more statements (premises) to reach a logical conclusion.
- Deductive reasoning links premises with conclusions.
- If all premises are true, the terms are clear, and the rules of deductive logic are followed, then the conclusion reached is necessarily true.
Intro and overview
Set theory and Z
Intro
The formal specification notation Z is based on Zermelo-Fraenkel set theory and first order predicate logic.
It has been developed by the Programming Research Group at the Oxford University Computing Laboratory and elsewhere since the late 1970s,
inspired by Jean-Raymond Abrial's seminal work. Z is now defined by the ISO/IEC 13568 standard and is public domain.
Z tools
- CZT - Community Z Tools, including LaTeX styles and parsers, typecheckers, etc
- czt-ide - Releases of standalone CZT IDE, based on Eclipse platform. Use it to author, develop and verify Z specifications.
- Download archived version for Windows 64 bits
- czt-ide-updates - Update sites for released CZT Eclipse plugins to be installed in your own Eclipse IDE.
- czt-jedit - Plugins for the jEdit text editor (www.jedit.org) adding support for typesetting Z specifications.
- czt - Standalone CZT library (classic distribution).
- maven - Instructions how to use CZT libraries deployed to Maven Central.
- CZT Z/Eves- Z Eclipse automated theorem prover IDE
- ZTC- Z type checker
- HOL-Z- High Order Logic Z checker - a plug-in for Isabelle/HOL
Overview
Alloy
Alloy = logic + language + analysis, where
- logic = first order logic + relational calculus
- language = syntax for structuring specifications in the logic
- analysis = bounded exhaustive search for counterexample to a claimed property using SAT
Focused on software engineering
- Alloy- MIT website, from Daniel Jackson
- Alloytools - for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks
Proof assistants
Isabelle (Cambridge/Muenchen)
- Isabelle- generic proof assistant, allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus, originally developed at the University of Cambridge and Technische Universität Muenchen
- Isabelle- University of Cambridge website
- Isabelle- Concrete Semantics (how to)
Coq (INRIA)
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.
- Coq-
- Coq implements a program specification and mathematical higher-level language called Gallina, based on a formal language called the Calculus of Inductive Constructions that itself combines both a higher-order logic and a richly-typed functional programming language
Process calculus
Finite State Machines
- FSM - Wikipedia
- NuSMV- Nex Symbolic Model Checker - open source SAT solver for Temporal Logic such as LTL and CTL - a reimplementation and extension of SMV symbolic model checker
Proposition logic, SAT, SMT
In mathematical logic, satisfiability and validity are elementary concepts of semantics.
- A formula is satisfiable if it is possible to find an interpretation (model) that makes the formula true.
- A formula is valid if all interpretations make the formula true.
SAT
SAT refers to the propositional (or boolean) satisfiability problem.
- Satisfiability.org- conference on propositional satisfiability problem (SAT)
- Satlib- benchmark problems, solvers and tools for SAT research
SMT
Satisfiability Modulo Theories (SMT) is an area of automated deduction that studies methods for checking the satisfiability of first-order formulas
with respect to some logical theory T of interest. It differs from general automated deduction in that the background theory T need not be finitely
or even first-order axiomatizable, and specialized inference methods are used for each theory.
- By being theory-specific and restricting their language to certain classes of formulas
(such as, typically but not exclusively, quantifier-free formulas), these specialized methods can be implemented in solvers that are more efficient
in practice than general-purpose theorem provers.
- An SMT instance is a formula in first-order logic, where some function and predicate symbols have additional interpretations,
and SMT is the problem of determining whether such a formula is satisfiable.
- SMT - Wikipedia
- SMTLIB- the Satisfiability Module Theories library
- Z3- Satisfiability Modulo Theories (SMT) solver by Microsoft
FOL and predicate logic
Basics
Prolog
KIF
- Knowledge Interchange Format - Wikipedia
- Is a computer language designed to enable systems to share and re-use information from knowledge-based systems.
- Similar to frame languages such as KL-One and LOOM but unlike such language its primary role is not intended as a framework for the expression or use of knowledge but rather for the interchange of knowledge between systems.
Has a declarative semantics.Knowledge can be described as objects, functions, relations, and rules.
- It is a formal language, i.e., it can express arbitrary statements in first order logic and can support reasoners that can prove the consistency of a set of KIF statements.
- KIF also supports non-monotonic reasoning.
- Although the original KIF group intended to submit to a formal standards body, that did not occur. A later version called Common Logic has since been developed for submission to ISO and has been approved and published.
- A variant called SUO-KIF is the language in which the Suggested Upper Merged Ontology SUMO) is written.
Subjective logic
Deontic logic
Other
Number theory
Primes
Graphs
Intro
Graph in ZK
DSP - FFT - wavelets - compression
Matrices
Linear Programming
- NIST DADS - Dictionary of Algorithms and Data Structures - includes definitions such as
NP etc, as well as algorithms and datastructures
- NIST GAMS - Guide to available mathematical software - including problem taxonomy
- imaginary.org- education and open source
- iPhython.org
- regex - a regular expression is a sequence of characters that define a search pattern
- A regex processor translates a regular expression into an internal representation which can be executed
and matched against a string representing the text being searched in.
- Each character in a regular expression is either a metacharacter or a regular character
that has a literal meaning.
For example, in the regex a., a is a literal character which matches just 'a', while '.' is a metacharacter
that matches every character except a newline.
- Basics:
- a matches letter 'a'
- [a-z] matches all lower case letters from 'a' to 'z'
- '.' is a metacharacter that matches every character except a newline
- a vertical bar separates alternatives ('or'), e.g. gr(a|e)y
- Quantifiers: a quantifier after a token (such as a character) or group specifies how often that a preceding element is allowed to occur
- ? indicates zero or one occurrences of the preceding element. For example, colou?r matches both "color" and "colour".
- * indicates zero or more occurrences of the preceding element. For example, ab*c matches "ac", "abc", "abbc", "abbbc", and so on.
- + indicates one or more occurrences of the preceding element. For example, ab+c matches "abc", "abbc", "abbbc", and so on, but not "ac"
- {n} means the preceding item is matched exactly n times.
- Anchors:
- ^The matches any string that starts with The
- end$ matches a string that ends with end
- ^The end$ exact string match (starts and ends with The end)
- roar matches any string that has the text roar in it
- Character classes:
- \d matches a single character that is a digit
- \w matches a word character (alphanumeric character plus underscore)
- \s matches a whitespace character (includes tabs and line breaks)
- \d, \w and \s also present their negations with \D, \W and \S respectively,
for example, \D will perform the inverse match with respect to that obtained with \d,
so \D matches a single non-digit character
- . matches any character as a wildcard, for example, a.b matches any string that contains an "a",
then any other character and then a "b",
a.*b matches any string that contains an "a" and a "b" at some later point.
- Escaping: in order to be taken literally, you must escape the characters ^.[$()|*+?{\with a backslash \
as they have special meaning, e.g. \$\d matches a string that has a $ before one digit
- Non-printables: you can match also non-printable characters like tabs \t, new-lines \n, carriage returns \r
- Using \1 to keep part of the pattern: "[a-z][a-z]" will match any two lower case letters.
If you wanted to search for lines that had two adjoining identical letters, this pattern wouldn't help.
You need to remember what you found, and see if the same pattern occurred again.
- To mark part of a pattern using "\(" and "\)",
- To recall the remembered pattern use "\" followed by a single digit.
Therefore, to search for two identical letters, use "\([a-z]\)\1". You can have 9 different remembered patterns.
- Standards: the IEEE POSIX standard has 3 sets of compliance: BRE (Basic Regular Expressions), ERE (Extended Regular Expressions), and SRE (Simple Regular Expressions) - deprecated
- Regex can be used e.g. in grep or sed, such as 'sed 's/regexp/replacement/g' inputFileName > outputFileName'
- In sed the s stands for substitute, while the g stands for global, which means that all matching occurrences in the line would be replaced.
- The replacement can be literal text or a format string containing the characters & for "entire match" or the special escape sequences \1 through \9 for the nth saved sub-expression
- Regex editor e.g. any https corresponds to /[https\:\/\/]/
sed - gnu.org page
sed - wikipedia - basic examples
- Usage: sed SCRIPT INPUTFILE...
- Usage for substitution: sed 's/regexp/replacement/g' inputFileName > outputFileName where
- s represents the substitute command
- g represents the global flag, i.e. replace all occurances found, not only the first one (as by default)
- ...
SageMath.org - OpenSource Mathematica
SageMath expository from David Joyner
SageMath - William Stein
SageMath Wiki
Wolfram's MATHworld - Eric Weisstein's World of Mathematics
Wolfram's Mathematica
Wolfram's search engine/solver - Wolfram Alpha
MathWorks - MATLAB -
NL - The MathWorks - MATLAB & Toolboxes such as:
- Statistic
- Curve Fitting
- Optimization
- Symbolic Math
- Image Processing
- Signal Processing
- Neural Network
- Filter Design
Humour
When a statistician passes the airport security check, they discover a bomb in his bag. He explains. "Statistics shows that the probability of a bomb being on an airplane is 1/1000. However, the chance that there are two bombs at one plane is 1/1000000. So, I am much safer..."
The same statistician later drowned in a river with an average depth of 30 cm.