Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userDenotational semantics as a foundation for cost recurrence extraction for functional languages
64
0
0.0
(
0
)
Added by
Norman Danner
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
A standard informal method for analyzing the asymptotic complexity of a program is to extract a recurrence that describes its cost in terms of the size of its input, and then to compute a closed-form upper bound on that recurrence. We give a formal account of that method for functional programs in a higher-order language with let-polymorphism The method consists of two phases. In the first phase, a monadic translation is performed to extract a cost-annotated version of the original program. In the second phase, the extracted program is interpreted in a model. The key feature of this second phase is that different models describe different notions of size. This plays out specifically for values of inductive type, where different notions of size may be appropriate depending on the analysis, and for polymorphic functions, where we show that the notion of size for a polymorphic function can be described formally as the data that is common to the notions of size of its instances. We give several examples of different models that formally justify various informal cost analyses to show the applicability of our approach.
rate research
Read More
A typical way of analyzing the time complexity of functional programs is to extract a recurrence expressing the running time of the program in terms of the size of its input, and then to solve the recurrence to obtain a big-O bound. For recurrence extraction to be compositional, it is also necessary to extract recurrences for the size of outputs of helper functions. Previous work has developed techniques for using logical relations to state a formal correctness theorem for a general recurrence extraction translation: a program is bounded by a recurrence when the operational cost is bounded by the extracted cost, and the output value is bounded, according to a value bounding relation defined by induction on types, by the extracted size. This previous work supports higher-order functions by viewing recurrences as programs in a lambda-calculus, or as mathematical entities in a denotational semantics thereof. In this paper, we extend these techniques to support amortized analysis, where costs are rearranged from one portion of a program to another to achieve more precise bounds. We give an intermediate language in which programs can be annotated according to the bankers method of amortized analysis; this language has an affine type system to ensure credits are not spent more than once. We give a recurrence extraction translation of this language into a recurrence language, a simply-typed lambda-calculus with a cost type, and state and prove a bounding logical relation expressing the correctness of this translation. The recurrence language has a denotational semantics in preorders, and we use this semantics to solve recurrences, e.g analyzing binary counters and splay trees.
PROMELA (Process Meta Language) is a high-level specification language designed for modeling interactions in distributed systems. PROMELA is used as the input language for the model checker SPIN (Simple Promela INterpreter). The main characteristics of PROMELA are non-determinism, process communication through synchronous as well as asynchronous channels, and the possibility to dynamically create instances of processes. In this paper, we introduce a bottom-up, fixpoint semantics that aims to model the behavior of PROMELA programs. This work is the first step towards a more ambitious goal where analysis and verification techniques based on abstract interpretation would be defined on top of such semantics.
In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a linear fragment (arena net) and a parallel weakening-contraction fragment (skew fibration). In particular we provide an encoding of modal formulas by means of directed graphs (modal arenas), and an encoding of linear proofs as modal arenas equipped with vertex partitions satisfying topological criteria. The second semantics is given by means of winning innocent strategies of a two-player game over modal arenas. This is given by extending the Heijltjes-Hughes-Stra{ss}burger correspondence between intuitionistic combinatorial proofs and winning innocent strategies in a Hyland-Ong arena. Using our first result, we provide a characterisation of winning strategies for games on a modal arena corresponding to proofs with modalities.
Constraint Handling Rules (CHR) are a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multi-headed guarded rules which allow one to rewrite constraints into simpler ones until a solved form is reached. CHR has received a considerable attention, both from the practical and from the theoretical side. Nevertheless, due the use of multi-headed clauses, there are several aspects of the CHR semantics which have not been clarified yet. In particular, no compositional semantics for CHR has been defined so far. In this paper we introduce a fix-point semantics which characterizes the input/output behavior of a CHR program and which is and-compositional, that is, which allows to retrieve the semantics of a conjunctive query from the semantics of its components. Such a semantics can be used as a basis to define incremental and modular analysis and verification tools.
Domain-specific languages are becoming increasingly important. Almost every application touches multiple domains. But how to define, use, and combine multiple DSLs within the same application? The most common approach is to split the project along the domain boundaries into multiple pieces and files. Each file is then compiled separately. Alternatively, multiple languages can be embedded in a flexible host language: within the same syntax a new domain semantic is provided. In this paper we follow a less explored route of metamorphic languages. These languages are able to modify their own syntax and semantics on the fly, thus becoming a more flexible host for DSLs. Our language allows for dynamic creation of grammars and switching languages where needed. We achieve this through a novel concept of Syntax-Directed Execution. A language grammar includes semantic actions that are pieces of functional code executed immediately during parsing. By avoiding additional intermediate representation, connecting actions from different languages and domains is greatly simplified. Still, actions can generate highly specialized code though lambda encapsulation and Dynamic Staging.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
