Monotone recursive types and recursive data representations in Cedille

Guided by Tarksi’s fixpoint theorem in order theory, we show how to derive monotone recursive types with constant-time roll and unroll operations within Cedille, an impredicative, constructive, and logically consistent pure typed lambda calculus. This derivation takes place within the preorder on Cedille types induced by type inclusions, a notion which is expressible within the theory itself. As applications, we use monotone recursive types to generically derive two recursive representations of data in lambda calculus, the Parigot and Scott encoding. For both encodings, we prove induction and examine the computational and extensional properties of their destructor, iterator, and primitive recursor in Cedille. For our Scott encoding in particular, we translate into Cedille a construction due to Lepigre and Raffalli (2019) that equips Scott naturals with primitive recursion, then extend this construction to derive a generic induction principle. This allows us to give efficient and provably unique (up to function extensionality) solutions for the iteration and primitive recursion schemes for Scott-encoded data.

Set Theory INC# ∞# Based on Innitary Intuitionistic Logic with Restricted Modus Ponens Rule. Hyper Inductive Denitions. Application in Transcendental Number Theory. Generalized Lindemann-Weierstrass Theorem

In this paper intuitionistic set theory INC#∞# in infinitary set theoretical language is considered. External induction principle in nonstandard intuitionistic arithmetic were derived. Non trivial application in number theory is considered.The Goldbach-Euler theorem is obtained without any references to Catalan conjecture. Main results are: (i) number ee is transcendental; (ii) the both numbers e + π and e − π are irrational.

Вплив енерговтрат імплантата з бездротовим живленням на тепловий стан організму

Technical means that create for regenerating lost functions of the human body primarily focused on the target function. However, even when implants achieve performance that corresponds to natural organs and systems, in many cases the developers do not pay enough attention to the energy supply of implants and additional heat load due to energy losses in mechanical, electrical, and electronic units. If you do not consider these factors, it limits the duration and medical safety of the devices. It is especially true for implants with significant power consumption and wireless power supply. Therefore, this work determines the allowable additional heat load of the human body to justify the choice of further circuit solutions for wireless powering of implants with significant energy consumption and long-term operation. The subject of research is the processes of heat exchange between the implant and body structures and their energy and temperature indicators. The research object was chosen as an implant of the type "Artificial Heart" device (AHD) with a maximum power of 20… 25 W and the magnetic induction principle of energy transfer. The research tasks are to analyze the processes of heat exchange between the implant and the biostructures of the body; to calculate quantitative indicators of energy exchange in the location of the main components of the implant; to determine the temperature of biotissues in the area of the receiving inductor. The subject of research is the processes of heat exchange between the implant and body structures and their energy and temperature indicators. The research object was chosen as the implant of the type "Artificial Heart" device (AHD) with a maximum power of 20… 25 W and the magnetic induction principle of energy transfer. The research tasks are to analyze the processes of heat exchange between the implant and the biostructures of the body; to calculate quantitative indicators of energy exchange in the location of the main components of the implant; to determine the temperature of biotissues in the area of the receiving inductor. Research results. The processes of heat exchange between the structural elements of the implant and the biostructures of the body have a complex combination of physiological and physical mechanisms. Estimates are made based on the thermal conductivity process, as the most objective in terms of known quantitative indicators. With an average efficiency of ~ 0.8 for mechanical, electrical, and electronic components of the implant "Artificial Heart," the human body can maintain a stable temperature of internal organs in the presence of an implant with a maximum power consumption of 20 watts. The calculation conducted using the method of electrothermal analogy showed a possible increase in the temperature of biotissues in contact with the surface of the receiving implanted inductor, by 1.32 ° C. This value refers to the critical levels of internal tissue temperature rise. Summary. For practical implementation of the autonomous device the Artificial Heart Device, it is necessary to combine known or to find the original circuit-technical and design decisions of construction of components of wireless power supply with the magnetic induction principle and efficiency of not less than 0,8. To prevent thermal overload of biotissues, it is advisable to introduce a temperature control channel at potentially critical locations of the implanted elements. It is possible to predict the finding of these critical points by calculations by the method of electrothermal analogy.

Relating Apartness and Bisimulation

A bisimulation for a coalgebra of a functor on the category of sets can be described via a coalgebra in the category of relations, of a lifted functor. A final coalgebra then gives rise to the coinduction principle, which states that two bisimilar elements are equal. For polynomial functors, this leads to well-known descriptions. In the present paper we look at the dual notion of "apartness". Intuitively, two elements are apart if there is a positive way to distinguish them. Phrased differently: two elements are apart if and only if they are not bisimilar. Since apartness is an inductive notion, described by a least fixed point, we can give a proof system, to derive that two elements are apart. This proof system has derivation rules and two elements are apart if and only if there is a finite derivation (using the rules) of this fact. We study apartness versus bisimulation in two separate ways. First, for weak forms of bisimulation on labelled transition systems, where silent (tau) steps are included, we define an apartness notion that corresponds to weak bisimulation and another apartness that corresponds to branching bisimulation. The rules for apartness can be used to show that two states of a labelled transition system are not branching bismilar. To support the apartness view on labelled transition systems, we cast a number of well-known properties of branching bisimulation in terms of branching apartness and prove them. Next, we also study the more general categorical situation and show that indeed, apartness is the dual of bisimilarity in a precise categorical sense: apartness is an initial algebra and gives rise to an induction principle. In this analogy, we include the powerset functor, which gives a semantics to non-deterministic choice in process-theory.

Set Theory INC# ∞# Based on Infinitary Intuitionistic Logic with Restricted Modus Ponens Rule (Part.II) Hyper Inductive Definitions

In this paper intuitionistic set theory INC# ∞# in infinitary set theoretical language is considered. External induction principle in nonstandard intuitionistic arithmetic were derived. Non trivial application in number theory is considered.The Goldbach-Euler theorem is obtained without anyreferences to Catalan conjecture.

Multivariate Dynamic Sneak-Out Inequalities on Time Scales

In this study, we extend some “sneak-out” inequalities on time scales for a function depending on more than one parameter. The results are proved by using the induction principle and time scale version of Minkowski inequalities. In seeking applications, these inequalities are discussed in classical, discrete, and quantum calculus.

A Note on the Difference of Powers and Falling Powers

Combinatorial sums and binomial identities have appeared in many branches of mathematics, physics, and engineering. They can be established by many techniques, from generating functions to special series. Here, using a simple mathematical induction principle, we obtain a new combinatorial sum that involves ordinary powers, falling powers, and binomial coefficient at once. This way, and without the use of any complicated analytic technique, we obtain a result that already exists and a generalization of an identity derived from Sterling numbers of the second kind. Our formula is new, genuine, and several identities can be derived from it. The findings of this study can help for better understanding of the relation between ordinary and falling powers, which both play a very important role in discrete mathematics.

An Electric Field Microsensor with Mutual Shielding Electrodes

This paper proposes an electric field microsensor (EFM) with mutual shielding electrodes. Based on the charge-induction principle, the EFM consists of fixed electrodes and piezoelectric-driving vertically-movable electrodes. All the fixed electrodes and movable electrodes work as both sensing electrodes and shielding electrodes. In other words, all the fixed and movable electrodes are sensing electrodes, and they are mutually shielding electrodes simultaneously. The movable electrodes are driven to periodically modulate the electric field distribution at themselves and the fixed electrodes, and the induced currents from both movable and fixed electrodes are generated simultaneously. The electrode structure adopts an interdigital structure, and the EFM has been simulated by finite element methods. Simulation results show that, since the sensing area of this EFM is doubled, the variation of induced charge is twice, and therefore the output signal of the sensor is increased. The piezoelectric material, lead zirconate titanate (PZT), is prepared by the sol–gel method, and the microsensor chip is fabricated.