Open Access

The goal of this report is to prove correctness of a considerable subset of transformations w.r.t. contextual equivalence in an extended lambda-calculus LS with case, constructors, seq, let, and choice, with a simple set of reduction rules; and to argue that an approximation calculus LA is equivalent to LS w.r.t. the contextual preorder, which enables the proof tool of simulation. Unfortunately, a direct proof appears to be impossible. The correctness proof is by defining another calculus L comprising the complex variants of copy, case-reduction and seq-reductions that use variable-binding chains. This complex calculus has well-behaved diagrams and allows a proof of correctness of transformations, and that the simple calculus LS, the calculus L, and the calculus LA all have an equivalent contextual preorder.

Fragestellung: Es existiert eine Vielzahl von Begriffen für Verhaltenssüchte, die Mängel in Operationalisierung, Bezug zum Verhalten, Kompatibilität mit internationalen Klassifikationen sowie nicht stigmatisierender Nutzung aufweisen. Daher werden einheitliche Begriffe für Verhaltenssüchte benötigt. Methode: Im Rahmen einer Leitlinie zur Diagnostik und Behandlung Internetbezogener Störungen wurden Lösungen in Form eines Expertenkonsens entwickelt. Ergebnisse: Als Grundlage wurde die Einteilung von Verhaltenssüchten in der 11. Revision der International Classification of Diseases (ICD-11) genutzt. Es wurden die Begriffe Computerspielstörung (CSS) und Glücksspielstörung (GSS) für die beiden in ICD-11 enthaltenen Verhaltenssüchte gewählt sowie drei weitere spezifizierte Verhaltenssüchte vorgeschlagen: Soziale-Netzwerke-Nutzungsstörung (SNS), Shoppingstörung (ShS) und Pornografie-Nutzungsstörung (PNS). Für CSS, GSS und ShS wird weiterhin zwischen vorwiegend online oder vorwiegend offline unterschieden. Als Oberbegriff wird Störungen aufgrund von Verhaltenssüchten vorgeschlagen. Für Störungen aufgrund von Verhaltenssüchten, die sich vorwiegend auf online ausgeübte Verhaltensweisen beziehen, kann alternativ der Oberbegriff Internetnutzungsstörungen verwendet werden. Schlussfolgerung: Die vorgeschlagenen Termini weisen Verbesserungen im Vergleich zu uneindeutigen oder aus anderen Gründen ungünstigen Begriffen dar. Gleichzeitig konnte eine Kompatibilität mit der ICD-11 ermöglicht werden.

In this dissertation a non-deterministic lambda-calculus with call-by-need evaluation is treated. Call-by-need means that subexpressions are evaluated at most once and only if their value must be known to compute the overall result. Also called "sharing", this technique is inevitable for an efficient implementation. In the lambda-ND calculus of chapter 3 sharing is represented explicitely by a let-construct. Above, the calculus has function application, lambda abstractions, sequential evaluation and pick for non-deterministic choice. Non-deterministic lambda calculi play a major role as a theoretical foundation for concurrent processes or side-effected input/output. In this work, non-determinism additionally makes visible when sharing is broken. Based on the bisimulation method this work develops a notion of equality which respects sharing. Using bisimulation to establish contextual equivalence requires substitutivity within contexts, i.e., the ability to "replace equals by equals" within every program or term. This property is called congruence or precongruence if it applies to a preorder. The open similarity of chapter 4 represents a new concept, insofar that the usual definition of a bisimulation is impossible in the lambda-ND calculus. So in section 3.2 a further calculus lambda-Approx has to be defined. Section 3.3 contains the proof of the so-called Approximation Theorem which states that the evaluation in lambda-ND and lambda-Approx agrees. The foundation for the non-trivial precongruence proof is set out in chapter 2 where the trailblazing method of Howe is extended to be capable with sharing. By the use of this (extended) method, the Precongruence Theorem proves open similarity to be a precongruence, involving the so-called precongruence candidate relation. Joining with the Approximation Theorem we obtain the Main Theorem which says that open similarity of the lambda-Approx calculus is contained within the contextual preorder of the lambda-ND calculus. However, this inclusion is strict, a property whose non-trivial proof involves the notion of syntactic continuity. Finally, chapter 6 discusses possible extensions of the base calculus such as recursive bindings or case and constructors. As a fundamental study the calculus lambda-ND provides neither of these concepts, since it was intentionally designed to keep the proofs as simple as possible. Section 6.1 illustrates that the addition case and constructors could be accomplished without big hurdles. However, recursive bindings cannot be represented simply by a fixed point combinator like Y, thus further investigations are necessary.

Extending the method of Howe, we establish a large class of untyped higher-order calculi, in particular such with call-by-need evaluation, where similarity, also called applicative simulation, can be used as a proof tool for showing contextual preorder. The paper also demonstrates that Mann’s approach using an intermediate “approximation” calculus scales up well from a basic call-by-need non-deterministic lambdacalculus to more expressive lambda calculi. I.e., it is demonstrated, that after transferring the contextual preorder of a non-deterministic call-byneed lambda calculus to its corresponding approximation calculus, it is possible to apply Howe’s method to show that similarity is a precongruence. The transfer is not treated in this paper. The paper also proposes an optimization of the similarity-test by cutting off redundant computations. Our results also applies to deterministic or non-deterministic call-by-value lambda-calculi, and improves upon previous work insofar as it is proved that only closed values are required as arguments for similaritytesting instead of all closed expressions.

Fission fragment mass distributions were measured in heavy-ion induced fissions using 238U target nucleus. The measured mass distributions changed drastically with incident energy. The results are explained by a change of the ratio between fusion and qasifission with nuclear orientation. A calculation based on a fluctuation dissipation model reproduced the mass distributions and their incident energy dependence. Fusion probability was determined in the analysis, and the values were consistent with those determined from the evaporation residue cross sections.