scholarly journals Polyprograms and Polyprogram Bisimulation

2018 ◽  
Vol 25 (5) ◽  
pp. 534-548
Author(s):  
Sergei Grechanik
Keyword(s):  
Denotational Semantics ◽  
Weak Form ◽  
Functional Language ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
First Order ◽  
Single Function ◽  
The Difference ◽  
Two Phases ◽  
Transformation Systems

A polyprogram is a generalization of a program which admits multiple definitions of a single function. Such objects arise in different transformation systems, such as the Burstall-Darlington framework or equality saturation. In this paper, we introduce the notion of a polyprogram in a non-strict first-order functional language. We define denotational semantics for polyprograms and describe some possible transformations of polyprograms, namely we present several main transformations in two different styles: in the style of the Burstall-Darlington framework and in the style of equality saturation. Transformations in the style of equality saturation are performed on polyprograms in decomposed form, where the difference between functions and expressions is blurred, and so is the difference between substitution and unfolding. Decomposed polyprograms are well suited for implementation and reasoning, although they are not very human-readable. We also introduce the notion of polyprogram bisimulation which enables a powerful transformation called merging by bisimulation, corresponding to proving equivalence of functions by induction or coinduction. Polyprogram bisimulation is a concept inspired by bisimulation of labelled transition systems, but yet it is quite different, because polyprogram bisimulation treats every definition as self-sufficient, that is a function is considered to be defined by any of its definitions, whereas in an LTS the behaviour of a state is defined by all transitions from this state. We present an algorithm for enumerating polyprogram bisimulations of a certain form. The algorithm consists of two phases: enumerating prebisimulations and converting them to proper bisimulations. This separation is required because polyprogram bisimulations take into account the possibility of parameter permutation. We prove correctness of this algorithm and formulate a certain weak form of its completeness. The article is published in the author’s wording.

Semantical proofs of correctness for programs performing non-deterministic tests on real numbers

2010 ◽  
Vol 20 (5) ◽  
pp. 723-751
Author(s):  
THOMAS ANBERRÉE
Keyword(s):  
Real Number ◽  
Denotational Semantics ◽  
Functional Language ◽  
Real Numbers ◽  
First Order

We consider a functional language that performs non-deterministic tests on real numbers and define a denotational semantics for that language based on Smyth powerdomains. The semantics is only an approximate one because the denotation of a program for a real number may not be precise enough to tell which real number the program computes. However, for many first-order total functions f : n → , there exists a program for f whose denotation is precise enough to show that the program indeed computes the function f. In practice, it is not difficult to find programs like this that possess a faithful denotation. We provide a few examples of such programs and the corresponding proofs of correctness.

scholarly journals A Denotational Investigation of Defunctionalization

2000 ◽  
Vol 7 (47) ◽  
Author(s):  
Lasse R. Nielsen
Keyword(s):  
Data Structures ◽  
Program Transformation ◽  
Denotational Semantics ◽  
Higher Order ◽  
Functional Language ◽  
First Order

<p>Defunctionalization was introduced by John Reynolds in his 1972<br />article Definitional Interpreters for Higher-Order Programming <br />Languages. Defunctionalization transforms a higher-order program into a first-order one, representing functional values as data structures. Since then it has been used quite widely, but we observe that it has never been proven correct. We formalize defunctionalization denotationally for a typed functional language, and we prove that it preserves the meaning of any terminating program. Our proof uses logical relations.</p><p>Keywords: defunctionalization, program transformation, denotational semantics, logical relations.</p>

scholarly journals On the Finitary Bisimulation

1995 ◽  
Vol 2 (59) ◽  
Author(s):  
Luca Aceto ◽  
Anna Ingólfsdóttir
Keyword(s):  
Denotational Semantics ◽  
Subject Classification ◽  
Process Algebras ◽  
Transition Systems ◽  
Behavioural Observation ◽  
Labelled Transition Systems ◽  
Full Abstraction ◽  
Ams Subject Classification ◽  
Keywords And Phrases

<p>The finitely observable, or finitary, part of bisimulation is a key tool in establishing full abstraction results for denotational semantics for process algebras with respect to bisimulation-based preorders. A bisimulation-like characterization of this relation for arbitrary transition systems is given, relying on Abramsky's characterization in terms of the finitary domain logic. More informative behavioural, observation-independent characterizations of the finitary bisimulation are also offered for several interesting classes of transition systems. These include transition systems with countable action sets, those that have bounded convergent sort and the sort-finite ones. The result for sort-finite transition systems sharpens a previous behavioural characterization of the finitary bisimulation for this class of structures given by Abramsky.</p><p><br />AMS Subject Classification (1991): 68Q10 (Modes of computation), 68Q55<br />(Semantics), 03B70 (Logic of Programming), 68Q90 (Transition nets).<br />Keywords and Phrases: Concurrency, labelled transition systems with divergence,<br />bisimulation preorder, finitary relations, domain logic for transition systems.</p>

Kinetics in Heterogeneous Systems

2007 ◽  
Author(s):  
Robert B. Jordan
Keyword(s):  
Liquid Phase ◽  
Mass Transport ◽  
Rate Constant ◽  
Heterogeneous Systems ◽  
Two Phase ◽  
First Order ◽  
Liquid Phases ◽  
Liquid Systems ◽  
The Difference ◽  
Two Phases

In this Chapter, a heterogeneous system is one in which the reactants are present in at least two phases. The discussion will concentrate on two such conditions, two-phase gas/liquid systems and three-phase gas/liquid/solid systems. Chemists tend to favor homogeneous conditions, with the reactants all in one phase, because they provide more controlled and reproducible conditions. However, heterogeneous conditions are often preferred in industrial processes because of the ease of separating the catalyst from the products. In many mechanistic studies, heterogeneity adds a complicating feature to be avoided, but there are times when this cannot be done, or when it happens unexpectedly. In gas/liquid systems, the gas often has limited solubility in the liquid which contains the other reagents. As a consequence, there can be problems of mass transport of the gaseous reactant from the gas to the liquid phase. Mass transport can limit the concentration of the gas in the liquid and/or become a rate-limiting feature of the system. These features can confuse interpretations of product distributions and rate laws. The gas/liquid/solid systems generally involve reactants in the gas and liquid phases and a catalyst as the solid phase. In some cases, the solid may be produced from initially homogeneous conditions, and a question arises as to whether the real catalyst is the original species added or the solid product formed under the reaction conditions. There are further questions about the factors that may control the rate of the catalytic process. In the chemistry laboratory, these systems are most often encountered with the gases H2 or CO reacting with substrate and possibly a catalyst in the liquid phase. For the mechanistic interpretation of kinetic observations, an important factor is the rate of mass transfer of the gas to the liquid phase. The rate of gas absorption into the liquid is typically represented as a first order process, driven by the difference between the saturated gas concentration [G(I)]f and the concentration at any time [G(I)], as given by where kLA is an effective first-order rate constant. This constant is taken as a product of an inherent absorption rate constant, kL, and something related to the surface area of the liquid phase, A.

scholarly journals Shock Structure and Relaxation in the Multi-Component Mixture of Euler Fluids

Symmetry ◽  
2021 ◽  
Vol 13 (6) ◽  
pp. 955
Author(s):  
Damir Madjarević ◽  
Milana Pavić-Čolić ◽  
Srboljub Simić
Keyword(s):  
Relaxation Times ◽  
Thermal Relaxation ◽  
Collision Operator ◽  
Weak Form ◽  
Shock Structure ◽  
Theory Approach ◽  
Component Mixture ◽  
Single Temperature ◽  
The Difference ◽  
Euler Fluids

The shock structure problem is studied for a multi-component mixture of Euler fluids described by the hyperbolic system of balance laws. The model is developed in the framework of extended thermodynamics. Thanks to the equivalence with the kinetic theory approach, phenomenological coefficients are computed from the linearized weak form of the collision operator. Shock structure is analyzed for a three-component mixture of polyatomic gases, and for various combinations of parameters of the model (Mach number, equilibrium concentrations and molecular mass ratios). The analysis revealed that three-component mixtures possess distinguishing features different from the binary ones, and that certain behavior may be attributed to polyatomic structure of the constituents. The multi-temperature model is compared with a single-temperature one, and the difference between the mean temperatures of the mixture are computed. Mechanical and thermal relaxation times are computed along the shock profiles, and revealed that the thermal ones are smaller in the case discussed in this study.

scholarly journals A fully abstract semantics for a first-order functional language with logic variables

1991 ◽  
Vol 13 (4) ◽  
pp. 577-625 ◽  
Author(s):  
Radha Jagadeesan ◽  
Keshav Pingali ◽  
Prakash Panangaden
Keyword(s):  
Functional Language ◽  
First Order ◽  
Abstract Semantics

scholarly journals Rapid compressions in a captive bubble apparatus are isothermal

2003 ◽  
Vol 95 (5) ◽  
pp. 1896-1900
Author(s):  
Wenfei Yan ◽  
Stephen B. Hall
Keyword(s):  
Hydrostatic Pressure ◽  
Gas Phase ◽  
Pulmonary Surfactant ◽  
First Order ◽  
First Order Kinetics ◽  
Gas Phase Molecules ◽  
Actual Change ◽  
Phase Temperature ◽  
Two Phases ◽  
Interfacial Films

Captive bubbles are commonly used to determine how interfacial films of pulmonary surfactant respond to changes in surface area, achieved by varying hydrostatic pressure. Although assumed to be isothermal, the gas phase temperature (Tg) would increase by >100°C during compression from 1 to 3 atm if the process were adiabatic. To determine the actual change in temperature, we monitored pressure (P) and volume (V) during compressions lasting <1 s for bubbles with and without interfacial films and used P · V to evaluate Tg. P · V fell during and after the rapid compressions, consistent with reductions in n, the moles of gas phase molecules, because of increasing solubility in the subphase at higher P. As expected for a process with first-order kinetics, during 1 h after the rapid compression P · V decreased along a simple exponential curve. The temporal variation of n moles of gas was determined from P · V >10 min after the compression when the two phases should be isothermal. Back extrapolation of n then allowed calculation of Tg from P · V immediately after the compression. Our results indicate that for bubbles with or without interfacial films compressed to >3 atm within 1 s, the change in Tg is <2°C.

Reconfiguration and Unified Kinematics Analysis of a Metamorphic Parallel Mechanism With Bifurcated Motion

2012 ◽  
Author(s):  
Dongming Gan ◽  
Jian S. Dai ◽  
Lakmal D. Seneviratne
Keyword(s):  
Parallel Mechanism ◽  
Geometric Condition ◽  
Translation Vector ◽  
Kinematics Analysis ◽  
Constraint Equations ◽  
Mechanism Modeling ◽  
The Difference ◽  
Two Phases ◽  
Set Up ◽  
Joint Center

This paper introduced a new metamorphic parallel mechanism consisting of four reconfigurable rTPS limbs. Based on the reconfigurability of the reconfigurable Hooke (rT) joint, the rTPS limb has two phases while in one phase the limb has no constraint to the platform, in the other it constrains the spherical joint center to lie on a plane. This results in the mechanism to have ability of reconfiguration between different topologies with variable mobility. Geometric constraint equations of the platform rotation matrix and translation vector are set up based on the point-plane constraint, which reveals the bifurcated motion property in the topology with mobility 2 and the geometric condition with mobility change in altering to other mechanism topologies. Following this, a unified kinematics limb modeling is proposed considering the difference between the two phases of the reconfigurable rTPS limb. This is further applied for the mechanism modeling and both the inverse and forward kinematics is analytically solved by combining phases of the four limbs covering all the mechanism topologies.

Sign in / Sign up

Export Citation Format

Share Document