Today I Learned

Some of the things I've learned every day since Oct 10, 2016

187: Craig Interpolation Theorem

Where \Gamma is a set of first-order formulas, let \mathcal{A}_\Gamma be the set of function, relation, and constant symbols which occur in \Gamma. That is, the smallest set \mathcal{A} such that each formula of \Gamma is an \mathcal{L}_{\mathcal{A}}-formula.

Suppose that \Gamma is any set of formulas, \varphi_1, \varphi_2 are formulas, \Gamma \vdash (\varphi_1 \rightarrow \varphi_2), and that \mathcal{A}_{\{\varphi_1\}} \cap \mathcal{A}_{\{\varphi_2\}} \subseteq \mathcal{A}_\Gamma. Then the Craig Interpolation Theorem states that there is an \mathcal{L}_{\mathcal{A}_\Gamma}-formula \psi, the interpolant, such that

\Gamma \vdash (\varphi_1 \rightarrow \psi)

and

\Gamma \vdash (\psi \rightarrow \varphi_2).

Advertisements

186: Proof by Contradiction

Suppose \Gamma is a set of first-order formulas, \varphi is a first-order formula, and that \Gamma \cup \{\neg \varphi \} is inconsistent. Then \Gamma \vdash \varphi. This can be seen as a formal statement of the legitimacy of proof by contradiction.

Sketch of proof: If \Gamma itself is inconsistent, then it’s trivial that \Gamma \vdash \varphi. Otherwise if \Gamma is consistent, it’s clear that the problem with consistency is the addition of \neg \varphi to \Gamma, implying that \Gamma \vdash \varphi.

185: The Deduction Theorem

Let \Gamma be a set of first-order \mathcal{L}-formulas. Then for \mathcal{L}-formulas \varphi_1, \varphi_2,

\Gamma \cup \{\varphi_1\} \vdash \varphi_2 \Leftrightarrow \Gamma \vdash (\varphi_1 \rightarrow \varphi_2).

The implication from right to left is obvious, and the converse can be proven by induction on formulas.

184: TreeMap vs. HashMap vs. LinkedHashMap (Java)

In Java, TreeMap, HashMap, and LinkedHashMap are all implementations of the Map interface, and are all just different ways of mapping keys to values. Importantly, though, they differ in their lookup and insertion times, as well as ordering they maintain.

  • HashMap is implemented as an array of linked lists, and is the implementation of a hash table most people are probably most familiar with. It offers O(1)  lookup and insertion, but doesn’t maintain any ordering of its keys.
  • TreeMap is implemented as a red-black tree, and so offers O(\text{log} N ) lookup and insertion. However, its keys are ordered according to its keys’ implementation of the \texttt{Comparable} interface.
  • LinkedHashMap is implemented as a linked list and like HashMap offers O(1) time, but in addition maintains ordering of its keys according to the order in which they were added to the map.

When to use which? If you need to retrieve keys ordered by their implementation of \texttt{Comparable} (perhaps when the keys are Integers or Strings), TreeMap can do that. If you need to retrieve keys ordered by their insertion time (as in a caching system), LinkedHashMap can do that. If neither of these orderings is needed, HashMap is the best go-to, being typically faster with less overhead than the other two options.

183: Cauchy’s Argument Principle

In complex analysis, Cauchy’s Argument Principle relates the value of the contour integral of a meromorphic function along a closed curve to the number of poles and zeroes of that function inside the curve:

Suppose f is meromorphic (holomorphic except for on a set of isolated poles) on an open set which contains a closed curve \gamma and its interior, and that f has no zeroes or poles on \gamma. Then

\int _\gamma \frac{f'(z)}{f(z)}dz = 2 \pi i (Z - P),

where Z is the number of zeroes of f inside \gamma, and P the number of poles.

 

182: final (Java)

In Java, the \texttt{final} keyword has several different uses depending on whether it’s used on a variable, method, or class. In all uses, it’s generally used to prevent something from being modified.

A variable declared \texttt{final} can’t have its value modified after declaration. When the variable is primitive, this is straightforward; \texttt{final int x = 5} will always have the value 5. If the variable is a reference type, however, it being final just means it will always point to the same object. The object itself, if mutable like a list, can still change.

A method declared \texttt{final} can’t be overridden.

A class declared \texttt{final} can’t be extended.

181: Vectors (Java)

The Vector class in Java is essentially a legacy version of ArrayList (ArrayList was actually the Java 1.2 Collections replacement for it) which by default synchronized each individual operation. While this makes the structure automatically thread-safe (unlike ArrayList), the better design is to lock sequences of operations rather than individual operations. The result is that in addition to not providing any control over synchronization, the Vector class performs considerably worse than alternatives, such as using Collections.synchronizedList to decorate a non-thread-safe collection such as ArrayList for concurrency. Thus it’s generally recommended that use of the Vectors class be avoided.

180: Software Aging and Rejuvenation

Software aging is the degradation of a software system’s ability to perform correctly after running continuously for long periods of time. Common causes include memory bloating, memory leaks, and data corruption.

To prevent undesirable effects of software aging, software rejuvenation can be done proactively. This can take many forms, the most well-known of which is a simple system reboot. Other forms include flushing OS kernel tables, garbage collection, or Apache’s method of killing and then recreating processes after serving a certain number of requests.

179: Universal Axiomatization and Substructures

Definition universal sentence is a first-order sentence of the form \forall \bar{v} \phi (\bar{v}), where \phi has no quantifiers.

Definition We say an \mathcal{L}-theory T has a universal axiomatization if there’s a set \Gamma of universal \mathcal{L}-sentences such that \mathcal{M} \vDash T if and only if \mathcal{M} \vDash \Gamma.

With the above definitions, an \mathcal{L}-theory  T has a universal axiomatization if and only if wherever \mathcal{M} \vDash T and \mathcal{N \subseteq M} we have that \mathcal{N} \vDash T. In the words of Marker’s Model Theory, “a theory is preserved under substructure if and only if it has a universal axiomatization.”

178: The Residue Formula

In complex analysis, the residue formula states that where f is a holomorphic function on an open set containing a circle C and its interior except for finitely many poles z_1, \dots, z_n in the interior of C,

\int _C f(z) dz = 2 \pi i \sum _{k = 1} ^n \text{res}_{z_k} (f).

That is, the integral of the circe is completely determined by the residues of f about the poles in its interior.