Dissipative Chaos in Semiconductor Superlattices

We consider the motion of ballistic electrons in a miniband of a semiconductor superlattice (SSL) under the influence of an external, time-periodic electric field. We use the semi-classical balance-equation approach which incorporates elastic and inelastic scattering (as dissipation) and the self-consistent field generated by the electron motion. The coupling of electrons in the miniband to the self-consistent field produces a cooperative nonlinear oscillatory mode which, when interacting with the oscillatory external field and the intrinsic Bloch-type oscillatory mode, can lead to complicated dynamics, including dissipative chaos. For a range of values of the dissipation parameters we determine the regions in the amplitude-frequency plane of the external field in which chaos can occur. Our results suggest that for terahertz external fields of the amplitudes achieved by present-day free electron lasers, chaos may be observable in SSLs. We clarify the nature of this novel nonlinear dynamics in the superlattice-external field system by exploring analogies to the Dicke model of an ensemble of two-level atoms coupled with a resonant cavity field and to Josephson junctions.

Typability and Type Checking in the Second-Order Λ-Calculus Are Equivalent and Undecidable (Preliminary Draft)

We consider the problems of typability[1] and type checking[2] in the Girard/Reynolds second-order polymorphic typed λ-calculus, for which we use the short name "System F" and which we use in the "Curry style" where types are assigned to pure λ -terms. These problems have been considered and proven to be decidable or undecidable for various restrictions and extensions of System F and other related systems, and lower-bound complexity results for System F have been achieved, but they have remained "embarrassing open problems"[3] for System F itself. We first prove that type checking in System F is undecidable by a reduction from semi-unification. We then prove typability in System F is undecidable by a reduction from type checking. Since the reverse reduction is already known, this implies the two problems are equivalent. The second reduction uses a novel method of constructing λ-terms such that in all type derivations, specific bound variables must always be assigned a specific type. Using this technique, we can require that specific subterms must be typable using a specific, fixed type assignment in order for the entire term to be typable at all. Any desired type assignment may be simulated. We develop this method, which we call "constants for free", for both the λK and λI calculi.