Formalization in Coq of the standardization theorem for λ-calculus

Abstract

Os teoremas da standardização são resultados fundamentais da teoria da redução do Cálculo-λ. Estes resultados estabelecem que um termo t reduz para um termo t′ se e só se t reduz para t′ seguindo uma sequência de redução específica, dita standard. Em particular, estes resultados garantem a completude de certas maneiras específicas de efetuar reduções, e são a base dos resultados sobre estratégias de avaliação, nomeadamente chamada-por-nome e chamada-por-valor, fazendo a ponte entre um cálculo (uma teoria equacional) e uma linguagem de programação. Esta dissertação apresenta uma formalização no sistema de prova assistida Coq do Teorema da Standardização para o Cálculo-λ. Neste sentido, consideramos uma prova deste resultado que extraímos de uma prova de um Teorema da Standardização para um cálculo-λ para lógica modal proposto por Espírito Santo-Pinto-Uustalu, onde redução standard é capturada através de uma relação definida indutivamente nos termos-λ, em linha com tratamentos de standardização para o Cálculo-λ por Loader e por Joachimski Matthes. A implementação da sintaxe dos termos-λ usa os índices de De Bruijn, mas a formalização Coq segue de muito perto a estrutura da prova do Teorema da Standardização (com termos-λ ordinários). Adicionalmente, esta dissertação considera uma noção independente de sequência de redução stan dard para o Cálculo-λ estudada por Plotkin. Por um lado, provámos que sequências de redução e a abordagem inicial de redução standard como uma relação indutiva nos termos-λ são formas equivalentes de caracterizar redução standard e, por outro, fornecemos uma formalização dessa equivalência em Coq.

Standardization theorems are fundamental results in the theory of reduction of λ-calculus. They es tablish that a term t reduces to a term t ′ if and only if t reduces to t ′ following some specific sequence of reductions said standard. In particular, these results guarantee completeness of specific ways of per forming reduction, and are at the basis of results about evaluation strategies, namely call-by-name and call-by-value, bridging between calculi (equational theories) and programming languages. This dissertation presents a formalization in the Coq proof assistant of the Standardization Theorem for the call-by-name version of λ-calculus, i.e. ordinary λ-calculus. In this development, we consider a proof of this result that we extracted from a proof of a standardization theorem for a λ-calculus for modal logic Espírito Santo-Pinto-Uustalu, where standard reduction is captured via an inductively defined relation on λ-terms, in line with treatments of standardization for λ-calculus by Loader and Joachimski-Matthes. The implementation of the λ-terms syntax uses the De Bruijn indices, but the Coq formalization follows closely the structure of the proof of the Standardization Theorem (with ordinary λ-terms), both in what concerns lemmata and the inductive structure of arguments. Additionally, this dissertation also considers an independent notion of standard reduction sequence for (call-by-name) λ-calculus studied by Plotkin. Firstly, we prove that reduction sequences and the approach of standard reduction as an inductive relation on λ-terms are indeed equivalent ways of characterizing standard reduction. Then, we provide a complete formalization in Coq of this equivalence.