987 resultados para Partial Order Semantics
Resumo:
In this Thesis we consider a class of second order partial differential operators with non-negative characteristic form and with smooth coefficients. Main assumptions on the relevant operators are hypoellipticity and existence of a well-behaved global fundamental solution. We first make a deep analysis of the L-Green function for arbitrary open sets and of its applications to the Representation Theorems of Riesz-type for L-subharmonic and L-superharmonic functions. Then, we prove an Inverse Mean value Theorem characterizing the superlevel sets of the fundamental solution by means of L-harmonic functions. Furthermore, we establish a Lebesgue-type result showing the role of the mean-integal operator in solving the homogeneus Dirichlet problem related to L in the Perron-Wiener sense. Finally, we compare Perron-Wiener and weak variational solutions of the homogeneous Dirichlet problem, under specific hypothesis on the boundary datum.
Resumo:
El cálculo de relaciones binarias fue creado por De Morgan en 1860 para ser posteriormente desarrollado en gran medida por Peirce y Schröder. Tarski, Givant, Freyd y Scedrov demostraron que las álgebras relacionales son capaces de formalizar la lógica de primer orden, la lógica de orden superior así como la teoría de conjuntos. A partir de los resultados matemáticos de Tarski y Freyd, esta tesis desarrolla semánticas denotacionales y operacionales para la programación lógica con restricciones usando el álgebra relacional como base. La idea principal es la utilización del concepto de semántica ejecutable, semánticas cuya característica principal es el que la ejecución es posible utilizando el razonamiento estándar del universo semántico, este caso, razonamiento ecuacional. En el caso de este trabajo, se muestra que las álgebras relacionales distributivas con un operador de punto fijo capturan toda la teoría y metateoría estándar de la programación lógica con restricciones incluyendo los árboles utilizados en la búsqueda de demostraciones. La mayor parte de técnicas de optimización de programas, evaluación parcial e interpretación abstracta pueden ser llevadas a cabo utilizando las semánticas aquí presentadas. La demostración de la corrección de la implementación resulta extremadamente sencilla. En la primera parte de la tesis, un programa lógico con restricciones es traducido a un conjunto de términos relacionales. La interpretación estándar en la teoría de conjuntos de dichas relaciones coincide con la semántica estándar para CLP. Las consultas contra el programa traducido son llevadas a cabo mediante la reescritura de relaciones. Para concluir la primera parte, se demuestra la corrección y equivalencia operacional de esta nueva semántica, así como se define un algoritmo de unificación mediante la reescritura de relaciones. La segunda parte de la tesis desarrolla una semántica para la programación lógica con restricciones usando la teoría de alegorías—versión categórica del álgebra de relaciones—de Freyd. Para ello, se definen dos nuevos conceptos de Categoría Regular de Lawvere y _-Alegoría, en las cuales es posible interpretar un programa lógico. La ventaja fundamental que el enfoque categórico aporta es la definición de una máquina categórica que mejora e sistema de reescritura presentado en la primera parte. Gracias al uso de relaciones tabulares, la máquina modela la ejecución eficiente sin salir de un marco estrictamente formal. Utilizando la reescritura de diagramas, se define un algoritmo para el cálculo de pullbacks en Categorías Regulares de Lawvere. Los dominios de las tabulaciones aportan información sobre la utilización de memoria y variable libres, mientras que el estado compartido queda capturado por los diagramas. La especificación de la máquina induce la derivación formal de un juego de instrucciones eficiente. El marco categórico aporta otras importantes ventajas, como la posibilidad de incorporar tipos de datos algebraicos, funciones y otras extensiones a Prolog, a la vez que se conserva el carácter 100% declarativo de nuestra semántica. ABSTRACT The calculus of binary relations was introduced by De Morgan in 1860, to be greatly developed by Peirce and Schröder, as well as many others in the twentieth century. Using different formulations of relational structures, Tarski, Givant, Freyd, and Scedrov have shown how relation algebras can provide a variable-free way of formalizing first order logic, higher order logic and set theory, among other formal systems. Building on those mathematical results, we develop denotational and operational semantics for Constraint Logic Programming using relation algebra. The idea of executable semantics plays a fundamental role in this work, both as a philosophical and technical foundation. We call a semantics executable when program execution can be carried out using the regular theory and tools that define the semantic universe. Throughout this work, the use of pure algebraic reasoning is the basis of denotational and operational results, eliminating all the classical non-equational meta-theory associated to traditional semantics for Logic Programming. All algebraic reasoning, including execution, is performed in an algebraic way, to the point we could state that the denotational semantics of a CLP program is directly executable. Techniques like optimization, partial evaluation and abstract interpretation find a natural place in our algebraic models. Other properties, like correctness of the implementation or program transformation are easy to check, as they are carried out using instances of the general equational theory. In the first part of the work, we translate Constraint Logic Programs to binary relations in a modified version of the distributive relation algebras used by Tarski. Execution is carried out by a rewriting system. We prove adequacy and operational equivalence of the semantics. In the second part of the work, the relation algebraic approach is improved by using allegory theory, a categorical version of the algebra of relations developed by Freyd and Scedrov. The use of allegories lifts the semantics to typed relations, which capture the number of logical variables used by a predicate or program state in a declarative way. A logic program is interpreted in a _-allegory, which is in turn generated from a new notion of Regular Lawvere Category. As in the untyped case, program translation coincides with program interpretation. Thus, we develop a categorical machine directly from the semantics. The machine is based on relation composition, with a pullback calculation algorithm at its core. The algorithm is defined with the help of a notion of diagram rewriting. In this operational interpretation, types represent information about memory allocation and the execution mechanism is more efficient, thanks to the faithful representation of shared state by categorical projections. We finish the work by illustrating how the categorical semantics allows the incorporation into Prolog of constructs typical of Functional Programming, like abstract data types, and strict and lazy functions.
Resumo:
A new formalism, called Hiord, for defining type-free higherorder logic programming languages with predicate abstraction is introduced. A model theory, based on partial combinatory algebras, is presented, with respect to which the formalism is shown sound. A programming language built on a subset of Hiord, and its implementation are discussed. A new proposal for defining modules in this framework is considered, along with several examples.
Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order
Resumo:
We derive by program transformation Pierre Crégut s full-reducing Krivine machine KN from the structural operational semantics of the normal order reduction strategy in a closure-converted pure lambda calculus. We thus establish the correspondence between the strategy and the machine, and showcase our technique for deriving full-reducing abstract machines. Actually, the machine we obtain is a slightly optimised version that can work with open terms and may be used in implementations of proof assistants.
Resumo:
Olivier Danvy and others have shown the syntactic correspondence between reduction semantics (a small-step semantics) and abstract machines, as well as the functional correspondence between reduction-free normalisers (a big-step semantics) and abstract machines. The correspondences are established by program transformation (so-called interderivation) techniques. A reduction semantics and a reduction-free normaliser are interderivable when the abstract machine obtained from them is the same. However, the correspondences fail when the underlying reduction strategy is hybrid, i.e., relies on another sub-strategy. Hybridisation is an essential structural property of full-reducing and complete strategies. Hybridisation is unproblematic in the functional correspondence. But in the syntactic correspondence the refocusing and inlining-of-iterate-function steps become context sensitive, preventing the refunctionalisation of the abstract machine. We show how to solve the problem and showcase the interderivation of normalisers for normal order, the standard, full-reducing and complete strategy of the pure lambda calculus. Our solution makes it possible to interderive, rather than contrive, full-reducing abstract machines. As expected, the machine we obtain is a variant of Pierre Crégut s full Krivine machine KN.
Resumo:
Purpose. Mice rendered hypoglycemic by a null mutation in the glucagon receptor gene Gcgr display late-onset retinal degeneration and loss of retinal sensitivity. Acute hyperglycemia induced by dextrose ingestion does not restore their retinal function, which is consistent with irreversible loss of vision. The goal of this study was to establish whether long-term administration of high dietary glucose rescues retinal function and circuit connectivity in aged Gcgr−/− mice. Methods. Gcgr−/− mice were administered a carbohydrate-rich diet starting at 12 months of age. After 1 month of treatment, retinal function and structure were evaluated using electroretinographic (ERG) recordings and immunohistochemistry. Results. Treatment with a carbohydrate-rich diet raised blood glucose levels and improved retinal function in Gcgr−/− mice. Blood glucose increased from moderate hypoglycemia to euglycemic levels, whereas ERG b-wave sensitivity improved approximately 10-fold. Because the b-wave reflects the electrical activity of second-order cells, we examined for changes in rod-to-bipolar cell synapses. Gcgr−/− retinas have 20% fewer synaptic pairings than Gcgr+/− retinas. Remarkably, most of the lost synapses were located farthest from the bipolar cell body, near the distal boundary of the outer plexiform layer (OPL), suggesting that apical synapses are most vulnerable to chronic hypoglycemia. Although treatment with the carbohydrate-rich diet restored retinal function, it did not restore these synaptic contacts. Conclusions. Prolonged exposure to diet-induced euglycemia improves retinal function but does not reestablish synaptic contacts lost by chronic hypoglycemia. These results suggest that retinal neurons have a homeostatic mechanism that integrates energetic status over prolonged periods of time and allows them to recover functionality despite synaptic loss.
Resumo:
Denote the set of 21 non-isomorphic cubic graphs of order 10 by L. We first determine precisely which L is an element of L occur as the leave of a partial Steiner triple system, thus settling the existence problem for partial Steiner triple systems of order 10 with cubic leaves. Then we settle the embedding problem for partial Steiner triple systems with leaves L is an element of L. This second result is obtained as a corollary of a more general result which gives, for each integer v greater than or equal to 10 and each L is an element of L, necessary and sufficient conditions for the existence of a partial Steiner triple system of order v with leave consisting of the complement of L and v - 10 isolated vertices. (C) 2004 Elsevier B.V. All rights reserved.
Resumo:
We consider the existence and uniqueness problem for partial differential-functional equations of the first order with the initial condition for which the right-hand side depends on the derivative of unknown function with deviating argument.
Resumo:
MSC 2010: 26A33, 34A37, 34K37, 34K40, 35R11
Resumo:
The substantive legislation on which Agricultural Processing Companies is based has some notable gaps with regard to the pertinent accounting system. There are grey areas concerning compulsory accounting records and their legalization, together with the process for drawing up, checking, approving and depositing the annual accounts.Consequently, in this paper, we will look first at the corporate and accounting records for Agricultural Processing Companies, putting forward proposals in the wake of recent legislation on the legalization of generally applied corporate and accounting documents.A critical analysis will also be made of the entire process of drafting, auditing, approving and depositing the annual accounts and other documents that Agricultural Processing Companies must send each year to their respective regional registries. Legal and mercantile registries will be differentiated from administrative ones and, in this last sense, changes will be suggested with regard to the place and objective of the deposit of such documents.After thirty-four years old, the substantive legislation in economic and accounting matters of the SAT is out of step with the current law, so a review is necessary. Recent regional regulations have not been a real breakthrough in this regard. We assert the existence of a gap between the substantive rules of the SAT and general accounting rules on financial statements, which is unsustainable and it needs a quick legislative action to be canceled.
Resumo:
Networks of Kuramoto oscillators with a positive correlation between the oscillators frequencies and the degree of their corresponding vertices exhibit so-called explosive synchronization behavior, which is now under intensive investigation. Here we study and discuss explosive synchronization in a situation that has not yet been considered, namely when only a part, typically a small part, of the vertices is subjected to a degree-frequency correlation. Our results show that in order to have explosive synchronization, it suffices to have degree-frequency correlations only for the hubs, the vertices with the highest degrees. Moreover, we show that a partial degree-frequency correlation does not only promotes but also allows explosive synchronization to happen in networks for which a full degree-frequency correlation would not allow it. We perform a mean-field analysis and our conclusions were corroborated by exhaustive numerical experiments for synthetic networks and also for the undirected and unweighed version of a typical benchmark biological network, namely the neural network of the worm Caenorhabditis elegans. The latter is an explicit example where partial degree-frequency correlation leads to explosive synchronization with hysteresis, in contrast with the fully correlated case, for which no explosive synchronization is observed.
Resumo:
We present an extensive study of the structural, magnetic, and thermodynamic properties of the two heterometallic oxyborates: Co(2)FeO(2)BO(3) and Ni(2)FeO(2)BO(3). This has been carried out through x-ray diffraction at room temperature (RT) and 150 K, dc and ac magnetic susceptibilities, and specific-heat experiments in single crystals above 2 K. The magnetic properties of these iron ludwigites are discussed in comparison with those of the other two known homometallic ludwigites: Fe(3)O(2)BO(3) and Co(3)O(2)BO(3). In both ludwigites now studied we have found that the magnetic ordering of the Fe(3+) ions occurs at temperatures very near to which they order in Fe(3)O(2)BO(3). A freezing of the divalent ions (Co and Ni) is observed at lower temperatures. Our x-ray diffraction study of both ludwigites at RT and 150 K showed very small ionic disorder in apparent contrast with the freezing of the divalent ion spins. The structural transition that occurs in homometallic Fe(3)O(2)BO(3) has not been found in the present mixed ludwigites in the temperature range investigated.
Resumo:
We establish the existence of mild solutions for a class of impulsive second-order partial neutral functional differential equations with infinite delay in a Banach space. (C) 2009 Published by Elsevier Ltd
Resumo:
In this work we study the existence and uniqueness of pseudo-almost periodic solutions for a first-order abstract functional differential equation with a linear part dominated by a Hille-Yosida type operator with a non-dense domain. (C) 2009 Published by Elsevier Ltd
Resumo:
In this paper we study the existence of mild solutions for a class of first order abstract partial neutral differential equations with state-dependent delay. (C) 2008 Elsevier Ltd. All rights reserved.