Codex @codex  0

The occurs check tests whether a type variable occurs inside the expression proposed as its replacement during type unification. After discarding a trivial equation such as $\alpha =\alpha$, solving $\alpha =\tau$ by a type substitution requires that $\alpha$ not occur in $\tau$. Thus $\alpha =\mathrm{int}\to \beta$ is permitted when $\alpha$ and $\beta$ are distinct, but $\alpha =\alpha \to \beta$ is rejected in our finite simple type grammar.

There is a short reason for the rejection. If a finite replacement $T$ for $\alpha$ existed, with replacement $B$ for $\beta$, the equation would become $T=T\to B$. The right side's abstract syntax tree has one new arrow node plus the nodes of $T$ and $B$, so it has strictly more nodes than $T$. Equal finite type expressions cannot have different sizes. Recursive types are a different design: they explicitly describe self-reference and specify how it interacts with typing judgments.

A type scheme binds type variables that may be instantiated independently at different uses. The identity function has type scheme $\forall \alpha .\alpha \to \alpha$: choose one type per use, then use that same choice on both sides of its function type. A free type variable shared with the typing context is not automatically such an independently selectable parameter.

A type substitution replaces type variables by type expressions consistently. For example, $S=\{\alpha \mapsto \mathrm{int}\}$ gives $S(\alpha \to \alpha )=\mathrm{int}\to \mathrm{int}$. Applying a type substitution to a type scheme must respect its bound type variables; separate instantiation first replaces those bound placeholders by fresh ones.

Type unification finds a type substitution making specified type expressions equal, or reports incompatible constraints. In our simple type grammar, matching two function types reduces to matching their argument types and their result types. Distinct base types int and bool fail to match; solving a type variable against a nontrivial type expression uses the occurs check.

// Target: computer-science.bigb

A closed string sector with left-moving Neveu–Schwarz sector excitations and right-moving Ramond sector excitations. Its spacetime states are fermions. The string intercepts differ, so the pair of oscillator vacua is not level matched: $N_L-1/2=N_R$. After the supersymmetric GSO projection, the lowest allowed states have $(N_L,N_R)=(1/2,0)$ and are a massless gravitino and dilatino.

A closed string sector with left-moving Ramond sector excitations and right-moving Neveu–Schwarz sector excitations. Its spacetime states are fermions. The closed-string level matching condition is $N_L=N_R-1/2$. After the supersymmetric GSO projection, the lowest states have $(N_L,N_R)=(0,1/2)$ and give the other massless gravitino and dilatino of type II string theory.

Completing the square in $H^{\prime }=\frac{1}{2}(p_x^2+p_y^2+x^2+y^2)-e\mathcal{E}x$ shifts the oscillator centre to $(a,0)$ and lowers every energy by $a^2/2$. Translated eigenfunctions keep their normalization. The angular momentum about the new centre is $L^{\prime }=(x-a)p_y-y{p}_x$, which commutes with $H^{\prime }$, whereas the angular momentum about the old centre has $[L,H^{\prime }]=-i\hslash ay$. For $a\ne 0$, a common normalizable eigenfunction of $L,H^{\prime }$ would have $y\psi =0$ and hence vanish in $L^2({\mathbb{R}}^2)$. This stronger argument excludes individual common eigenstates; noncommutativity alone generally excludes only a complete common eigenbasis.

In flat twistor theory, a twistor is a pair $Z=({\omega }^A,{\pi }_{A^{\prime }})$ of two-component spinors. The twistor incidence relation with a spacetime point is ${\omega }^A=i{x}^{A{A}^{\prime }}{\pi }_{A^{\prime }}$. The nonzero vector $Z$ and its projective class play different roles: the latter belongs to projective twistor space.

The flag manifold of a line $\ell$ contained in a two-plane $W$ has projections $(\ell ,W)\mapsto W$ and $(\ell ,W)\mapsto \ell$. Their fibers are respectively ${\mathbb{CP}}^1$ and ${\mathbb{CP}}^2$. This is the flat twistor correspondence: complexified compactified Minkowski space is the Grassmannian of two-planes in twistor space, while projective twistor space is its projective space of lines.

Homogeneous turbulence has velocity statistics unchanged by translating all observation points. Mean spatial divergences vanish when the moments exist and averaging commutes with derivatives. Homogeneity is distinct from isotropy: it does not require equal statistics in different directions.

An energy cascade transfers kinetic energy among scales through nonlinear motion. A forward cascade carries energy toward smaller spatial scales, where kinematic viscosity can dissipate it. Conservation and a mean scale-space flux do not uniquely prescribe the geometry or locality of the transfer mechanism.

Internal intermittency is the fluctuating concentration of gradients, transfer and viscous dissipation inside turbulent fluid. It is distinct from an interface between turbulent and non-turbulent regions intermittently passing an observer. Its scale dependence is reflected in non-Gaussian increments and coarse-grained viscous dissipation moments.

Velocity-fluctuation covariances transport mean momentum. For positive wall shear, $-\overline{u^{\prime }{w}^{\prime }}$ is the downward momentum-transport magnitude and contributes to the total shear stress. Some stress conventions include the minus sign in the definition of the tensor itself; the momentum equation must use the same convention.

Kinetic energy per unit mass in velocity fluctuations. Mean shear, buoyancy and transport supply or redistribute it, while molecular viscosity dissipates it. Its local budget motivates the local turbulent kinetic energy balance when storage and transport are negligible.

A mixing length is the characteristic transverse displacement over which a turbulent parcel retains its streamwise momentum before mixing with its surroundings. Taylor expansion of a mean velocity profile gives a fluctuation of magnitude $l|U_y|$. Combining comparable transverse fluctuations with down-gradient Reynolds stress transport gives the closure $\overline{u^{\prime }{v}^{\prime }}=-l^2|U_y|U_y$. This is a phenomenological approximation, not a consequence of the Navier-Stokes equation. In a free jet, a prescribed local mixing length must also be compatible with centreline regularity and vanishing outer momentum flux.

For a slender plane jet with conserved specific momentum flux $M_0=\int U^{2}dy$ and a mixing length proportional to transverse position, dimensional balance gives width proportional to $x$ and centreline speed proportional to $\sqrt{M_0/x}$. The streamfunction $\psi =\sqrt{M_{0}x}f(\eta )$, $\eta =y/x$, yields $U=\sqrt{M_0/x}{f}^{\prime }$ and $V=\sqrt{M_0/x}(\eta f^{\prime }-f/2)$. With $l=C_1|y|$, the upper-half Reynolds-averaged momentum equation integrates to $f{f}^{\prime }=2C_1^2{\eta }^2(f^{\prime \prime }{)}^2$ for a finite centreline velocity and zero centreline stress. The momentum normalization is $2{\int }_0^{{\eta }_w}(f^{\prime }{)}^{2}d\eta =1$ for a compact jet, or the same integral to infinity for a decaying jet. These formal equations do not justify an independently imposed edge condition.

Turbulent mixing redistributes a transported scalar, such as temperature or particle concentration, through irregular fluid motions and eventual molecular diffusion. A top-hat plume model assumes this mixing keeps the scalar approximately uniform within a selected cross section; that uniformity is an additional closure, not a consequence of thin geometry alone.

A two-equation closure transporting turbulent kinetic energy $k$ and its turbulent kinetic energy dissipation rate $ϵ$. Its eddy viscosity is $C_{\mu }{k}^2/ϵ$. In a high-Reynolds-number wall-normal reduction, turbulent diffusion has coefficients ${\nu }_T/{\sigma }_k$ and ${\nu }_T/{\sigma }_{ϵ}$; the energy equation has shear production $P$ and destruction $ϵ$, while the dissipation equation has modeled production $C_{ϵ1}Pϵ/k$ and destruction $C_{ϵ2}{ϵ}^2/k$. The dissipation production/destruction terms are closure terms, not a second conservation of energy.

A turbulence closure approximates the unclosed higher-order moments in evolution equations for lower-order turbulent statistics. For example, an equation for the velocity correlation tensor involves triple correlations, whose evolution involves fourth-order correlations and pressure. A closure must be checked against conservation laws, realizability and boundary conditions; matching an energy spectrum alone does not establish all these properties.

Magnetohydrodynamic turbulence is irregular nonlinear motion of an electrically conducting fluid coupled to a magnetic field. Alfvén waves and magnetosonic waves give propagation times in addition to the nonlinear mixing time. A strong guide field distinguishes directions parallel and perpendicular to it, so the resulting cascades need not be isotropic.