<p> Partial Evaluation (PE) is a program transformation technique that generates a specialized version of a program with respect to a subset of its inputs. PE is an automatic approach to program generation and meta-programming. This thesis presents a method of partially evaluating Maple programs using a fully online methodology.</p> <p> We present an implementation called MapleMIX, and use it towards two goals. Firstly we show how MapleMIX can be used to generate optimized versions of generic programs written in Maple. Secondly we use MapleMIX to mine symbolic computation code for residual theorems, which we present as precise solutions to parametric problems encountered in Computer Algebra Systems.</p> <p> The implementation of MapleMIX has been modularized using a high-level intermediate language called M-form. Several syntax transformations from Maple to M-form make it an ideal representation for performing program specialization. Many specialization techniques have been explored including a novel online approach to handle partially-static data structures and an on-the-fly syntax transformation technique that propagates loop context into the body of dynamic conditionals.</p> / Thesis / Master of Science (MSc)

We constructed a parallelizing compiler that utilizes partial evaluation to achieve efficient parallel object code from very high-level data independent source programs. On several important scientific applications, the compiler attains parallel performance equivalent to or better than the best observed results from the manual restructuring of code. This is the first attempt to capitalize on partial evaluation's ability to expose low-level parallelism. New static scheduling techniques are used to utilize the fine-grained parallelism of the computations. The compiler maps the computation graph resulting from partial evaluation onto the Supercomputer Toolkit, an eight VLIW processor parallel computer.

[ES] La evaluación parcial de programas es una técnica general y potente de optimización de programas que preserva su semántica y tiene muchas aplicaciones relevantes. La optimización se consigue al especializar programas con respecto a una parte de sus datos de entrada, lo que produce un nuevo programa llamado residual o programa especializado tal que, al ejecutarlo con los datos de entrada restantes, producirá el mismo resultado que produce el programa original con todos sus datos de entrada. Los esquemas de evaluación parcial existentes no son aplicables a lenguajes expresivos basados en reglas como Maude, CafeOBJ, OBJ, ASF+SDF y ELAN, los cuales soportan: 1) sofisticados tipos estructurados con subtipos y sobrecarga de operadores; y 2) teorías ecuacionales modulo varias combinaciones de axiomas tales como asociatividad, conmutatividad e identidad. Esta tesis desarrolla las bases teóricas necesarias e ilustra los conceptos principales para su aplicación a programas expresivos escritos en el lenguaje Maude. El esquema de evaluación parcial presentado en esta tesis está basado en un algoritmo automático de desplegado que computa variantes de términos. Para asegurar la terminación del proceso de especialización se han diseñado algoritmos de alto rendimiento para la generalización ecuacional menos general con tipos ordenados y subsunción homeomórfica ecuacional con tipos ordenados. Se muestra que la técnica de evaluación parcial desarrollada es correcta y completa para teorías de reescritura convergentes que pueden contener varias combinaciones de axiomas de asociatividad, conmutatividad y/o identidad para diferentes operadores binarios. Finalmente se presenta Victoria, el primer evaluador parcial para teorías ecuacionales de tipos ordenados para el lenguaje Maude, y se demuestra la efectividad y el incremento en eficiencia ganado a través de experimentos realizados con ejemplos reales. / [CA] L'avaluació parcial de programes és una tècnica general i potent d'optimització de programes que preserva la seua semàntica i té moltes aplicacions rellevants. L'optimització s'aconseguix a l'especialitzar programes respecte a una part de les seues dades d'entrada, la qual cosa produïx un nou programa cridat residual o programa especialitzat tal que, a l'executar-ho amb les dades d'entrada restants, produirà el mateix resultat que produïx el programa original amb totes les seues dades d'entrada. Els esquemes d'avaluació parcial existents no són aplicables a llenguatges expressius basats en regles com Maude, CafeOBJ, OBJ, ASF+SDF i ELAN, els quals suporten: 1) sofisticats tipus estructurats amb subtipus i sobrecàrrega d'operadors; i 2) teories equacionals mòdul diverses combinacions d'axiomes com asociativitat, conmutativitat i identitat. Esta tesi desenrotlla les bases teòriques necessàries i il·lustra els conceptes principals per a la seua aplicació a programes expressius escrits en el llenguatge Maude. L'esquema d'avaluació parcial presentat en esta tesi està basat en un algoritme automàtic de desplegat que computa variants de termes. Per a assegurar la terminació del procés d'especialització s'han dissenyat algoritmes d'alt rendiment per a la generalització ecuacional menys general amb subtipus ordenats i subsunción ecuacional homeomórfica amb subtipus ordenats. Es mostra que la tècnica d'avaluació parcial desenrotllada és correcta i completa per a teories de reescriptura convergents que poden contindre diverses combinacions d'axiomes d'asociativitat, conmutativitat i identitat per a diferents operadors binaris. Finalment es presenta Victoria, el primer avaluador parcial per a teories equacionals de tipus ordenats per al llenguatge Maude i es demostra l'efectivitat i l'increment en eficiència guanyat a través d'experiments realitzats amb exemples reals. / [EN] Partial evaluation is a powerful and general program optimization technique that preserves program semantics and has many successful applications. Optimization is achieved by specializing programs w.r.t. a part of their input data so that, when the residual or specialized program is executed on the remaining input data, it produces the same outcome than the original program with all of its input data. Existing PE schemes do not apply to expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: 1) rich type structures with sorts, subsorts, and overloading; and 2) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity. This thesis develops the new foundations needed and illustrates the key concepts of equational order sorted partial evaluation by showing how they apply to the specialization of expressive programs written in Maude. Our partial evaluation scheme is based on an automatic unfolding algorithm that computes term variants and relies on high-performance order-sorted equational least general generalization and ordersorted equational homeomorphic embedding algorithms for ensuring termination.We show that our partial evaluation technique is sound and complete for order-sorted equational theories that may contain various combinations of associativity, commutativity, and/or identity axioms for different binary operators. Finally, we present Victoria, the first partial evaluator for Maude's order-sorted equational theories, and demonstrate the effectiveness of our partial evaluation scheme on several examples where it shows significant speed-up. / Finally, I extend my thanks to SENESCYT for the support provided for my studies. Also, I thank the Universidad de Guayaquil that is my place of work. / Cuenca Ortega, ÁE. (2019). Partial Evaluation of Rewriting Logic Theories [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/130206

Partial evaluation is a program transformation technique that specializes a program with respect to part of its input. While the specialization is typically performed ahead-of-time, moving it to a later stage may expose additional opportunities and allow for faster residual programs to be constructed. In this thesis, we present a method for specializing programs at run-time, for compiled code, using an online partial evaluator. Although partial evaluation has several applications, the evaluation of the method primarily focuses on its performance benefits. The main research problem addressed in this thesis is that of incorporating an online partial evaluator in compiled code. The partial evaluator is a sourceto-source translator that takes and produces an abstract syntax tree (AST). Our approach consists of three parts, namely that of partially evaluating, obtaining a partially evaluable representation and run-time code emitting. Concretely, we use the concept of lifting to store an AST in the compiled code that the partial evaluator then specializes at run-time. The residual code is thereafter naively just-in-time (JIT) compiled through dynamically linking it back to the executable as a shared library. We evaluate the method on several programs and show that the specialized programs sometimes are faster even with a low recursion depth. Though, while the results are promising, the overhead is typically significant and therefore the break-even points are large. Further research, for example using an efficient JIT compiler, is required to better evaluate the performance benefits of the approach. / Partiell evaluering är en programtransformationsteknik som specialiserar ett program givet delar av dess indata. Typisk sätt specialiseras program innan de exekveras, men genom att flytta specialisering till då programmet körs kan ytterligare information utnyttjas och därmed snabbare residualprogram konstrueras. I det här examensarbetet presenteras en metod för att specialisera program i körtid med online partiell evaluering, specifikt för kompilerade program. Metoden utvärderas främst utefter prestanda, men det ska nämnas att partiell evaluering har fler tillämpningar än så. Det huvudsakliga problemet som examensarbetet undersöker är inkorporeringen av en programspecialiserare (partial evaluator) i kompilerad kod. Den programspecialiserare som används tar både som indata och producerar ett abstrakt syntaxträd (AST). Vårt tillvägagångssätt består av tre delar, nämligen programspecialisering, erhållning av en representation som kan specialiseras och slutligen kodgenerering i körtid. Mer specifikt används konceptet lyftning för att spara ett AST i den kompilerade koden som därefter partiellt evalueras av programspecialiseraren under körtid. Som ett sista steg just-in-time (JIT) kompileras residualprogrammet. Detta görs på ett naivt vis genom att programmet kompileras till ett delat bibliotek som därefter dynamiskt länkas tillbaka till huvudprogrammet. Metoden utvärderas på flera program och vi visar att de specialiserade programmen i vissa fall var snabbare och det även med små rekursionsdjup. Resultaten är lovande, men den overhead som metoden ger upphov till är ofta signifikant vilket gör att det krävs många iterationer innan det specialiserade programmet blir snabbare. Ytterligare forskning och tester, till exempel med en effektiv JIT kompilator, är nödvändig för att bättre kunna utvärdera metodens prestandafördelar.

Type inference can be considered a form of partial evaluation that only evaluates a program with respect to its type annotations. Building on this key observation, this dissertation presents a uniform framework for expressing computation, its dynamic properties and corresponding static type information. By using a unified approach, the static phase divide between values and types is lifted. Instead, computations and properties can be freely assigned to the static or dynamic phase of computation. Even more, moving a property from one world to the other does not require any program modifications. This thesis builds a bridge between two worlds: That of statically typed languages and the dynamically typed world. The former is wanted for the offered static guarantees and detection of a range of defects. With the increasing power of type systems available, the kinds of errors that can be statically detected is growing, nearing the goal of proving overall program correctness from the program’s source code alone. However, such power does come for a price: Type systems are becoming more complex, restrictive and invasive, to the point where specifying type annotations becomes as complex as specifying the algorithm itself. Untyped languages, in contrast, may provide less static safety but they have simpler semantics and offer a higher flexibility. They allow programmers to express their ideas without worrying about provable correctness. Not surprisingly, untyped languages have a strong following when it comes to prototyping and rapid application development. Using the framework presented in this thesis, the programmer can have both: Prototyping applications using a dynamically typed approach and gradual refinement of prototypes into programs with static guarantees. Technically, this flexibility is achieved with the novel concept of auxiliary computations. Auxiliary computation are additional streams of computation. They model, next to the data’s computation, the computation of property of data. These streams thereby may depend on the actual data that is computed, as well as on further auxiliary computations. This expressiveness brings auxiliary computations into the domain of dependent types. Partial evaluation of auxiliary computations is used to infer static knowledge from auxiliary computations. Due to the interdependencies between auxiliary computations, evaluating only those parts of a program that contribute to a property is non trivial. A further contribution of this work is the use of demands on computations to narrow the extent of partial evaluation to a single property. An algorithm for demand inference is presented and the correctness of the inferred demands is shown.

Program manipulation is the task to perform transformations on program code, and is normally done in order to optimize the code with respect of the utilization of some computer resource. Partial evaluation is the task when partial computations can be performed in a program before it is actually executed. If a parameter to a procedure is constant a specialized version of that procedure can be generated if the constant is inserted instead of the parameter in the procedure body and as much computations in the code as possible are performed. A system is described which works on programs written in INTERLISP, and which performs partial evaluation together with other transformations such as beta-expansion and certain other optimization operations. The system works on full LISP and not only for a "pure" LISP dialect, and deals with problems occurring there involving side-effects, variable assignments etc. An analysis of a previous system, REDFUN, results in a list of problems, desired extensions and new features. This is used as a basis for a new design, resulting in a new implementation, REDFUN-2. This implementation, design considerations, constraints in the system, remaining problems, and other experience from the development and experiments with the system are reported in this paper.

Personalization constitutes the mechanisms and technologies necessary to customize information access to the end-user. It can be defined as the automatic adjustment of information content, structure, and presentation. The central thesis of this dissertation is that modeling interaction explicitly in a representation, and studying how partial information can be harnessed in it by program transformations to direct the flow of the interaction, can provide insight into, reveal opportunities for, and define a model for personalized interaction. To evaluate this thesis, a formal modeling methodology is developed for personalizing interactions with information systems, especially hierarchical hypermedia, based on program transformations. The predominant form of personalized interaction developed in this thesis is out-of-turn interaction, a technique which empowers the user to take the initiative in a user--system dialog by providing unsolicited, but relevant, information out-of-turn. Out-of-turn interaction helps flexibly bridge any mismatch between the user's model of information seeking and the system's hardwired hyperlink structure in a manner fundamentally different from extant solutions, such as multiple faceted browsing classifications and search tools. This capability is showcased through two interaction interfaces using alternate modalities to capture and communicate out-of-turn information to the underlying system: a toolbar embedded into a traditional browser for out-of-turn textual input and voice-enabled content pages for out-of-turn speech input. The specific research issues addressed involve identifying and developing representations and transformations suitable for general classes of hierarchical hypermedia, providing supplemental interactions for improving the personalized experience, and studying user's (out-of-turn) interactions with resulting systems. / Ph. D.

Simulating the human heart is a challenging problem, with simulations being very time consuming, to the extent that some can take days to compute even on high performance computing resources. There is considerable interest in computational optimisation techniques, with a view to making whole-heart simulations tractable. Reliability of heart model simulations is also of great concern, particularly considering clinical applications. Simulation software should be easily testable and maintainable, which is often not the case with extensively hand-optimised software. It is thus crucial to automate and verify any optimisations. CellML is an XML language designed for describing biological cell models from a mathematical modeller’s perspective, and is being developed at the University of Auckland. It gives us an abstract format for such models, and from a computer science perspective looks like a domain specific programming language. We are investigating the gains available from exploiting this viewpoint. We describe various static checks for CellML models, notably checking the dimensional consistency of mathematics, and investigate the possibilities of provably correct optimisations. In particular, we demonstrate that partial evaluation is a promising technique for this purpose, and that it combines well with a lookup table technique, commonly used in cardiac modelling, which we have automated. We have developed a formal operational semantics for CellML, which enables us to mathematically prove the partial evaluation of CellML correct, in that optimisation of models will not change the results of simulations. The use of lookup tables involves an approximation, thus introduces some error; we have analysed this using a posteriori techniques and shown how it may be managed. While the techniques could be applied more widely to biological models in general, this work focuses on cardiac models as an application area. We present experimental results demonstrating the effectiveness of our optimisations on a representative sample of cardiac cell models, in a variety of settings.

On est habitué à penser comme suit à un programme qui exécute: une donnée entre (un input), un moment passe, et un résultat ressort. On assume tacitement de l'information complète sur le input, le résultat, et n'importe quels résultats intermédiaires. Dans ce travail-ci, on demande ce que ça voudrait dire d'exécuter un programme sur de l'information partielle. Comme réponse possible, on introduit l'interprétation partielle, notre contribution principale. Au lieu de considérer un seul input, on considère un ensemble de inputs possibles. Au lieu de calculer un seul résultat, on calcule un ensemble de résultats possibles, et des ensembles de résultats intermédiaires possibles. On approche l'interprétation partielle à partir du problème de la spécialisation de programme: l'optimisation d'un programme pour certains inputs. Faire ça automatiquement porte historiquement le nom d'évaluation partielle. Ç'a été appliqué avec succès à plusieurs problèmes spécifiques. On croit que ça devrait être un outil de programmation commun, pour spécialiser des librairies générales pour usage spécifique - mais ce n'est pas le cas. Souvent, une implantation donnée de l'évaluation partielle ne fonctionne pas uniformément bien sur tous les programmes. Ça se prête mal à un usage commun. On voit ce manque de régularité comme un problème de précision: si l'évaluateur partiel était très précis, il trouverait la bonne spécialisation, indépendamment de notre style de programme. On propose donc une approche de principe à l'évaluation partielle, visant la précision complète, retirée d'exemples particuliers. On reformule l'évaluation partielle pour la baser sur l'interprétation partielle: le calcul sur de l'information partielle. Si on peut déterminer ce qu'on sait sur chaque donnée dans le programme, on peut décider quelles opérations peuvent être éliminées pour spécialiser le programme: les opérations dont le résultat est unique. On définit une représentation d'ensembles qui ressemble à la définition en compréhension, en mathématiques. On modifie un interpréteur pour des programmes fonctionnels, pour qu'il calcule sur ces ensembles. On utilise un solver SMT pour réaliser les opérations sur les ensembles. Pour assurer la terminaison de l'interpréteur modifié, on applique des idées de l'interprétation abstraite: le calcul de point fixe, et le widening. Notre implantation initiale produit de bons résultats, mais elle est lente pour de plus gros exemples. On montre comment l'accélérer mille fois, en dépendant moins de SMT. / We are used to the following picture of an executing program: an input is provided, the program runs for a while, and a result comes out. We tacitly assume complete information about the input, the result, and any intermediate results in between. In this work, we ask what it would mean to execute a program over partial information. As a possible answer, we introduce partial interpretation, our main contribution. Instead of considering a unique input, we consider a set of possible inputs. Instead of computing a unique result, we compute a set of possible results, and sets of possible intermediate results. We approach partial interpretation from the problem of program specialization: the optimization of a program's execution time for certain inputs. Doing this automatically is historically known as partial evaluation. Partial evaluation has been applied successfully to many specific problems. We believe it should be a mainstream programming tool, to specialize general libraries for specific use - but such a tool has not been delivered. One common problem is that a given implementation of partial evaluation is inconsistent: it does not work uniformly well on all input programs. This inconsistency makes it unsuited for mainstream use. We view this inconsistency as an accuracy problem: if the partial evaluator was very accurate, it would find the correct specialization, no matter how we present the input program. We therefore propose a principled approach to partial evaluation, aimed at complete accuracy, removed from any particular example program. We reformulate partial evaluation to root it in partial interpretation: computation over partial information. If we can determine what we know about every piece of data in the program, we can decide which operations can be removed to specialize the program: those operations whose result is uniquely known. We represent sets with a kind of mathematical set comprehension. We modify an interpreter for functional programs, to compute over these sets. We use an SMT solver (Satisfiability Modulo Theories) to perform set operations. To ensure termination of the modified interpreter, we apply ideas from abstract interpretation: fixed point computation, and widening. Our initial implementation produces good results, but it is slow for larger examples. We show how to speed it up a thousandfold, by relying less on SMT.

Le langage de programmation Python est aujourd'hui parmi les plus populaires au monde grâce à son accessibilité ainsi que l'existence d'un grand nombre de librairies standards. Paradoxalement, Python est également reconnu pour ses performances médiocres lors de l'exécution de nombreuses tâches. Ainsi, l'écriture d’implémentations efficaces du langage est nécessaire. Elle est toutefois freinée par la sémantique complexe de Python, ainsi que par l’absence de sémantique formelle officielle. Pour régler ce problème, nous présentons une sémantique formelle pour Python axée sur l’implémentation de compilateurs optimisants. Cette sémantique est écrite de manière à pouvoir être intégrée et analysée aisément par des compilateurs déjà existants. Nous introduisons également semPy, un évaluateur partiel de notre sémantique formelle. Celui-ci permet d'identifier et de retirer automatiquement certaines opérations redondantes dans la sémantique de Python. Ce faisant, semPy génère une sémantique naturellement plus performante lorsqu'exécutée. Nous terminons en présentant Zipi, un compilateur optimisant pour le langage Python développé avec l'assistance de semPy. Sur certaines tâches, Zipi offre des performances compétitionnant avec celle de PyPy, un compilateur Python reconnu pour ses bonnes performances. Ces résultats ouvrent la porte à des optimisations basées sur une évaluation partielle générant une implémentation spécialisée pour les cas d'usage fréquent du langage. / Python is among the most popular programming language in the world due to its accessibility and extensive standard library. Paradoxically, Python is also known for its poor performance on many tasks. Hence, more efficient implementations of the language are required. The development of such optimized implementations is nevertheless hampered by the complex semantics of Python and the lack of an official formal semantics. We address this issue by presenting a formal semantics for Python focussed on the development of optimizing compilers. This semantics is written as to be easily reusable by existing compilers. We also introduce semPy, a partial evaluator of our formal semantics. This tool allows to automatically target and remove redundant operations from the semantics of Python. As such, semPy generates a semantics which naturally executes more efficiently. Finally, we present Zipi, a Python optimizing compiler developped with the aid of semPy. On some tasks, Zipi displays performance competing with those of PyPy, a Python compiler known for its good performance. These results open the door to optimizations based on a partial evaluation technique which generates specialized implementations for frequent use cases.