28 research outputs found
Dependently Typed Attribute Grammars
No full textAttribute Grammars (AGs) are a domain-specific language for functional and composable descriptions of tree traversals. Given such a description, it is not immediately clear how to state and prove properties of AGs formally. To meet this challenge, we apply dependent types to AGs. In a dependently typed AG, the type of an attribute may refer to values of attributes. The type of an attribute is an invariant, the value of an attribute a proof for that invariant. Additionally, when an AG is cycle-free, the composition of the attributes is logically consistent. We present a lightweight approach using a preprocessor in combination with the dependently typed language Agda
The Very Lazy Lambda-Calculus and the STEC Machine
No full textCurrent implementations of non-strict functional languages rely on call-by-name reduction to implement the λ-calculus. An interesting alternative is head occurrence reduction, a reduction strategy specifically designed for the implementation of non-strict, purely functional languages. This work introduces the very lazy λ -calculus, which allows a systematic description of this approach. It is not based on regular β-reduction but a generalised rewriting rule called γ-reduction that requires fewer reductions to obtain useful results from a term. It therefore promises more efficient program execution than conventional execution models. To demonstrate the applicability of the approach, an adaptation of the Pointer Abstract Machine (PAM) is specified that implements the very lazy λ-calculus and constitutes a foundation for a new class of efficient functional language implementations
Feedback genereren in leeromgevingen voor algebra
No full textHet gebruik van leeromgevingen bij het wiskundeonderwijs in algebra is de afgelopen jaren toegenomen. Het geven van feedback, bijvoorbeeld door een diagnose van een stap die een leerling heeft gezet te stellen, een hint te geven, of een volledige uitwerking van een opgave te geven, is binnen veel van deze omgevingen niet mogelijk, of zeer arbeidsintensief om te specificeren. In dit artikel presenteren Johan Jeuring en Bastiaan Heeren het Ideas-raamwerk, waarmee leeromgevingen automatisch feedback kunnen geven. Voor het geven van feedback wordt gebruik gemaakt van fundamentele concepten uit de wiskunde en informatica, zoals herschrijfstappen, views of normaalvormen en herschrijfstrategieën. Door het probleem van het geven van feedback te transformeren naar het ontleden van gebruikersstappen aan de hand van een herschrijfstrategie, wordt gebruik gemaakt van kennis over ontleden om automatisch feedback te geven
Visitor-based Attribute Grammars with Side Effect
No full textThe visitor design pattern is often applied to program traversal algorithms over Abstract Syntax Trees (ASTs). It defines a visitor, an object with a visit method that is executed for each node in the AST. These visitors have the advantage that the order of traversal is explicitly under control of the programmer, which is essential to deal with side-effectful computations. Unfortunately, the exchange of results between traversals is error-prone. Attribute Grammars (AGs) are an alternative way to write multi-traversal algorithms. An attribute evaluator decorates the AST with attributes in one or more traversals. The attributes form a convenient mechanism to exchange results between traversals. Unfortunately, AGs discourage the use of side effect. In this paper, we present ruler-front, a language capturing the combination of the above approaches. A ruler-front grammar can be translated to traversal algorithms in multiple languages. In this paper, we translate to the imperative, dynamically-typed language JavaScript
Inference of Program Properties with Attribute Grammars, Revisited
No full textA programming language is an essential ingredient for writing concise, maintainable, and error-free computer programs. A compiler takes a text written in such a language and compiles into machine instructions, and is usually implemented as a number of traversals over the abstract syntax of the program. Attribute Grammars (AGs) are a powerful tool for the description of such traversals and thus the implementation of a compiler: AGs offer aspect-oriented programming, abstraction over common traversal patterns, and automatic inference of a sound and efficient traversal algorithm. Over the years, computer languages have become more complex and harder to implement. Notoriously difficult to implement is type checking or type inference, which for complex languages is not only specified in terms of the abstract syntax but also in terms of the inferred types, and requires traversals that are hard to describe in general, and in particular with AGs. The reason is that the traversals mutually depend on types, which are not known apriori, thus the traversal represents some strategy that decides during the process in which order type information is collected and processed. In this thesis, we investigated the application of attribute grammars to the description of inference algorithms, with the goal of being able to describe such algorithms while retaining the good properties of AGs. To this end, this thesis builds on higher-order attribute grammars to describe traversals over semantics instead of syntax, conditional attribute grammars to describe the decisions to be made during the inference process, and ordered attribute grammars to express inference strategies. Visits, a concept from ordered attribute grammars, play an essential role in our work. A visit to a node in the abstract syntax tree represents a unit of evaluation. We make visits explicit in our AG descriptions so that we can express the order of evaluation and conditionally iterate visits. Moreover, we show that on top of visits, we can express decision points, and present a stepwise evaluation strategy that allows us to explore alternative choices until reaching a decision. Our work is a conservative extension of attribute grammars, and preserves their good aspects. We declaratively express properties of the evaluation order, while keeping the automatic scheduling of attribute computations. Our work integrates well with various attribute grammar extensions, such as parallel evaluation. In particular, our work facilitates an integration with dependently typed programming, which paves the way to prove and enforce the correctness of compilers described with attribute grammars
Less Is More : Generic Programming Theory and Practice
No full textAbstraction is ubiquitous in computer programming. The work of this thesis focuses on one specific form of abstraction. Computer programs manipulate data, which can either be primitive machine data (such as integer or fractional numbers) or programmer-defined data (such as lists, trees, matrices, images, etc.). There is only a small number of primitive datatypes, but a potentially infinite number of programmer-defined data. The structure of the latter data depends on the problem at hand, and while some structures appear very often (such as sequences of values), others are truly specific to a particular problem. Some kind of functionality is generally desired for all types of data. Reading and storing files to the disk, for instance, is as important for machine integers as it is for complex healthcare databases, or genealogy trees. And not just reading and writing files: testing for equality, sorting, traversing, computing the length, all are examples of functionality that is often desired for all kinds of data. Most programming languages allow defining complex datatypes as a form of abstraction, but few provide good support for defining behaviour that is generic over data. As such, programmers are forced to specify this behaviour over and over again, once for each new type of data, and also to adapt this code whenever the structure of their data changes. This is a tedious task, and can quickly become time-consuming, leading some programmers to write programs to generate this type of functionality automatically from the structure of data. We think that a programming language should allow programmers to define generic programs, which specify behaviour that is generic over the type of data. Moreover, it should automatically provide generic behaviour for new data, eliminating the need for repeated writing and rewriting of trivial code that just specialises general behaviour to a particular type of data. It should do so in a convenient way for the programmer, leading to more abstract and concise programs, while remaining clear and efficient. This leads us to the two research questions we set out to answer: 1) There are many different approaches to generic programming, varying in complexity and expressiveness. How can we better understand each of the approaches, and the way they relate to each other? 2) Poor runtime efficiency, insufficient datatype support, and lack of proper language integration are often pointed out as deficiencies in generic programming implementations. How can we best address these concerns? We answer the first question in the first part of this thesis. We start by picking a number of generic programming approaches and define a concise model for each of them. We then use this model to formally express how to embed the structural representation of data of one approach into another, allowing us to better understand the relation between different approaches. The second part of this thesis deals with answering the second question, devoting one chapter to analysing and mitigating each of the practical concern
Improving Audio Chord Transcription by Exploiting Harmonic and Metric Knowledge
No full textWe present a new system for chord transcription from polyphonic musical audio that uses domain-specific knowledge about tonal harmony and metrical position to improve chord transcription performance. Low-level pulse and spectral features are extracted from an audio source using the Vamp plugin architecture. Subsequently, for each beat-synchronised chromagram we compute a list of chord candidates matching that chromagram, together with the confidence in each candidate. When one particular chord candidate matches the chromagram significantly better than all others, this chord is selected to represent the segment. However, when multiple chords match the chromagram similarly well, we use a formal music theoretical model of tonal harmony to select the chord candidate that best matches the sequence based on the surrounding chords. In an experiment we show that exploiting metrical and harmonic knowledge yields statistically significant chord transcription improvements on a corpus of 217 Beatles, Queen, and Zweieck songs
Type-changing rewriting and semantics-preserving transformation
No full textWe have identified a class of whole-program transformations that are regular in structure and require changing the types of terms throughout a program while simultaneously preserving the initial semantics after transformation. This class of transformations cannot be safely performed with typical term rewriting techniques, which do not allow for changing the types of terms. In this paper, we present a formalization of type-and-transform systems, an automated approach to the whole-program transformation of terms of one type to terms of a different, isomorphic type using type-changing rewrite rules. A type-and-transform system defines typing and semantics relations between all corresponding source and target subprograms such that a complete transformation guarantees that the whole programs have equivalent types and semantics. We describe the type-and-transform system for the lambda calculus with let-polymorphism and general recursion, including several examples from the literature and properties of the system. (C) 2015 Elsevier B.V. All rights reserved
HarmTrace: Improving Harmonic Similarity Estimation Using Functional Harmony Analysis
No full text[TODO] Add abstract here
