scholarly journals On the Taylor expansion of $\lambda$-terms and the groupoid structure of their rigid approximants

2022 ◽  
Vol Volume 18, Issue 1 ◽  
Author(s):  
Federico Olimpieri ◽  
Lionel Vaux Auclair
Keyword(s):  
Normal Form ◽  
Taylor Expansion ◽  
Ad Hoc ◽  
Abstract Machine ◽  
Original Proof ◽  
Reduction Strategy ◽  
Uniformity Property

We show that the normal form of the Taylor expansion of a $\lambda$-term is isomorphic to its B\"ohm tree, improving Ehrhard and Regnier's original proof along three independent directions. First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad hoc. We also introduce a groupoid of permutations of copies of arguments in a rigid variant of the resource calculus, and relate the coefficients of Taylor expansion with this structure, while Ehrhard and Regnier worked with groups of permutations of occurrences of variables. Finally, we extend all the results to a nondeterministic setting: by contrast with previous attempts, we show that the uniformity property that was crucial in Ehrhard and Regnier's approach can be preserved in this setting.

The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus

2019 ◽  
Vol 29 ◽  
Author(s):  
ÁLVARO GARCÍA-PÉREZ ◽  
PABLO NOGUEIRA
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Order Reduction ◽  
Normal Order ◽  
Abstract Machine ◽  
Reduction Strategy ◽  
Structural Operational Semantics ◽  
Standard Normal ◽  
De Bruijn ◽  
De Bruijn Indices

AbstractWe exploit the idea of proving properties of an abstract machine by using a corresponding semantic artefact better suited to their proof. The abstract machine is an improved version of Pierre Crégut’s full-reducing Krivine machine KN. The original version works with closed terms of the pure lambda calculus with de Bruijn indices. The improved version reduces in similar fashion but works on closures where terms may be open. The corresponding semantic artefact is a structural operational semantics of a calculus of closures whose reduction relation is purposely a reduction strategy. As shown in previous work, improved KN and the structural operational semantics ‘correspond’, i.e. both artefacts realise the same reduction strategy. In this paper, we prove in the calculus of closures that the reduction strategy simulates in lockstep (at every reduction step) the complete and standard normal-order strategy (i.e. leftmost reduction to normal form) of the pure lambda calculus. The simulation is witnessed by a substitution function from closures of the closure calculus to pure terms of the pure lambda calculus. Thus, KN also simulates normal-order in lockstep by the correspondence. This result is stronger than the known proof that KN is complete, for in the pure lambda calculus there are complete but non-standard strategies. The lockstep simulation proof consists of straightforward structural inductions, thanks to three properties of the closure calculus we call ‘index alignment’, ‘parameters-as-levels’ and ‘balanced derivations’. The first two come from KN. Thanks to these properties, a proof in a calculus of closures involving de Bruijn indices and de Bruijn levels is unproblematic. There is no lexical adjustment at binding lookup, on-the-fly alpha-conversion or recursive traversals of the term to deal with bound and free variables as in other calculi. This paper contributes to the framework for environment machines of Biernacka and Danvy a full-reducing open-terms closure calculus, its corresponding abstract machine, and a lockstep simulation proof via a substitution function.

scholarly journals Two-Parameters Bifurcation in Quasilinear Dierential-Algebraic Equations

2016 ◽  
Vol 12 (1) ◽  
pp. 5786-5796
Author(s):  
Kamal H Yasir ◽  
Abbas M Al_husenawe
Keyword(s):  
Normal Form ◽  
Basic Principle ◽  
Bifurcation Theory ◽  
Taylor Expansion ◽  
Pitchfork Bifurcation ◽  
Algebraic Equations ◽  
Saddle Node ◽  
Two Parameters

In this paper, bifurcation of solution of guasilinear dierential-algebraic equations (DAEs) is studied. Whereas basic principle that quasilinear DAE is eventually reducible to an ordinary dierential equation (ODEs) and that this reduction so we can apply the classical bifurcation theory of the (ODEs). The taylor expansion applied to the reduced DAEs to prove that is equivalent to an ODE which is a normal form under some non-degeneracy conditions theorems given in this work deal with the saddle node,transcritical and pitchfork bifurcation with two-parameters. Some illustrated examples are given to explain the idea of the paper.

scholarly journals Asymptotically Optimal Box Packing Theorems

10.37236/802 ◽  
2008 ◽  
Vol 15 (1) ◽  
Author(s):  
Michael Reid
Keyword(s):  
Algebraic Geometry ◽  
Ad Hoc ◽  
Necessary Conditions ◽  
Combinatorial Proof ◽  
Original Proof ◽  
Asymptotically Optimal ◽  
Straightforward Calculation ◽  
Complete Answer ◽  
Special Case

Given a protoset of $d$-dimensional polyominoes, we ask which boxes can be packed by the protoset. In some cases, it may be too difficult to give a complete answer to this question, so we ask the easier question about determining all sufficiently large boxes that can be packed. (We say that a box is "sufficiently large" if all edge lengths are ${} \ge C$ for some large $C$.) We give numerous examples (mostly $2$-dimensional) where we can answer this easier question. The various techniques involved are: checkerboard-type colorings/numberings (tile homology), the boundary word method of Conway and Lagarias (tile homotopy), ad hoc geometric arguments, and a very nice theorem of Barnes. Barnes' Theorem asserts that all necessary conditions for a box to be packable can be given in a certain form, and these conditions are also sufficient for large boxes. Barnes' Theorem has not received the appreciation it deserves. We give a new, purely combinatorial proof of this important result. (Barnes' original proof uses techniques of algebraic geometry.) In the special case that all the prototiles are boxes themselves, we show how to determine all sufficiently large boxes that they pack. We prove a theorem based on Barnes' result that reduces this to a straightforward calculation.

scholarly journals Equivariant decomposition of polynomial vector fields

2020 ◽  
pp. 2050083
Author(s):  
Fahimeh Mokhtari ◽  
Jan A. Sanders
Keyword(s):  
Normal Form ◽  
Vector Fields ◽  
Systematic Approach ◽  
Ad Hoc ◽  
Linear Part ◽  
Polynomial Vector ◽  
Polynomial Vector Fields ◽  
Explicit Formulas ◽  
Structure Constants ◽  
2D And 3D

To compute the unique formal normal form of families of vector fields with nilpotent linear part, we choose a basis of the Lie algebra consisting of orbits under the action of the nilpotent linear part. This creates a new problem: to find explicit formulas for the structure constants in this new basis. These are well known in the 2D case, and recently expressions were found for the 3D case by ad hoc methods. The goal of the this paper is to formulate a systematic approach to this calculation. We propose to do this using a rational method for the inversion of the Clebsch–Gordan coefficients. We illustrate the method on a family of 3D vector fields and compute the unique formal normal form for the Euler family both in the 2D and 3D cases, followed by an application to the computation of the unique normal form of the Rössler equation.

Minimal forms inλ-cakulus computations

1980 ◽  
Vol 45 (1) ◽  
pp. 165-171 ◽  
Author(s):  
Corrado Böhm ◽  
Silvio Micali
Keyword(s):  
Normal Form ◽  
Reduction Strategy ◽  
Computational Environment ◽  
Minimal Form ◽  
Generic Term

AbstractThe notion of a minimal form is defined as an extension of the notion of a normal form inλ-β-calculus and its meaning is discussed in a computational environment. The features of the Knuth-Gross reduction strategy are used to prove that to possess a minimal form, for a generic term, is a semidecidable predicate.

Truncation criteria and algorithm for the reduction to normal form of catastrophe unfoldings - I. Singularities with zero rank

1989 ◽  
Vol 424 (1867) ◽  
pp. 327-342 ◽  
Keyword(s):  
Normal Form ◽  
Taylor Series ◽  
Finite Subset ◽  
Catastrophe Theory ◽  
Taylor Expansion ◽  
Normal Forms ◽  
Finite Degree ◽  
Equivalence Transformations ◽  
Right Equivalence

Applications of elementary catastrophe theory often require the determination of right-equivalence transformations which reduce unfold­ings of singularities to their associated normal forms. In general these transformations can only be found approximately, such as in the form of truncated Taylor series. It is shown that the reduction to normal form of an unfolding, to a given finite degree in the control variables, is determined by a finite subset of terms in its multivariate Taylor expansion. An algorithm to construct the transformation that effects the reduction to normal form of an unfolding is presented.

Closing the GAP—A 5Å Scanning Microscope

1969 ◽  
Vol 27 ◽  
pp. 6-7
Author(s):  
A. V. Crewe
Keyword(s):  
Normal Form ◽  
The Other ◽  
Resolving Power ◽  
Scanning Microscope ◽  
Conventional Microscope ◽  
Other Hand ◽  
Closing The Gap ◽  
Thermal Sources ◽  
Better Than ◽  
Transmission Microscope

We have become accustomed to differentiating between the scanning microscope and the conventional transmission microscope according to the resolving power which the two instruments offer. The conventional microscope is capable of a point resolution of a few angstroms and line resolutions of periodic objects of about 1Å. On the other hand, the scanning microscope, in its normal form, is not ordinarily capable of a point resolution better than 100Å. Upon examining reasons for the 100Å limitation, it becomes clear that this is based more on tradition than reason, and in particular, it is a condition imposed upon the microscope by adherence to thermal sources of electrons.

Sign in / Sign up

Export Citation Format

Share Document