Today I Learned

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

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.

177: Elementary Embeddings, Elementary Substructures

In logic and model theory, an embedding \gamma : \mathcal{M} \rightarrow \mathcal{N} between \mathcal{L}-structures \mathcal{M, N} is called an elementary embedding if

\mathcal{M} \vDash \phi(a_1, \dots, a_n) \Leftrightarrow \mathcal{N} \vDash \phi(\gamma(a_1), \dots, \gamma(a_n))

for any \mathcal{L}-sentence \phi and a_1, \dots, a_n \in M. A substructure \mathcal{M} \subseteq \mathcal{N} is called an elementary substructure, denoted \mathcal{M} \preceq \mathcal{N}, if the inclusion map is an elementary embedding.

176: Removable Singularities vs. Poles

Let f: \Omega \rightarrow \mathbb{C} be holomorphic on \Omega except at isolated points where it’s undefined. One such isolated point z_0 is said to be removable if f can be extended to include z_0 such that the extension is holomorphic in a neighborhood of z_0. That is, if z_0 is “correctable”.

By contrast, an isolated undefined point is said to be a pole if not removable, but there’s a positive integer n such that z_0 is a removable singularity of the function

f(z)(z - z_0)^n.

In this case, n is called the order of the pole.

175: Tarski’s Theorem

In first-order logic, Tarski’s Theorem states that where \mathcal{M, N} are structures and \mathcal{M} \subseteq \mathcal{N}, the following are equivalent:

  1. \mathcal{M} \preceq \mathcal{N}
  2. For all Y \subseteq N definable over M, if Y \neq \varnothing then Y \cap M \neq \varnothing.


174: Decidability of Recursive, Complete, Satisfiable Theories

It’s pretty much in the title. If T is an \mathcal{L}-theory which is recursive, complete, and satisfiable, then T is decidable. That is, there’s an algorithm which takes an \mathcal{L}-sentence \phi and outputs whether or not T \vDash \phi.

(T being recursive means that there’s an algorithm which similarly takes \phi as input but outputs whether \phi \in T.)

173: Vaught’s Test

In model theory, Vaught’s Test (also known as the Łoś–Vaught test) determines whether certain \mathcal{L}-theories T are complete. It states that if T is satisfiable, has no finite models, and is \kappa-categorical for some \kappa \geq |\mathcal{L}|, then T is complete.

Proof outline Assume T isn’t complete. Then there’s a sentence \phi such that T \nvDash \phi, T \nvDash \neg \phi, meaning T \cup \{\phi\}, T \cup \{\neg \phi \} are satisfiable, meaning both have infinite models (since T has no finite models), so by [172] we can find models \mathcal{M}, \mathcal{N} of cardinality \kappa which respectively satisfy these theories. But since \mathcal{M}, \mathcal{N} disagree on \phi, they are not elementarily equivalent and hence not isomorphic, contradicting the assumption that T is \kappa-categorical. Thus T must be complete.