Biblioteca Digital | FCEN-UBA

Biblioteca Digital ¿Por qué?
Objetivos
Impactos
Estadísticas
Documentos
Presentaciones
Notas
Autores y derechos
¿Por qué depositar?
¿Cómo depositar?
Autorización
Depositar y publicar
Editoriales
Publicar mi tesis Formulario Tesis Posgrado
Formulario Tesis Grado
Normativa
Res. CD 2053/05
Res. CD 2533/09
Res. CD 0272/13
Res. CD 2793/15

Colecciones Tesis Doctorales
Fotografías
Publicaciones
Archivo
Libros
Reportes Técnicos

Tesis > TEMA

Computación [ 80 tesis ]

Lenguajes y Sistemas Informáticos [ 2 tesis ]

Bonelli, Eduardo. "Reescritura de términos y sustituciones explícitas" (2003) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
La operación de sustitución constituye un engranaje básico en los fundamentos de la teoría de lenguajes de programación. Juega un rol central en el lambda cálculo (por ende, en lenguajes de programación funcional), en unificación de primer orden y de orden superior (por ende, en lenguajes de programación basados en el paradigma lógico), en modalidades de pasaje de parámetros (por ende, en lenguajes de programación imperativos), etc. Recientemente, investigadores en informática se han interesado en el pasaje de la noción usual de la sustitución, atómica, y de gruesa granularidad, hacia una noción más refinada, de más fina granularidad. La noción de sustitución es transportada del metalenguaje (nuestro lenguaje de discurso) al lenguaje objeto (nuestro lenguaje de estudio). Como consecuencia de ello se obtienen los llamados cálculos de sustituciones explícitas. Estos son de sumo interés a la hora de estudiar la interpretación operacional de los formalismos en cuestión y constituyen los objetos de interés de esta tesis. Se desarrollan los siguientes tres ejes de estudio: Primero, se consideran estrategias de reescritura perpetuas en lambda cálculos con sustituciones explícitas. Estas son estrategias de reescritura que preservan la posibilidad de reducciones infinitas. Se propone una caracterización inductiva del conjunto de términos que no poseen reducciones infinitas (los llamados fuertemente normalizantes). Un lambda cálculo polimórfico con sustituciones explícitas también es analizado, incluyendo propiedades tales como subject reduction y normalización fuerte. Segundo, colocamos el ς-cálculo de M. Abadi and L. Cardelli enriquecido con sustituciones explícitas bajo el microscopio. Este cálculo se encuentra en un nivel semejante de abstracción al lambda cálculo pero se basa en objetos en lugar de funciones. Propiedades tales como simulación del lambda cálculo, confluencia y preservación de la normalización fuerte (aquellos términos que son fuertemente normalizantes en ς también lo son en ς con sustituciones explícitas) son consideradas. Finalmente, dirigimos nuestra atención a la tarea de relacionar la reescritura de orden superior con aquella de primer orden. Fijamos una variante de los ERS (apodados SERSdb) de Z. Khasidashvili como nuestro formalismo de orden superior de partida y definimos un proceso de conversión que permite codificar cualquier SERSdb como un sistema de reescritura de primer orden. En este último, cada paso de reescritura se lleva a cabo módulo una teoría ecuacional determinada por un cálculo de sustituciones explícitas. La misma se formula de manera genérica a través de una presentación de cálculos de sustituciones explícitas basada en macros y axiomas sobre estas macros, parametrizando de esta manera al procedimiento de conversión sobre cualquier cálculo de sustituciones explícitas que obedece la presentación basada en macros. El procedimiento de conversión se encarga de codificar pattern matching de orden superior y sustitución en el entorno de reescritura de primer orden. Asimismo, propiedades que relacionan la noción de reescritura en el orden superior con aquella de primer orden son analizadas en detalle. Se identifica una clase de SERSdb para los cuales el sistema de primer orden resultante de su conversión no requiere una teoría ecuacional para implementar pattern matching de orden superior, bastando para ello matching sintáctico. También se argumenta que esta clase de sistemas de orden superior es apropiada para transferir resultados del entorno de reescritura de orden superior a aquella de primer orden. A modo de ejemplo no-trivial de ello, estudiamos la transferencia del teorema de standarización (fuerte).

Abstract:
Substitution spans many areas in programming language theory. It plays a central role in the lambda calculus (hence functional programming), in first and higher-order unikation (hence logic programming), parameter passing methods (hence imperative programming), etc. Recently researchers became interested in shifting from the usual atomic, coarse grained view of substitution to a more refined, fine grained one. Substitution is promoted from the metalevel (our language of discourse) to the object-level (our language of study). This is interesting when studying the operational interpretation of the formalisms in question. Calculi of object-level or explicit substitution is the concern of this thesis. The following three study axes are developed. First we consider perpetual rewrite strategies in lambda calculi of explicit substitutions. These are rewrite strategies that preserve the possibility of inhite derivations. Also, we study how to characterize inductively the set of terms that do not possess infinite derivations (the strongly normalizing terms). Polymorphic lambda calculus with explicit substitutions shall receive our attention too, including properties such as subject reduction and strong normalization. Secondly, we put the ς-calculus of M.Abadi and L.Cardelli augmented with explicit substitutions under the microscope. This calculus is at the level of the lambda calculus but is based on objects instead of functions. Properties such as simulation of the lambda calculus, confluence and preservation of strong normalization (terms which are strongly normalizing in ς are also strongly normalizii in ς with explicit substitutions) are considered. Finally, we address the task of reducing higher-order rewriting to first-order rewriting. We fix a variant of Z-Khasidashvili's ERS (dubbed SERSdb) as our departing formalism and provide a conversion procedure to encode any ERS as a first-order rewrite system in which a rewrite step takes place modulo an equational theory determined by a calculus of explicit substitutions. The latter is achieved with the aid of a macro-based presentation of calculi of explicit substitutions, thus parametrizing the conversion procedure over any calculus of explicit substitutions in compliance with the aforementioned presentation. The conversion procedure is in charge of encoding higherorder pattern matching and substitution in the first-order framework. Properties relating the rewrite relation in the higher-order framework and that of the resulting first-order system are studied in detail. We then identify a class of SERSdb for which the resulting first-order system does not require the equational theory to implement higher-order pattern matching, thus contenting itself with syntactic matching. It is argued that this class of systems is appropriate for transferring results from the first-order framework to the higher-order one. As a non-trivial example we study the transfer of the (strong) standardization theorem.

Moscato, Mariano Miguel. "Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving" (2013) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
El análisis formal de especificaciones de software suele atacarse desde dos enfoques, usualmente llamados: liviano y pesado. En el lado liviano encontramos lenguajes fáciles de aprender y utilizar junto con herramientas automáticas de análisis, pero de alcance parcial. El lado pesado nos ofrece lograr certeza absoluta, pero a costo de requerir usuarios altamente capacitados. Un buen representante de los métodos livianos es lenguaje de modelado Alloy y su analizador automático: el Alloy Analyzer. Su análisis consiste en transcribir un modelo Alloy a una fórmula proposicional que luego se procesa utilizando SAT-solvers estándar. Esta transcripción requiere que el usuario establezca cotas en los tamaños de los dominios modelados en la especificación. El análisis, entonces, es parcial, ya que está limitado por esas cotas. Por ello, puede pensarse que no es seguro utilizar el Alloy Analyzer para trabajar en el desarrollo de aplicaciones críticas donde se necesitan resultados concluyentes. En esta tesis presentamos un cálculo basado en álgebras de Fork que permite realizar demostraciones en cálculo de secuentes sobre especificaciones Alloy. También hemos desarrollado una herramienta (Dynamite) que lo implementa. Dynamite es una extensión del sistema de demostración semiatomático PVS, método pesado ampliamente utilizado por la comunidad. Así, Dynamite consigue complementar el análisis parcial que ofrece Alloy, además de potenciar el esfuerzo realizado durante una demostración usando el Alloy Analyzer para detectar errores tempranamente, refinar secuentes y proponer términos para utilizar como testigos de propiedades cuantificadas existencialmente.

Abstract:
Formal analysis of software models can be undertaken following two approaches: the lightweight and the heavyweight. The former offers languages with simple syntax and semantics, supported by automatic analysis tools. Nevertheless, the analysis they perform is usually partial. The latter provides full confidence analysis of models, but often requires interaction from highly trained users. Alloy is a good example of a lightweight method. Automatic analysis of Alloy models is supported by the Alloy Analyzer, a tool that translates an Alloy model to a propositional formula that is then analyzed using off- the-shelf SAT-solvers. The translation requires user-provided bounds on the sizes of data domains. The analysis is limited by the bounds, and is therefore partial. Thus, the Alloy Analyzer may not be appropriate for the analysis of critical applications where more conclusive results are necessary. In this thesis we develop Dynamite, an extension of PVS that embeds a complete calculus for Alloy. PVS is a well-known heavyweight method. It provides a semi-automatic theorem prover for higher order logic. Dynamite complements the partial automatic analysis offered by the Alloy Analyzer with semi-automatic verification through theorem proving. It also improves the theorem proving experience by using the Alloy Analyzer to provide automatic functionality intended for early detection of errors, proof refinement and witness generation for existentially quantified properties.

http://digital.bl.fcen.uba.ar

Biblioteca Central Dr. Luis Federico Leloir - Facultad de Ciencias Exactas y Naturales - Universidad de Buenos Aires
Intendente Güiraldes 2160 - Ciudad Universitaria - Pabellón II - C1428EGA - Tel. (54 11) 4789-9293 int 34