text:
# openListener(String) -- open a port for listening

## Synopsis

• Function: openListener
• Usage:
f = openListener s
• Inputs:
• s, , of the form "\$interface:port". Both parts are optional. If the port is omitted, the colon is optional.
• Outputs:
• f, a file, an open listener on the specified interface of the local host at the specified service port. If the port is omitted, it is taken to be port 2500. If the interface is omitted, the listener accepts connections on all interfaces.

## Description

Use openInOut f to accept an incoming connection on the listener, returning a new input output file that serves as the connection. The function isReady can be used to determine whether an incoming connection has arrived, without blocking.


text:
## IFIP Working Group 2.2 Meeting 25 - 29 September 2000, Oldenburg, Germany.

### Davide Sangiorgi (joint work with Francesca Levi) Controlling Interference in Ambients

Two forms of interferences are individuated in Cardelli and Gordon's Mobile Ambients (MA): plain interferences, which are similar to the interferences one finds in CCS and pi-calculus; and grave interferences, which are more dangerous and may be regarded as programming errors. To control interferences, the MA movement primitives are modified. On the new calculus, the Safe Ambients (SA), a type system is defined that: controls the mobility of ambients; removes all grave interferences. Other advantages of SA are: a useful algebraic theory; programs sometimes more robust (they require milder conditions for correctness) and/or simpler. These points are illustrated on several examples.

The talk is based on joint work with Francesca Levi (University of Pisa), published in the proceedings of POPL'00.

### Wojciech Penczek Efficient methods for model checking of Timed Petri Nets

Model checking is one of the most popular methods of automated verification of concurrent systems, e.g., hardware circuits, communication protocols, and distributed programs. However, the practical applicability of this method is strongly restricted by the state explosion problem, which is mainly caused by representing concurrency of operations by their interleaving. Therefore, many different reduction techniques have been introduced in order to alleviate the state explosion. The major methods include application of partial order reductions, symmetry reductions, abstraction techniques, BDD-based symbolic storage, and SAT-related algorithms. Recently, the interest in automated verification is moving towards concurrent real-time systems. Two main models for representing such systems are usually exploited: timed automata and Time Petri Nets. The properties to be verified are expressed in either a standard temporal logic like LTL and CTLS, or in its timed versions like LTL$_\Delta$, MITL, and TCTL. The lecture is on verification of timed and untimed branching time temporal properties of Time Petri Nets. Since Time Petri Nets have usually infinite state spaces, abstraction techniques are used to represent these by finite ones. To reduce the sizes of abstract state spaces partial order reductions are exploited. In this lecture an automata-theoretic approach to model-checking is applied. The theoretical framework developed by Kupferman-Vardi-Wolper is used, where it is shown that the problem of branching-time model checking can be translated to checking the non-emptiness of an alternating 1-letter word automaton. The latter problem is known to have a linear complexity, which allows to perform verification efficiently. The outline of the lecture is as follows:
• Introduction to model checking - automata-theoretic approach,
• Reduction methods for untimed global state approaches: on-the-fly, po-reductions, symbolic (BDDs), translation to SAT,
• Timed and untimed temporal logics: LTL, CTLS, ACTLS, LTL$_\Delta$, MITL, and TCTL,
• Translations from temporal logics to automata,
• Timed Petri Nets,
• Abstractions preserving timed and untimed temporal logics,
• Partial order reductions for Time Petr Nets.
The main novelty of the presented work relies on:
• improving the variant of the geometric region method for defining abstract state spaces preserving properties of \CTLS\/ and \ACTLS\/ such that the structure of a verified formula is exploited,
• showing how to extend the po-reduction methods to deal with branching properties of Time Petri Nets.
The lecture is based on the following papers of the author:
• W. Penczek: Partial order reductions for checking branching properties of Timed Petri Nets, Proc. of CS\&P, Berlin, to appear, 2000.
• W. Penczek, M. Szreter, R. Gerth and R. Kuiper: Improving Partial Order Reductions for Universal Branching Timed Properties, Fundamenta Informaticae, to appear, 2000.
• M. Szreter and W. Penczek: More than one, less than all: Linear to Branching revisited, Proc. of CS\&P, Berlin, to appear, 2000.
• R. Gerth, R. Kuiper, D. Peled, and W. Penczek: A Partial Order Approach to Branching Time Logic Model Checking, Information and Computation, Vol. 150, No. 2, pp. 132-152, 1999.

### Igor Walukiewicz Deciding low levels of the mu-calculus alternation hierarchy

Consider the hierarchy obtained by alternating least and greatest fixpoints in mu-calculus terms. Alternatively this hierarchy can be characterised by sizes of winning conditions in automata on trees. The problem is: "given a regular tree language establish the least number of fixpoint alternations needed to write a term defining the language".

I will show that it is EXPTIME-complete to decide if the language can be written using the least fixpoints only. The same bound also holds for terms with only the greatest fixpoints. The case of mixed (but not alternating) fixpoints is already much more difficult to solve. The subject is also a good occasion to give a very short summary of what is known about the alternation hierarchy.

### Georghe Stefanescu Using space-time duality to structure interaction systems

Space-time duality may by used to transform simple imperative programs into (pure) object-oriented programs. By this mechanism the usual memory states describing (spatial) interfaces of imperative programs are transformed into temporal interfaces of interacting systems. As a side-effect, this suggest a way to pass from the current stream-based temporal interfaces to abstract, highly structured temporal interfaces. In the same time, the well-known techniques used for structured programms in imperative programming area may be used to obtain structural interaction systems. Finaly, but clearly a very important point, the classical program verification techniques for imerative programms may be used to get similar tools for object-orineted programs.

The aim of the talk is to present the space-time duality mechanism and to look at a few aspects of the interaction systems which have to be reconsidered in the view of space-time duality. Also, a few technical ingredients, most of them based on the network algebra approach, will be presented.

For more on this, one may have a look on the book: G. Stefanescu, Network Algebra, Springer-Verlag, London/Berlin/... http://funinf.cs.unibuc.ro/~ghstef/na/myAdv.html

### Hans Langmaack (work with M. Mueller-Olm and A. Wolff) On preservation of relative correctness

M. Mueller-Olm and A. Wolf have introduced the notions relative correctness of programs'' and preservation of relative correctness of program implementations and of compilations''. These notions generalize the notions of total resp. partial correctness and their preservations. The latter notions do not satisfy enough the requirements in practical software engineering and program compilation. Realistic software implementation and compiler construction have to master in the same context both types of errors: of acceptable, excusable, unavoidable errors on the one hand and of unacceptable, inexcusable, avoidable ones on the other.

It is quite known that total program correctness is more difficult to prove than partial correctness. But it is most interesting to see that for preservation of total resp. partial correctness the situation is the other way round. This phenomenon has been first observed when compiling while-programs into flat assembly code with unconditional and conditional jumps [MOl95] and later when translating ALGOL-like programs with nested blocks, parameterless procedures and static scoping into flat assembly code augmented by subroutine and return jumps [MOW00,Wol00]. Source languages are assumed to be furnished with denotational (predicate transformer) semantics, target languages with operational step semantics.

The decisive difference is evoked by the premis whether divergence (infinite computation) is considered to be an unacceptable error (generalized total correctness) or to be an acceptable one (generalized partial correctness). The inductive proof of generalized total correctness preservation utilizers just a series of algebraic laws for assembly instructions semantics. But above that, proof of preservation of generalized partial correctness has to exploit a fixpoint characterization of the operational target semantics. In case divergence is unacceptable operational target semantics is indeed the least fixpoint of a certain functional, otherwise the largest fixpoint [MOl97,MOW99,MOW00,Wol00].

Easiness of proof might be an indication why software engineering in the past has favoured preservation of total correctness for software implementation. But in usual information processing outside process programming preservation of (generalized) partial correctness is at least as important, especially because realistic target machines with their finite resources cannot fulfill all total program correctness wishes.

Most realistic compilers do a lot of code optimizations like dead or redundant code elimination, code motion or unswitching. But often language and compiler manuals do not inform the users decently enough about correctness of optimizations, namely what conditions source programs must fulfill and what consequences on computing results are to be expected. Relative program correctness and its preservartion allow very precise investigations and delineations of these conditions and consequences [MOW99,MOW00,Wol00].

[MOl95]
M. Mueller-Olm. An Exercise in Compiler Verification. Kiel, 1995. Available from the author.
[MOl97]
M. Mueller-Olm. Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction. LNCS, Vol. 1283, Springer-Verlag, 1997.
[MOW99]
M. Mueller-Olm and A. Wolf. On Excusable and Inexcusable Failures: On an Adequate Notion of Translation Correctness. In J. Wing, J. Woodcock and J. Davies (eds.), FM '99 - Formal Methods. LNCS, vol. 1709, 1107 - 1127, Springer-Verlag, 1999.
[MOW00]
M. Mueller-Olm and A. Wolf. On the Translation of Procedures to Finite Machines: Abstraction allows a Clean Proof. In G. Smolka (ed.) Programming Languages and Systems. Proc. ESOP 2000, LNCS, vol. 1782, 290 - 304, Springer-Verlag, 2000.
[Wol00]
A. Wolf. Weakest Relative Precondition Semantics: Balancing Approved Theory and Realistic Translation Verification. Univ. Kiel, dissertation, subm. 2000.

abstract

### Catuscia Palamidessi Probabilistic asynchronous $\pi$-calculus

We propose an extension of the asynchronous $\pi$-calculus with a notion of random choice. We define an operational semantics which distinguishes between probabilistic choice, made internally by the process, and nondeterministic choice, made externally by an adversary scheduler. This distinction will allow us to reason about the probabilistic correctness of algorithms under certain schedulers. We show that in this language we can solve the electoral problem, which was proved not possible in the asynchronous $\pi$-calculus. Finally, we show an implementation of the probabilistic asynchronous $\pi$-calculus in a Java-like language.

### Philippe Darondeau (joint work with B.Caillaud, L.Helouet, and G.Lesventes) Realizing HMSC's by Distributable PN's

High Level Message Sequence Charts (HMSC's) may be considered as specifications for distributed systems. Realization thereof may be seeked in distributable Petri nets, a subclass of Petri nets where transitions are endowed with locations and conflicts between transitions are always local. Distributable nets translate actually to equivalent (up to branching bisimulation) families of automata communicating by asynchronous messages. One can unfortunately not decide whether a given HMSC may be realized exactly (i.e. up to the equality of languages) by some distributable Petri net. We advocate therefore for taking HMSC's as incomplete specifications. In this case, each HMSC has an optimal realization by a distributable Petri net, with the least language including the language of the HMSC. This realization may be computed and it may also be model-checked. We set the question whether relations between specifications and realizations of reactive systems should not be reconsidered in this way.

### Masahiko Sato $\alpha$: A purely functional language with imperative language inside

We present a purely functional language $\alpha$ that naturally contains an imperative language as its sublanguage. $\alpha$ is pure in the sense that (1) it is confulent and (2) it is a conservative extension of the pure $\lambda$ calculus. The purity of $\alpha$ makes it a mathematically and logically well founded language. For example, it becomes possible to prove properties of programs written in $\alpha$ by equational reasoning.

The main characteristic of $\alpha$ is that it has environments as first-class objects. By using first-class environments, we can encapsulate imperative programs by treating imperative programs as environment tranformers. In this way, side-effects caused by the execution of imperative programs becomes invisible from outside.

We also discuss another usages of first-class environments. For example, we show that given an abstract obtained by abstracting several variables, we can instantiate any of these variables by specifying the name of the variable to be instantiated and the value which will replace the variable.

WG 2.2 (darondeau@irisa.fr)

format: plain


text:
# Why are relativistic quantum field theories so much more restrictive than non-relativistic ones?

One of the reasons relativistic theories are so restrictive is because of the rigidity of the the symmetry group. Indeed, the (homogeneous part) of the same is simple, as opposed to that of non-relativistic systems, which is not.

The isometry group of Minkowski spacetime is $$\mathrm{Poincar\acute{e}}=\mathrm{ISO}(\mathbb R^{1,d-1})=\mathrm O(1,d-1)\ltimes\mathbb R^d$$ whose homogeneous part is $\mathrm O(1,d-1)$, the so-called Lorentz Group1. This group is simple.

On the other hand, the isometry group of Galilean space+time is2 $$\text{Bargmann}=\mathrm{ISO}(\mathbb R^1\times\mathbb R^{d-1})\times\mathrm U(1)=(\mathrm O(d-1)\ltimes\mathbb R^{d-1})\ltimes(\mathrm U(1)\times\mathbb R^1\times\mathbb R^{d-1})$$ whose homogeneous part is $\mathrm O(d-1)\ltimes\mathbb R^{d-1}$, the so-called (homogeneous) Galilei Group. This group is not semi-simple (it contains a non-trivial normal subgroup, that of boosts).

There is in fact a classification of all physically admissible kinematical symmetry groups (due to Lévy-Leblond), which pretty much singles out Poincaré as the only group with the above properties. There is a single family of such groups, which contains two parameters: the AdS radius $\ell$ and the speed of light $c$ (and all the rotation invariant İnönü-Wigner contractions thereof). As long as $\ell$ is finite, the group is simple. If you take $\ell\to\infty$ you get Poincaré which has a non-trivial normal subgroup, the group of translations (and if you quotient out this group, you get a simple group, Lorentz). If you also take $c\to\infty$ you get Bargmann (or Galilei), which also has a non-trivial normal subgroup (and if you quotient out this group, you do not get a simple group; rather, you get Galilei, which has a non-trivial normal subgroup, that of boosts).

Another reason is that the postulate of causality is trivial in non-relativistic systems (because there is an absolute notion of time), but it imposes strong restrictions on relativistic systems (because there is no absolute notion of time). This postulate is translated into the quantum theory through the axiom of locality, $$[\phi(x),\phi(y)]=0\quad\forall x,y\quad \text{s.t.}\quad (x-y)^2<0$$ where $[\cdot,\cdot]$ denotes a supercommutator. In other words, any two operators whose support are casually disconnected must (super)commute. In non-relativistic systems this axiom is vacuous because all spacetime intervals are timelike, $(x-y)^2>0$, that is, all spacetime points are casually connected. In relativistic systems, this axiom is very strong.

These two remarks can be applied to the theorems you quote:

• Reeh-Schlieder depends on the locality axiom, so it is no surprise it no longer applies to non-relativistic systems.

• Coleman-Mandula (see here for a proof). The rotation group is compact and therefore it admits finite-dimensional unitary representations. On the other hand, the Lorentz group is non-compact and therefore the only finite-dimensional unitary representation is the trivial one. Note that this is used in the step 4 in the proof above; it is here where the proof breaks down.

• Haag also applies to non-relativistic systems, so it is not a good example of OP's point. See this PSE post for more details.

• Weinberg-Witten. To begin with, this theorem is about massless particles, so it is not clear what such particles even mean in non-relativistic systems. From the point of view of irreducible representations they may be meaningful, at least in principle. But they need not correspond to helicity representations (precisely because the little group of the reference momentum is not simple). Therefore, the theorem breaks down (as it depends crucially on helicity representations).

• Spin-statistics. As in Reeh-Schlieder, in non-relativistic systems the locality axiom is vacuous, so it implies no restriction on operators.

• CPT. Idem.

• Coleman-Gross. I'm not familiar with this result so I cannot comment. I don't even know whether it is violated in non-relativistic systems.

1: More generally, the indefinite orthogonal (or pseudo-orthogonal) group $\mathrm O(p,q)$ is defined as the set of $(p+q)$-dimensional matrices, with real coefficients, that leave invariant the metric with signature $(p,q)$: $$\mathrm O(p,q):=\{M\in \mathrm{M}_{p+q}(\mathbb R)\ \mid\ M\eta M^T\equiv \eta\},\qquad \eta:=\mathrm{diag}(\overbrace{-1,\dots,-1}^p,\overbrace{+1,\dots,+1}^q)$$

The special indefinite orthogonal group $\mathrm{SO}(p,q)$ is the subset of $\mathrm O(p,q)$ with unit determinant. If $pq\neq0$, the group $\mathrm{SO}(p,q)$ has two disconnected components. In this answer, "Lorentz group" may refer to the orthogonal group with signature $(1,d-1)$; to its $\det(M)\equiv+1$ component; or to its orthochronus subgroup $M^0{}_0\ge+1$. Only the latter is simply-connected. The topology of the group is mostly irrelevant for this answer, so we shall make no distinction between the three different possible notions of "Lorentz group".

2: One can prove that the inhomogeneous Galilei algebra, and unlike the Poincaré algebra, has a non-trivial second co-homology group. In other words, it admits a non-trivial central extension. The Bargmann group is defined precisely as the centrally extended inhomogeneous Galilei group. Strictly speaking, all we know is that the central extension has the algebra $\mathbb R$; at the group level, it could lead to a factor of $\mathrm U(1)$ as above, or to a factor of $\mathbb R$. In quantum mechanics the first option is more natural, because we may identify this phase with the $\mathrm U(1)$ symmetry of the Schrödinger equation (which has a larger symmetry group, the so-called Schrödinger group). Again, the details of the topology of the group are mostly irrelevant for this answer.

Lorentz invariance is also an indirect contributor to the restrictions that renormalizability places on the theory. The logic goes something likes this:

1. The action must be Lorentz invariant, thus the number of spatial derivatives must equal the number of time derivatives in the action.
2. We want the Hamiltonian to play the role of energy (has lower bound and provides stability), therefore the action can have no more than two time derivatives (for more, see: this previous answer on renormalization).
3. By 1 and 2, the propagator $\Delta(x,y)$ will, necessarily, diverge like $\left([x^\mu-y^\mu][x_\mu-y_\mu]\right)^{-1}$ as $x\rightarrow y$ (equivalently, the momentum space form looks like $(p^\mu p_\mu)^{-1}$ for $p\rightarrow \infty$).

It is that third step that leads to the divergences that require renormalization, and renormalizibility is very restrictive on what terms the action is allowed to contain. Without Lorentz invariance, we could add more spatial derivatives without time derivatives, produce a well behaved finite propagator, and work with a much broader class of theories.

Granted, as discussed in the linked answer, you could relax 2, some, but that doesn't allow any theory, just more.

Here's one (incomplete) perspective, mostly about the infrared:

For a field with given charges under Lorentz and all other symmetries, there is essentially only one theory with quadratic action to first order in derivatives. For integer spins it's $\partial_\mu \phi \partial^\mu \phi + m^2 \phi^2$ and for half integer spins it's $\bar \psi \gamma^\mu D_\mu \psi + m \bar \psi \psi$. This is a fact of representation theory, and the fact that all you have to contract spacetime indices are $g_{\mu \nu}$, $\gamma^\mu$, and things with more spacetime indices. Note that the form of these actions determine the bare propagators to be the relativistic ones $1/(p^2 - m^2)$ and $1/(p-m)$, respectively.

On the other hand, if you were to break Lorentz symmetry, say by choosing a vector field $v^\mu$, then you could write terms like $\phi v^\mu \partial_\mu \phi$, which would change the dispersion relation for $\phi$ to be linear in $p$ for momenta parallel to $v$. Note that for timelike $v$ this breaks the Lorentz group $SO(1,d)$ to $SO(d)$.

For an applied magnetic field $F_{ij}$ on fermions we could add a term $\bar \psi F_{ij} \gamma^i \gamma^j \psi$ which can mess up spin-statistics.

I think these new Gaussian fixed points" cause lots of things to go wonky (in the IR) when you do perturbation theory around them.

On the other hand, there aren't that many terms that can lead these ones, and because of that most of the theories we end up studying in condensed matter have emergent Lorentz invariance in the IR. Some significant exceptions are theories with singular fermi surface or others with UV/IR" mixing that cause the field theory to see the lattice.


text:
# Example 2, Sec. 25 in Munkres TOPOLOGY 2nd ed: Is this subspace also connected?

The topologist's sine curve is the closure $\overline{S}$ of the subset $S$ of $\mathbb{R}^2$, where $$S\ = \ \{ \ x \times \sin \frac{1}{x} \ \colon \ 0 < x \leq 1 \ \}.$$ So $$\overline{S} = S \cup V,$$ where $$V = \{0 \} \times [-1,1].$$

Now let $A$ the subset of $V$ obtained by removing all points with rational second co-ordinates; that is let $$A = \{0\} \times \left( [-1,1] - \mathbb{Q} \right).$$

Then $A$ is not connected as a subspace of $V$. Am I right?

Is $A$ connected as a subsapce of $\overline{S}$?

• Regarding question 2: It looks like $A$ is not a subspace of $S$ at all; am I misunderstanding something? – Eric Stucky May 6 '15 at 7:03
• @EricStucky, you're absolutely right. I'll edit my post forthwith. – Saaqib Mahmood May 6 '15 at 7:48
• I've made a correction to my original post. – Saaqib Mahmood May 6 '15 at 12:19

Suppose $A$ is connected, and consider the inclusion mappings $A \to V \to \Bbb{R^2}$. These maps are continuous, so you conclude that $A$ is connected also as a subspace of $\Bbb{R}^2$. Contradiction.
• $A$ is not connected in $V$. Can't we use the same argument with $V$ replaced by $\overline{S}$ to conclude that $A$ is not connected in $\overline{S}$? – Saaqib Mahmood May 6 '15 at 7:51
• Oh, yes, this argument applies on every set containing $A$. – Crostul May 6 '15 at 7:55


text:
Michaelis–Menten kinetics

Model of enzyme kinetics

In biochemistry, Michaelis–Menten kinetics is one of the best-known models of enzyme kinetics. It is named after German biochemist Leonor Michaelis and Canadian physician Maud Menten. The model takes the form of an equation describing the rate of enzymatic reactions, by relating reaction rate ${\displaystyle v}$ (rate of formation of product, ${\displaystyle [{\ce {P}}]}$) to ${\displaystyle [{\ce {S}}]}$, the concentration of a substrate S.

Quotes

• ${\displaystyle {\frac {d{x}}{d{t}}}=k_{3}p={\frac {k_{3}e(a-x)}{a-x+{\frac {k_{2}+k_{3}}{k_{1}}}}}}$
This is Michaelis and Menten's [1913] equation, (k2 + k3)/k1 representing their constant Ks. […] It may be remarked that with this modification of their theory, Michaelis and Menten's analysis of the effects of the products of the reaction, or other substances which combine with the enzyme, still holds good.


text:
# Binomial Theorem implementation, including complex numbers

#include <iostream>
#include <complex>
#include <vector>
#include <cmath>

/*
*/
template<typename T = int, typename U = unsigned long long int>
inline U computeBinomialCoefficient(const T& n, const T& k) {
if (n == k || k == 0) {
return 1;
}

U out = n - k + 1;

for (T i = 1; i < k; ++i) {
out = out * (n - k + 1 + i) / (i + 1);
}

return out;
}

/*
compute the horizontal shift of a polynomial
with coefficients coeffs (decreasing order)
by shift units
*/
template<typename T = int>
const std::vector<T> computeHorizontalShiftBinomialThm(const std::vector<T>& coeffs, const T& shift) {
std::size_t size = coeffs.size();
std::vector<T> out (size, 0);

for (std::size_t i = 0; i < size; i++) {
T coefficient = coeffs[i];
if (coefficient == 0) {
continue;
}

std::size_t n = size - i - 1; // power of monomial
for (std::size_t k = 0; k <= n; k++) {
T kthPower = computeBinomialCoefficient(n, k) * powl(-1 * shift, n - k);
out[size - k - 1] += coefficient * kthPower;
}
}

return out;
}

/*
Specialization for std::complex
*/
template<typename ComplexType>
const std::vector<std::complex<ComplexType>> computeHorizontalShiftBinomialThm(const std::vector<std::complex<ComplexType>>& coeffs, const std::complex<ComplexType>& shift) {
using imag = std::complex<ComplexType>;

std::size_t size = coeffs.size();
std::vector<imag> out (size, 0);

for (std::size_t i = 0; i < size; i++) {
imag coefficient = coeffs[i];
if (coefficient == std::complex<ComplexType>(0, 0)) {
continue;
}

std::size_t n = size - i - 1; // power of monomial
for (std::size_t k = 0; k <= n; k++) {
ComplexType binomialCoeff = computeBinomialCoefficient(n, k);
imag power = (imag) pow(shift * (ComplexType) -1, n - k);
imag kthPower = (std::complex<decltype(binomialCoeff)>) power * binomialCoeff;
out[size - k - 1] += coefficient * kthPower;
}
}

return out;
}

template<typename T>
void print(const std::vector<T>& vec) {
for (const T& n : vec) {
std::cout << n << " ";
}
std::cout << "\n";
}

int main()
{
std::vector<int> intCoeffs {2, 19, 0, 0, 1};
int intShift {5};

auto intExample = computeHorizontalShiftBinomialThm(intCoeffs, intShift);
print(intExample);

std::vector<std::complex<double>> imaginaryCoeffs {1, 0, 0, 0};
std::complex<double> imaginaryShift (0, 2);

auto complexExample = computeHorizontalShiftBinomialThm(imaginaryCoeffs, imaginaryShift);
print(complexExample);

return 0;
}

And it works! I get out

2 -21 15 425 -1124
(1,0) (3.67394e-16,-6) (-12,-1.46958e-15) (-1.46958e-15,8)

How can I reduce/eliminate floating point error, increase speed, and make the code easier to read?

# Avoid needing to specialize

It is possible to make just one template that can compute the desired result without having a specialization for std::complex. You just have to ensure that variables get their correct type. Some tricks you can use:

• Use T{} to get a default initialized value of type T; this is the way to get a correctly typed zero.
• Use auto where possible to let the compiler deduce the right type.
• Use operators or functions to get a result of the right type, for example:
• Write -foo instead of -1 * foo.
• Use decltype(std::abs(value)) to get a scalar type even if value is std::complex.

Here is your template rewritten to work with std::complex:

template<typename T = int>
const std::vector<T> computeHorizontalShiftBinomialThm(const std::vector<T>& coeffs, const T& shift) {
std::size_t size = coeffs.size();
std::vector<T> out (size, 0);

for (std::size_t i = 0; i < size; i++) {
T coefficient = coeffs[i];
if (coefficient == T{}) {
continue;
}

std::size_t n = size - i - 1;
for (std::size_t k = 0; k <= n; k++) {
T binomialCoeff = computeBinomialCoefficient(n, k);
auto power = std::pow(-shift, n - k);
auto kthPower = power * binomialCoeff;
out[size - k - 1] += coefficient * kthPower;
}
}

return out;
}

The only issue with the above code is that you want extended precision for some temporary variables like binomialCoeff and power. In particular you want to use long long if T is an integer type, long double if it's a floating point type, and std::complex<long double> if it's a complex number. To tackle this, I would create a separate template function to compute kthPower, and then this could be specialized for integers, floating point and complex types.

# Use std:: versions of math functions

Use std::pow() instead of pow(). The C++ versions of the math functions have overloads for the various floating point types, so you don't have to worry about whether you are passing in a float, double, long double. Even better, std::pow() has overloads where the first argument is a floating point number but the second is an integer, so it can choose a more optimal implementation for raising values to an integer power.

The same goes for all other function from <cmath>.

# Avoid unnecessary copies

You already pass the parameters by reference, which is great, especially if you pass containers or types of which you don't know the size. However, there are a few other places where copies could be made that might be expensive depending on the type.

The first is in the for-loop in computeBinomialCoefficient(). Use out *= ... instead of out = out * ....

The other is coefficient in computeHorizontalShiftBinomialThm(). Use this instead:

const T& coefficient = coeffs[i];

For simple types like float, double and even std::complex types, the compiler will likely produce exactly the same code either way, but consider for example someone using a BigInt library and wanting to process very large numbers.

# Naming things

Your functions have very long names. Consider finding ways to make them more concise while still being clear and descriptive given the context they would be used in. I would drop the prefix compute; you won't see a compute_sin() function in the standard library for example. Use binomial() instead of computeBinomialCoefficient(). I think it is usually clear that a function with that name that takes two parameters produces the binomial coefficient as the output. As for the function that does the horizontal shift, it might be a bit hard to come up with a better name apart from dropping the compute part.

Be consistent when naming things. I see both coefficient and the abbreviation coeff being used. Choose one and use it everywhere.

One suggestion that I think is good is to cache the Ncr results.

struct Ncr {
using T = long double;
static std::vector<T> &fact() {
static std::vector<T> _fact{1};
return _fact;
}

static std::vector<T> &inv_fact() {
static std::vector<T> _inv_fact{1};
return _inv_fact;
}

static T C(int n, int k) {
if (k < 0 || k > n) {
return 0;
}
while ((int) fact().size() < n + 1) {
fact().push_back(fact().back() * (int) fact().size());
inv_fact().push_back(1 / fact().back());
}
return fact()[n] * inv_fact()[k] * inv_fact()[n - k];
}
};

I have added an example code and to use it you can directly call it by Ncr::C(n, k) this will save all the previous results and you might not have to recompute every time. You have to make sure you don't actually run this with int or any other small-sized DS as factorials encreases polynomially and can overflow in case of int or long long. That's why using long double might be helpful here.
Also, notice the long double this is actually to improve the precision. When I run the code I got the following output.

2 -21 15 425 -1124
(1.000000,0.000000) (0.000000,-6.000000) (-12.000000,-0.000000) (-0.000000,8.000000)


text:
# American Institute of Mathematical Sciences

ISSN:
2158-2491

eISSN:
2158-2505

All Issues

## Journal of Computational Dynamics

April 2021 , Volume 8 , Issue 2

Select all articles

Export/Reference:

2021, 8(2): 131-152 doi: 10.3934/jcd.2021006 +[Abstract](1610) +[HTML](465) +[PDF](3923.59KB)
Abstract:

We propose a deep neural network architecture and associated loss functions for a training algorithm for computing approximate Lyapunov functions of systems of nonlinear ordinary differential equations. Under the assumption that the system admits a compositional Lyapunov function, we prove that the number of neurons needed for an approximation of a Lyapunov function with fixed accuracy grows only polynomially in the state dimension, i.e., the proposed approach is able to overcome the curse of dimensionality. We show that nonlinear systems satisfying a small-gain condition admit compositional Lyapunov functions. Numerical examples in up to ten space dimensions illustrate the performance of the training scheme.

2021, 8(2): 153-163 doi: 10.3934/jcd.2021007 +[Abstract](607) +[HTML](264) +[PDF](323.78KB)
Abstract:

The shuffle algorithm is applied to analysis of the fractional descriptor discrete-time linear systems. Using the shuffle algorithm the singularity of the fractional descriptor linear system is eliminated and the system is decomposed into dynamic and static parts. Procedures for computation of the solution and dynamic and static parts of the system are proposed. Sufficient conditions for the positivity of the fractional descriptor discrete-time linear systems are established.

2021, 8(2): 165-181 doi: 10.3934/jcd.2021008 +[Abstract](638) +[HTML](260) +[PDF](788.43KB)
Abstract:

We propose a numerical approach for computing center manifolds of equilibria in ordinary differential equations. Near the equilibria, the center manifolds are represented as graphs of functions satisfying certain partial differential equations (PDEs). We use a Chebyshev spectral method for solving the PDEs numerically to compute the center manifolds. We illustrate our approach for three examples: A two-dimensional system, the Hénon-Heiles system (a two-degree-of-freedom Hamiltonian system) and a three-degree-of-freedom Hamiltonian system which have one-, two- and four-dimensional center manifolds, respectively. The obtained results are compared with polynomial approximations and other numerical computations.

2021, 8(2): 183-211 doi: 10.3934/jcd.2021009 +[Abstract](522) +[HTML](228) +[PDF](1235.6KB)
Abstract:

Manin transformations are maps of the plane that preserve a pencil of cubic curves. They are the composition of two involutions. Each involution is constructed in terms of an involution point that is required to be one of the base points of the pencil. We generalise this construction to explicit birational maps of the plane that preserve quadratic resp. certain quartic pencils, and show that they are measure-preserving and hence integrable. In the quartic construction the two involution points are required to be base points of the pencil of multiplicity 2. On the other hand, for the quadratic pencils the involution points can be any two distinct points in the plane (except for base points). We employ Pascal's theorem to show that the maps that preserve a quadratic pencil admit infinitely many symmetries. The full 18-parameter QRT map is obtained as a special instance of the quartic case in a limit where the two involution points go to infinity. We show by construction that each generalised Manin transformation can be brought to QRT form by a fractional affine transformation. We also specify classes of generalised Manin transformations which admit a root.

2021, 8(2): 213-240 doi: 10.3934/jcd.2021010 +[Abstract](1279) +[HTML](253) +[PDF](1216.17KB)
Abstract:

In this paper we consider the Shigesada-Kawasaki-Teramoto (SKT) model to account for stable inhomogeneous steady states exhibiting spatial segregation, which describe a situation of coexistence of two competing species. We provide a deeper understanding on the conditions required on both the cross-diffusion and the reaction coefficients for non-homogeneous steady states to exist, by combining a detailed linearized analysis with advanced numerical bifurcation methods via the continuation software $\mathtt{pde2path}$. We report some numerical experiments suggesting that, when cross-diffusion is taken into account, there exist positive and stable non-homogeneous steady states outside of the range of parameters for which the coexistence homogeneous steady state is positive. Furthermore, we also analyze the case in which self-diffusion terms are considered.

2020 CiteScore: 1


text:
Danielle P.

# how do i find where a function is discontinuous if the bottom part of the function has been factored out?

my problem is:

Indicate all values for which the function is discontinuous. for each discontinuity point "a" give the limit of the function as x approaches "a". Clearly indicate limits that do not exist.

(10-x)/ ((x-2)(x-3))

By:

Mathematics/writing tutor, with degrees in math and education

Danielle P.

okay so the rational function ((x^2)-4)/((x-2)(x+3)) i just described would still be discontinuous at x=2 and x=-3, correct?

and then when it is time to find the limit for both of them there limits would not exist because the limits are -infinity and infinity because as x approaches both numbers the function gets bigger and bigger? or am i totally off base?

Report

09/30/12

Jonathan F.

You can have a limit at a point outside of the domain. So the limit as x approaches 2 would be 4/5 (as you saw from your simplification), but the point 2 is discontinuous and not actually a part of the function. If you were to graph it you would make an open circle on the graph where x=2 to represent this.

The limit as x approached -3 would be -8, you solve that one normally.

Report

09/30/12

Jonathan F.

Sorry it pasted funky when i tried to help you with -3.

As x approaches -3 from the left does it go to + or - inf? When it approaches from the left does it go to + or - inf?

Report

09/30/12

Danielle P.

Thank you that makes sense! One more thought... If i have rational function (as you call it)and it has a numerator that can be factored (for example: the numerator is (x^2)-4) and the denominator is already factored out to be (x-2)(x+3), would I simplify it first by factoring the numerator and then cancelling out the x-2 from both the denominator and the numerator leaving me with (x+2)/(X+3)? And then go from there to find the limit?
Report

09/30/12

Jonathan F.

That's a great question!

Ask yourself this are fractions in the form of 0/0 allowed in math? The answer: not at all. You just can't factor a 0 out of the denominator. So in your example the function would still be discontinuous at x=-2.

Now here is a truly interesting question (one your class should be answering in a few days), what would the limit look like as it approached -2? Would it be different than the problem you just worked with?

I do think you have a slight misunderstanding though. The fact that the denominator is factored doesn’t impact the answer in any way. (10-x)/ ((x-2)(x-3)) is discontinuous at 2 and 3, but so is (10-x) /(x2 - 5x – 6)

Report

09/30/12

## Still looking for help? Get the right answer, fast.

Get a free answer to a quick problem.
Most questions answered within 4 hours.

#### OR

Choose an expert and meet online. No packages or subscriptions, pay only for the time you need.


text:
# On the extension of surjective isometries whose domain is the unit sphere of a space of compact operators

25 May 2020  ·  Peralta Antonio M. ·

We prove that every surjective isometry from the unit sphere of the space $K(H),$ of all compact operators on an arbitrary complex Hilbert space $H$, onto the unit sphere of an arbitrary real Banach space $Y$ can be extended to a surjective real linear isometry from $K(H)$ onto $Y$. This is probably the first example of an infinite dimensional non-commutative C$^*$-algebra containing no unitaries and satisfying the Mazur--Ulam property... We also prove that all compact C$^*$-algebras and all weakly compact JB$^*$-triples satisfy the Mazur--Ulam property. read more

PDF Abstract

## Code Add Remove Mark official

No code implementations yet. Submit your code now

## Categories

Functional Analysis Operator Algebras


text:
# 2721. Javanese Cryptoanalysis

Javanese is the language of the people in the Central and Eastern parts of the island of Java, Indonesia.

In 1926, a standard orthography using the English Alphabet was created for the Javanese language. This writing system uses all letters from A to Z. The five letters A, E, I, O, and U are vowels, while all other letters are consonants. In Javanese words vowels and consonants always alternate. This property is quite useful when deciphering encrypted Javanese texts.

A text $s$ consists of words, each word contains only capital letters. Let’s call text $s$ legitimate if in each word of $s$ vowels and consonants alternate (no two vowels and no two consonants are located next to each other).

A simple substitution cipher is applied to a text $s$. That is, a bijection $f : A \rightarrow A$ is chosen, where $A$ is the set of capital letters. The encoded text $t$ is obtained from $s$ by substituting each letter $c$ with $f(c)$.

You’re given the encoded text $t$. Find any legitimate text $s$ that can be encoded as $t$, or detect that there is no such legitimate $s$.

### 输入格式

The input file contains the encoded text $t$, a list of words separated by spaces and/or line breaks. Each word consists only of capital letters (A to Z).

The input file contains no more than $100~000$ characters.

### 输出格式

If the text $t$ cannot be an encoded legitimate text, output only one word impossible.

Otherwise, output any legitimate text $s$ that can be encoded into $t$. Separate words of $s$ with spaces and/or line breaks. All letters in $s$ should be capital.

### 样例

Input
NEERC

Output
impossible

Input
O RISK LIP FOCUS LUCKY

Output
A CODE FOR VALID FILES

7 人解决，11 人已尝试。

148 份提交通过，共有 168 份提交。

5.9 EMB 奖励。


text:
Chapter 53

### INTRODUCTION

Since its introduction in the early 1980s, propofol has been a cornerstone of anesthetic practice. Propofol is an intravenous anesthetic used for the induction and maintenance of general anesthesia and for sedation in and outside of the operating room.

### STRUCTURE AND FORMULATION

The structure of propofol is 2, 6-diisopropylphenol (Figure 53-1). As an alkylphenol derivative, propofol exists as an oil at room temperature. Because it is highly lipophilic and insoluble in aqueous solution, propofol is formulated in a rather complicated 1% (10 mg/mL) lipid solution, containing 10% soybean oil, 2.25% glycerol, 1.2% purified egg phosphatide, and 0.0005% sodium edetate (antimicrobial).

###### FIGURE 53-1

Structure of propofol.

The incidence of anaphylactic reactions to propofol is around 1:20 000, but more common in patients with eczema and/or multiple food allergies. Common clinical practice is to avoid administering propofol to patients with soybean, peanut, and egg allergies due to its formulation with similar products. Despite this “clinical wisdom,” most egg allergies are to egg protein (whites) rather than the egg phosphatide (yolk) that makes up the propofol solution. Avoiding the use of propofol in those with egg allergy may not be warranted.

### PHARMACOKINETICS

Propofol has a very favorable pharmacokinetic profile (Table 53-1). After a single bolus injection, it is quickly redistributed and eliminated. It is rapidly metabolized in the liver by conjugation to glucuronide and sulfate to produce inactive water-soluble compounds that are excreted by the kidneys. Clearance of propofol exceeds liver metabolism, suggesting extra-hepatic metabolism. This fact is confirmed during the anhepatic phase of liver transplant surgery. The kidneys account for roughly 30% of total body clearance. The lungs have also been implicated in propofol metabolism and are responsible for 30% uptake and first-pass metabolism after bolus dose. Propofol exhibits concentration-dependent inhibition of cytochrome P450, specifically CYP 3A4. It may alter metabolism of other drugs that are metabolized by this system, such as opiates and midazolam, which are both often coadministered during induction.

TABLE 53-1Pharmacokinetic Profile for Propofol

Fospropofol (phosphono-O-methyl 0-2, 6-diisopropylphenol) is a prodrug of propofol with a slightly longer time to peak effect and a prolonged effect. Fospropofol undergoes hydrolysis by endothelial cell surface ...

Sign in to your MyAccess profile while you are actively authenticated on this site via your institution (you will be able to verify this by looking at the top right corner of the screen - if you see your institution's name, you are authenticated). Once logged in to your MyAccess profile, you will be able to access your institution's subscription for 90 days from any location. You must be logged in while authenticated at least once every 90 days to maintain this remote access.

Ok

## Subscription Options

### AccessAnesthesiology Full Site: One-Year Subscription

Connect to the full suite of AccessAnesthesiology content and resources including procedural videos, interactive self-assessment, real-life cases, 20+ textbooks, and more


text:
25-29 September 2017
Salamanca, Spain
Europe/Zurich timezone

## Isospin-violation in the extended linear sigma model

26 Sep 2017, 19:00
2h
Auditorium Hall

#### Auditorium Hall

Poster Spectroscopy of mesons

### Speaker

Mrs Nora Weickgenannt

### Description

We study isospin-breaking effects in the extended linear sigma model (eLSM) for $N_f=3$ quark flavors. The eLSM contains scalar, pseudoscalar, vector, and axial-vector mesons, which consist of quarks and antiquarks. It is constructed on the basis of a global chiral $U(N_f)_L \times U(N_f)_R$ symmetry which is spontaneously broken by a quark-antiquark condensate, as well as explicitly broken by the $U(1)_A$ anomaly of quantum chromodynamics and non-vanishing quark masses. Unequal masses for the non-strange and strange quarks lead to a splitting between the vacuum expectation values for the non-strange scalar-isoscalar field $\sigma_N$ and the strange $\sigma_S$. Analogously, unequal masses for the up- and down quarks lead to a non-vanishing vacuum expectation value for the neutral scalar-isotriplet $a_0^0$ field. We explicitly compute the effect of isopin breaking on meson masses within the eLSM.

### Primary authors

Dirk Rischke (University Frankfurt)

### Presentation Materials

There are no materials yet.


text:
+0

Two numbers are independently selected from the set of positive integers less than or equal to 5. What is the probability that the sum of th

0
75
1

Two numbers are independently selected from the set of positive integers less than or equal to 5. What is the probability that the sum of the two numbers is greater than their product? Express your answer as a common fraction.

Sep 26, 2019

#1
+2361
+2

To find the probability, first find all possible cases (note that zero is neither positive or negative)

2 are picked out of 5, so

Using the combination formula : $$\frac{5!}{2!3!}$$

Which is - $$10$$

Now that is the number of possible cases of 2 numbers getting chosen out of 5.

Now lets list all the cases of "the sum of the two numbers is greater than their product" (note that one number can't be chosen twice)

1 and 2

1 and 3

1 and 4

1 and 5

And thats all (4 cases)

2/5

Sep 26, 2019

#1
+2361
+2

To find the probability, first find all possible cases (note that zero is neither positive or negative)

2 are picked out of 5, so

Using the combination formula : $$\frac{5!}{2!3!}$$

Which is - $$10$$

Now that is the number of possible cases of 2 numbers getting chosen out of 5.

Now lets list all the cases of "the sum of the two numbers is greater than their product" (note that one number can't be chosen twice)

1 and 2

1 and 3

1 and 4

1 and 5

And thats all (4 cases)


text:
# Ete transection from the spinoencephalic junction is performed just after 5N transection. Third, element of

Ete transection from the spinoencephalic junction is performed just after 5N transection. Third, element of your response is mediated by descending pathways as suggested by the powerful decrease in EMGs amplitudes for cold stimulations right after spinoencephalic transection, in specimens for which less skin was left on the FL and neck. Fourth, projections descending in the brain are crucial to produce rhythmic, locomotor-like responses from the FL as these responses persisted immediately after 5N sections or skin removal but had been abolished after spinoencephalic transections.May/June 2019, 6(three) e0347-18.Concerning the final point, the effect from the transection could possibly be as a consequence of a basic decrease within the sensory drive impinging on the spinal circuitry creating limb movements or to the section of certain pathways essential to induce rhythmic activity. As for the latter, probably the most probable candidates are reticulospinal projections, which form the bulk of descending projections in newborn opossums (Wang et al., 1992). Additionally, the reticulospinal program is often a critical element with the supraspinal manage of locomotion in vertebrates (for evaluation, see Grillner, 2003; Rossignol et al., 2006; Brownstone and Chopek, 2018). The motor responses obtained following Dibenzyl disulfide Formula stimulation to neutral temperature may possibly seem surprising, but might be attributed to stimulation of skin mechanoreceptors induced by liquid movement. In comparable in vitro preparations of newborn opossums, facial pressures induced triceps muscle contractions (Desmarais et al., 2016). These contractions had been decreased, but not entirely abolished (five on the maximal amplitude), after skin removal, possibly as a result of exposure of totally free nerve endings inside the remaining dermis. The truth that responses to neutral temperature stimulations herein had been nearly abolished by facial skin removal or 5N transections supports this interpretation. Even so, mechanosensation, if involved, most likely explains aspect of the responses to any temperature. By comparison to responses to neutral stimulations, triceps responses following cold stimulations had been on typical four much more frequent, with latencies 300 ms shorter and amplitudes four higher. This clearly supports that cold stimulation solicited cold thermoreceptors additionally to doable mechanosensory components resulting from pressure on the liquid ejection. A study on the coding of temperature by spinal dorsal horn neurons within the adult mouse revealed that the amplitude of responses to cold is correlated to T whereas responses to heat are correlated together with the absolute worth of your target temperature (i.e., warmer stimulating temperatures create huge responses even using a low T Ran et al., 2016). By contrast, in newborn opossums, a deviation from the neutral temperature, either small or large, seems adequate to induce sturdy FL responses to cold. Indeed, with the bath at 25 , stimulations at 21 induced FL movements at rates comparable to stimulations at four (92.five vs 100 ), whilst stimulations at 22 weren’t as efficient to induce FL responses when the bath was at 22 (21.4 4 ). Concerning the responses to hot temperature, our benefits show a relationship with increased temperature but do not permit to distinguish whether responses are far more dependent around the Tor the absolute worth given that stimulations at 34 induced a response price of eight.five when the bath was at 25 ( T9 ) and stimulation at 45 induced response rates of 24.9 7.8 when the bath was at 22 ( T23 ). Having said that, the effect of hot temperature stimulations is com.


text:
angle between the vectors

Printable View

• March 25th 2009, 06:09 PM
oceanmd
angle between the vectors
Please check my work. Thank you.
Find the dot product of the following vectors. Find the angle between the vectors.
v=3i+2j, w=-4i-5j
Dot product v x w=-12-10=-22
cos of angle = -22/sq. root of 13 x sq. root of 41=-0.9529
the angle = 17.64 degrees.

Please tell me where I made a mistake, because when I graph the vectors, the angle looks like it is about 100 degrees.

Thank you very much.
• March 25th 2009, 06:20 PM
skeeter
Quote:

Originally Posted by oceanmd
Please check my work. Thank you.
Find the dot product of the following vectors. Find the angle between the vectors.
v=3i+2j, w=-4i-5j
Dot product v x w=-12-10=-22
cos of angle = -22/sq. root of 13 x sq. root of 41=-0.9529
the angle = 17.64 degrees.

Please tell me where I made a mistake, because when I graph the vectors, the angle looks like it is about 100 degrees.

Thank you very much.

a bit larger than 100 degrees, but it is obtuse ...

$\theta = \arccos(-0.9529) = 162.3^{\circ}$

inverse cosine of a negative value yields a quad II angle.
• March 25th 2009, 06:27 PM
oceanmd
Thank you very much


text:
## anonymous 5 years ago determine all critical points 3x^2-96sqrt(x)

1. anonymous

hey buddies am waiting

2. anonymous

This early in the morning there may not always be someone who can answer a Caclulus question so it may take some time to get an answer. That said, I can help. So, because I won't work the problem for you, let's see if we can figure it out. Do you recall what critical points are?

3. anonymous

yes i do . i know i have to find the max n min values

4. anonymous

Okay, so in general what makes a point a critical point? In other words, how are they defined?

5. anonymous

yes

6. anonymous

So, tell me. How are critical points defined? Understanding that is key to working this problem and we need the definition to proceed to the next step. I'm sorry, but I'm not going to just work the problem for you. I want you to understand how to work these problems in general so you can do them again during, say, an exam.

7. anonymous

ok

8. anonymous

they are thos points in a fuction that the behaviour changes. For instance change in inflection, or moving from max to min or viceversa

9. anonymous

Well, yes and no. Places where a function changes concavity (infection points) are not always critical points. Minimum and maximum points are critical points, but there are also critical points that are not minimum and maximums. So, think of it instead in terms of the function itself. For a general function, say f(x), critical points are defined to be the values of x for which the derivative, f ' (x) is zero or does not exist. So, we need the derivative of your function to find the critical points. What is the derivative of your function?

10. anonymous

ok. makes sense

11. anonymous

i knw how to find the derivative

12. anonymous

Good, so what is the derivative? Or can you do the problem from here?

13. anonymous

well the derivative will be y=6x-48

14. anonymous

if i say thats equal to zero then x=8

15. anonymous

Yes, except your derivative of the second term isn't quite correct. Isn't the derivative of $$\sqrt{x}$$, $\frac{1}{2}x^{-\frac{1}{2}}$ ? That will change your deriviatve and your critical points.

16. anonymous

I SHUD B FINE FROM HERE. thanks

17. anonymous

Okay, glad I could be some help.


text:
# Constructive proof of pigeonhole principle

I'm trying to prove Pigeonhole principle with Coq proof assistant.

Here is how I defined it:

Theorem pigeonhole
:  forall m n : nat, m < n
-> forall f : nat -> nat, (forall i, f i < m)
-> exists i, i < n
-> exists j, j < i /\ f i = f j.

After spending some time on attempts to prove it by induction I found this discussion (https://math.stackexchange.com/a/228604/15013) that suggest it is impossible.

Is it possible (and how) to prove Pigeonhole principle without using contradiction? Using principle of explosion is fine, but excluded middle is not accepted.

• Could you state exactly which pigeonhole principle you mean? There are several principles that could go by that name. – Carl Mummert Aug 27 '14 at 10:34
• Yep, sorry. I added my definition (failed to TeXify it, but hope it is clear as it is). – max taldykin Aug 27 '14 at 10:50
• Another version, actually a generalization, of the pigeonhole principle is "the average of a finite bag (multiset) of numbers $\leq$ its maximum". That may or may not help... – Marnix Klooster Aug 27 '14 at 20:24

Here is a proof that would go through in Bishop's system and similar systems where equality of natural numbers is decidable.

We only need to prove the case $n = m+ 1$, because this implies the general case $n > m$. So we will work with functions from $n = \{0, 1, \ldots, n-1\}$ to $m = n - 1 = \{0, \ldots, m-1\}$.

The proof will be by induction on $n$. The case $n = 1$ is impossible (there is no function from $1$ to $0$) so the base case is $n = 2$. In this case $f(0) = f(1) = 0$ so we're done.

For the inductive case, assume $f$ is a function from $n = m+1$ to $m$ where $m > 1$. We don't have full excluded middle constructively, but we do have constructively that either there is some $i < m$ with $f(i) = f(m)$, or there is not. Speaking formally, we can prove $$(\forall f)(\forall k)(\forall m)[(\exists i < m)[f(i) = k] \lor \lnot (\exists i < m)[f(i) = k]]$$ by induction on $m$, with $f$ and $k$ as parameters.

So, working constructively, we can split into those two cases: either there is some $i < m$ with $f(i) = f(m)$, or there is not. In the first case, we are done already.

In the second case, we make a new function $g$ from $m$ to $m - 1$ so that $g(a) = f(a)$ whenever $f(a) < f(m)$, and $g(a) = f(a) -1$ when $f(a) > f(m)$. This is a sound definition because we have assumed $f(a) \not = f(m)$ for all $a < m$. Now we can apply the inductive hypothesis to $g$ to find $i,j < m$ with $g(i) = g(j)$; then $f(i) = f(j)$ also and we are done.

Here is a guide to prove $$(\forall f)(\forall k)(\forall m)[(\exists i < m)[f(i) = k] \lor \lnot (\exists i < m)[f(i) = k]]$$

The first step is to prove $(\forall x)(\forall y)[x = y \lor x \not = y]$. This is proved by induction on $x$ with $y$ as a parameter.

• For the base case, we prove $(\forall y)[y = 0 \lor y \not = 0]$ from the axioms

1) $0 \not = S(z)$

2) $y = 0 \lor ( \exists z)[y = S(z)]$.

• For the inductive case, we use the additional axiom $x = y \leftrightarrow S(x) = S(y)$.

Once we have the first step, then we can prove the desired formula by induction on $m$ with $k$ and $f$ as parameters.

• The base case is $\lnot (\exists i < 0)[f(i) = k]$.

• For the inductive case, we use the additional axiom $x = S(y) \to z < x \to z < y \lor z = y$ (or we derive this separately).

• Thank you very much. The proof is really easy and straightforward, I even thought about applying inductive hypothesis to some new function but then got distracted and switched to googling for hints. – max taldykin Aug 27 '14 at 11:30
• The facts about decidability follow from induction and the axioms (1) $x \not = S(x)$; (2) $x = 0 \lor (\exists y)[x = S(y)]$; (3) $x = y \leftrightarrow S(x) = S(y)$. – Carl Mummert Aug 27 '14 at 12:01
• (1) should be $0 \not = S(x)$ – Carl Mummert Aug 27 '14 at 12:30
• Thanks for accepting - I assume that means you were able to formalize the proof? I have been thinking for a while about trying to learn Coq. Would you be willing to share the formalized proof with me? If so, could you email me at the address listed in my profile? I would deeply appreciate it. @max taldykin – Carl Mummert Aug 27 '14 at 19:41
• I succeeded formalizing everything except $(\forall f)(\forall k)(\forall m)[(\exists i < m)[f(i) = k] \lor \lnot (\exists i < m)[f(i) = k]]$. It is easy to prove it by classic axiom but I still trying to understand how to prove it by induction. – max taldykin Aug 27 '14 at 19:54


text:
# Entropy has units of energy-per-temperature; what is the impled relation between energy and temperature?

Entropy has units of energy-per-temperature, e.g. $X$ joules per Kelvin. Can this be reduced to a simple English sentence that describes the relationship between those $X$ joules and 1 Kelvin?

For example, when we say that an object's velocity is 10 meters per second north, we mean,

At that instant, if you measure a small enough change in the object's position, and divide by the corresponding change in time, the ratio approaches 10 meters north per second.

In every other SI unit I've encountered that was a ratio of one thing to some other thing, it was always possible to write a sentence like that to connect them.

So, if a system's entropy is 10 joules per Kelvin, how would you complete this sentence:

If you _______________ small amount of energy, and _______________ small change in temperature, the ratio approaches 10 joules per Kelvin.

After all, heat capacity is also measured in joules per Kelvin, and that's much easier to understand: "5 joules per Kelvin means if you apply 5 joules of heat energy to the system you raise the temperature by 1 Kelvin." But I can't figure out a similar understanding of joules per Kelvin for entropy.

• Have you checked Clausius Theorem/Inequality construction? It says that for a reservoir of constant temperature $T$ acting on a system, either if you have a reversible or irreversible process in curse, you can build up that several reversible machines acting between two points in the process "carry" changes $\Delta Q_{rev}$ in reversible heat (summing up in a quasi-static process). Entropy comes as the relation between them, reversible heat by absolute temperature in a given reservoir. And the construction leads to show that this quotient is a thermodynamic variable (coordinate). – chandrasekhar17 Jul 4 '18 at 3:19
• Just to note it, we qualify temperature units like Celsius and Fahrenheit with "degrees" to point out that their zeros aren't at absolute zero. By contrast, temperature units like Kelvin and Rankine have their zeros at absolute zero, such that they're not "degree" units. – Nat Jul 8 '18 at 20:13

The derivative encountered in calculus is the limit of the ratio of two distinct changes which are interdependent. For e.g. for a vehicle, distance travelled $x$ is a function of time $t$, and the derivative $dx/dt$ gives its velocity $v$. But suppose you write this relation as $dx/v=dt$. Now we have a strange quantity $dx/v$, equal to change in time $dt$, which cannot be interpreted as "change of something when something else changes". But the strangeness is only apparent; to make it look natural rewrite the relation as $dx=v~dt$ or $dx/dt=v$.
Same goes for change in entropy, $dS=dQ/T$, in which $Q$ is heat energy, $T$ is temperature, and the heat transfer is reversible. If it feels strange then rewrite it as $dQ=T~dS$ and interpret accordingly. You can't interpret entropy change as "change of something when something else changes" simply because of the way it is defined.
• OK but I still don't understand how to interpret $dS=dQ/T$ in terms of what happens. Are you saying that if I add a small quantity of heat energy $dQ$, then the entropy change in the system will be $dS$, where $dS=dQ/T$ ? – Bennett Jul 4 '18 at 7:46
• @Bennett Yes, that's right. It is like saying, if I move a small distance $dx$ at velocity $v$ then the elapsed time will be $dt=dx/v$. – Deep Jul 4 '18 at 7:55


text:
MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

## Hecke operators acting as correspondences?

This question is inspired by http://mathoverflow.net/questions/19684/relation-between-hecke-operator-and-hecke-algebra

I remember having heard of yet another way of looking at Hecke operators acting on the spaces of modular forms for classical congruence subgroups of $SL_2(\mathbf{Z})$, and I would like to ask if anyone knows a reference for that. Here are some details and a related question.

There is a universal elliptic curve $U$ over $\mathbf{H}$, the upper half-plane. It is an analytic manifold obtained by taking the quotient of $\mathbf{C}\times\mathbf{H}$ by the action of $\mathbf{Z}^2$ given by $(n,m)\cdot (z,\tau)=(z+n+m\tau,\tau)$ where $n,m\in\mathbf{Z},z\in \mathbf{C}$ and $\tau\in\mathbf{H}$.

A torsion free finite index subgroup $\Gamma$ of $SL_2(\mathbf{Z})$ (congruence or not) acts on $U$. Here is the first question: for which $\Gamma$ is the quotient $U/\Gamma$ algebraic?

In any case $U/\Gamma$ is algebraic if $\Gamma=\Gamma(N)=\ker (SL_2(\mathbf{Z})\to SL_2(\mathbf{Z}/N))$ and $N\geq 3$. Denote the corresponding quotient $U/\Gamma(N)$ by $U(N)$. This is the universal elliptic curve with a level $N$ structure. (The notation $U(N)$ may be non-standard, in which case please let me know.)

There is a natural map $U(N)\to Y(N)=\mathbf{H}/\Gamma(N)$. Now take the $n$-th fibered cartesian power $U^n(N)$ of $U(N)$ over $Y(N)$ and let $p:U^n(N)\to Y(N)$ be the projection.

All derived direct images of the constant sheaf under $p$ decompose as direct sums of the Hodge local systems, which correspond to the symmetric powers of the standard representation of $\Gamma(N)$. Using the Eichler-Shimura isomorphism one can construct classes in $H^1(Y(N),V_k)$ from modular forms of weight $k+2$ for $\Gamma(N)$ where $V_k$ is the local system on $Y(N)$ that comes the $k$-th symmetric power of the standard representation. (In fact these classes can be interpreted in terms of the Hodge theory, see http://mathoverflow.net/questions/9599/eichler-shimura-isomorphism-and-mixed-hodge-theory) So modular forms give elements in the $E_2$ sheet of the Leray spectral sequence for $p$.

I would like to ask: can one interpret the Hecke operators acting on modular forms as correspondences acting on $U^n(N)$ over $Y(N)$ (and hence, on the Leray spectral sequence for $p$)?

-

The answer to your last question is yes, modulo my own misunderstandings. In Scholl's "Motives for modular forms", §4, the Hecke operators are defined in this way, and I think the equivalence of these definitions is implied by the diagram (3.16) and proposition 3.18 of Deligne's "Formes modulaires et representations l-adiques".

Let p be a prime not dividing N, and let Y(N,p) be the moduli scheme parametrizing elliptic curves with full level N structure and a choice of a cyclic subgroup C of order p. There are two natural "forgetful" maps q1 and q2 from Y(N,p) to Y(N) -- the former forgets the cyclic subgroup, the latter takes the induced level N structure on the quotient by C.

From these two maps, one gets two different families of elliptic curves over Y(N,p). Explicitly, the pullback of Un(N) along q1 is isomorphic to the n:th fibered power of the universal elliptic curve over Y(N,p); let us denote it Un(N,p). Let Q(N,p) be the quotient of U(N,p) by the cyclic subgroup C, and take its n:th fibered power as well. Then similarly Qn(N,p) is the pullback of Un(N) along q2. Finally, the quotient map gives us $\phi : U^n(N,p) \to Q^n(N,p)$.

But this data gives us the right correspondence on Un(N) over Y(N), namely, one takes the composite $q_{1\ast} \phi^\ast q_2^\ast$ (where I use q1 and q2 also for the induced maps on fibered powers of universal curves).

-
 Thanks, Dan! – algori Jun 3 2010 at 12:12


text:
## Re: proof (mathematical proof?)

Finally!

A very very big thanks to you guys for your help.
It is my first time proving something in math, so it was a very good problem to tackle as it is going to get harder from here...
The teacher don't help too much so it was very fortunate for me to have you explain how to do this right.
Now whats left is for my teacher to check it (and the other problems I solved) and rate it, we'll see how much I get...

Thanks a lot again!


text:
### Q-2, r. 38 - Regulation respecting the quality of the atmosphere

SCHEDULE A
(s. 24)
(Replaced, O.C. 501-2011)
process weight emission standards
rate (tonnes/h) kg/h

0.50 1.3
1.00 2.0
1.50 2.6
2.00 3.2
2.50 3.7
3.00 4.2
3.50 4.6
4.00 5.1
4.50 5.5
5.00 5.9
6.00 6.6
7.00 7.4
8.00 8.1
9.00 8.7
10.0 9.4
12.0 10.6
15.0 12.3
17.0 13.3
20.0 14.9
22.0 15.8
25.0 17.2
27.0 17.5
30.0 18.0
35.0 18.6
40.0 19.1
45.0 19.6
50.0 20.0
60.0 20.8
70.0 21.5
80.0 22.1
90.0 22.6
100 23.0
150 25.0
200 26.4
250 27.5
300 28.4
350 29.2
400 29.9
450 30.6
500 31.1
550 31.6
600 32.1
N.B. The process weight rate is determined by the total weight of all materials introduced into any process for a specified period of time. For the purpose of this Schedule, solid fuels are considered part of the process, but liquid and gaseous fuels and combustion air are not.
Interpolation of the data in this Schedule for process weight rates under 25t/h shall be accomplished by use of the equation E = 2,0p0.67 and interpolation and extrapolation of the data for process weight rates equal to or in excess of 25 t/h shall be accomplished by use of the equation E = 25,0p0.11--18, where E is the emission standard in kg/h and P is the process weight rate in t/h.
In the case of discontinuous operation of the process, the rate is calculated by dividing the total process weight rate by the number of hours of complete operations, less the time during which the equipment was not in operation. The process weight rate per hour is then calculated by dividing the process weight rate for a typical period of time by the number of hours of such period.
R.R.Q., 1981, c. Q-2, r. 20, Sch. A; O.C. 501-2011, s. 215.