Science, Faculty of
Computer Science, Department of
DSpace
UBCV
Xu, Junfeng
Master of Science - MSc
University of British Columbia
When defining the syntax and semantics of programming languages, computer scientists often use some kind of computer science metanotations. These metanotations are often informal or under-defined: human readers can understand them intuitively, but they are unsuitable for use in rigorous formal proofs. The aim of this project is to develop a tool that bridges the gap between the intuitive metanotations for defining programming languages, and proof assistant languages in which properties of the languages defined can be formally proven. In this thesis, I present Redex-Plus, an implementation of a computer science metanotation based on the Racket language Redex, which is used to define programming language models. Redex-Plus is a compiler that translates language models defined in the Redex language to corresponding definitions in various proof assistant languages. Redex-Plus also generates boilerplate such as binding operations, saving the users from the tedious job of writing boilerplate by hand. Redex-Plus supports Coq, Agda, SMT-LIB, and Beluga as translation targets; it can faithfully translate language models with multiple types of bound variables; and it gives users the choice between multiple ways to represent variable binding when using the Coq or Agda targets. I evaluate Redex-Plus by formalizing a variant of Simply Typed Lambda Calculus and proving some important properties of the language model in both Coq and Agda, and by formalizing a variant of System F and attempting to prove the same properties in Coq. The source code repository of Redex-Plus is publicly available at https://gitlab.com/xujunfeng/redex-plus , and on Zenodo.
REDEX-PLUS:A Metanotation for Programming LanguagesbyJunfeng XuB.Eng., Imperial College London, 2019A THESIS SUBMITTED IN PARTIAL FULFILLMENTOF THE REQUIREMENTS FOR THE DEGREE OFMaster of ScienceinTHE FACULTY OF GRADUATE AND POSTDOCTORALSTUDIES(Computer Science)The University of British Columbia(Vancouver)August 2023© Junfeng Xu, 2023The following individuals certify that they have read, and recommend to the Fac-ulty of Graduate and Postdoctoral Studies for acceptance, the thesis entitled:REDEX-PLUS:A Metanotation for Programming Languagessubmitted by Junfeng Xu in partial fulfillment of the requirements for the degreeof Master of Science in Computer Science.Examining Committee:William Bowman, Professor, Computer Science, UBCSupervisorRonald Garcia, Professor, Computer Science, UBCSupervisory Committee MemberiiAbstractWhen defining the syntax and semantics of programming languages, computer sci-entists often use some kind of computer science metanotations. These metano-tations are often informal or under-defined: human readers can understand themintuitively, but they are unsuitable for use in rigorous formal proofs. The aim ofthis project is to develop a tool that bridges the gap between the intuitive metanota-tions for defining programming languages, and proof assistant languages in whichproperties of the languages defined can be formally proven.In this thesis, I present REDEX-PLUS, an implementation of a computer sci-ence metanotation based on the Racket language Redex, which is used to defineprogramming language models. REDEX-PLUS is a compiler that translates lan-guage models defined in the Redex language to corresponding definitions in var-ious proof assistant languages. REDEX-PLUS also generates boilerplate such asbinding operations, saving the users from the tedious job of writing boilerplate byhand. REDEX-PLUS supports Coq, Agda, SMT-LIB, and Beluga as translationtargets; it can faithfully translate language models with multiple types of boundvariables; and it gives users the choice between multiple ways to represent vari-able binding when using the Coq or Agda targets. I evaluate REDEX-PLUS byformalizing a variant of Simply Typed Lambda Calculus and proving some impor-tant properties of the language model in both Coq and Agda, and by formalizing avariant of System F and attempting to prove the same properties in Coq.The source code repository of REDEX-PLUS is publicly available at https://gitlab.com/xujunfeng/redex-plus, and on Zenodo [41].iiiLay SummaryWhen reasoning about programming languages, computer scientists use metano-tations to state how the programming languages look and behave. However, thesemetanotations are often informal, and cannot be used in formal, rigorous, math-ematical proofs. In this thesis I present REDEX-PLUS, a tool that translates pro-gramming language definitions written using a certain metanotation into code thatcan be used in formal proofs. I also demonstrate REDEX-PLUS’s usefulness byusing it to translate the definition of a certain well-known programming languageinto code, and then using the translated code to prove some important properties ofthe programming language in question.ivPrefaceThis thesis presents original, unpublished work by the author Junfeng Xu under thesupervision of Professor William Bowman.REDEX-PLUS, the tool presented in this thesis, is based on the Racket libraryRedex. The SMT-LIB translation target (see section 4.2.3) was developed as theauthor’s personal project for the CPSC 513 course. The proofs in section 7.2 arebased on similar proofs in the books Programming Language Foundations in Agdaand Software Foundations.vTable of ContentsAbstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iiiLay Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ivPreface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vTable of Contents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . viList of Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ixList of Figures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xAcknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xiv1 Introduction: Who Formalizes the Formalization? . . . . . . . . . . 11.1 “The Most Popular Programming Language” . . . . . . . . . . . 11.2 Dreaming of a Computer Science Metanotation . . . . . . . . . . 21.3 REDEX-PLUS . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41.3.1 Structure of this Thesis . . . . . . . . . . . . . . . . . . . 52 Background: Existing Metanotation Implementations . . . . . . . . 62.1 Ott . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.1.1 LNgen . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.2 Lem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82.3 Spoofax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9vi3 REDEX-PLUS: A Computer Science Metanotation . . . . . . . . . . 103.1 Redex . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103.1.1 A Basic Example . . . . . . . . . . . . . . . . . . . . . . 123.1.2 Problems with Translating Redex . . . . . . . . . . . . . 143.2 The Supported Redex Subset . . . . . . . . . . . . . . . . . . . . 184 Translating Language Models, and Generating Code . . . . . . . . . 224.1 Language Models to Intermediate Representation . . . . . . . . . 234.1.1 Poultry: The Intermediate Representation . . . . . . . . . 234.1.2 From Redex To Poultry . . . . . . . . . . . . . . . . . . . 254.2 Generating Code . . . . . . . . . . . . . . . . . . . . . . . . . . 354.2.1 Dependently Typed Proof Assistants . . . . . . . . . . . . 364.2.2 Beluga . . . . . . . . . . . . . . . . . . . . . . . . . . . 404.2.3 SMT-LIB . . . . . . . . . . . . . . . . . . . . . . . . . . 415 Variable Binding: Representation & Implementation . . . . . . . . 435.1 Named . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 445.1.1 Determining when to Generate Binding Operations . . . . 475.1.2 Variable Capturing . . . . . . . . . . . . . . . . . . . . . 475.2 Locally Nameless . . . . . . . . . . . . . . . . . . . . . . . . . . 495.3 Shifted Names . . . . . . . . . . . . . . . . . . . . . . . . . . . . 525.4 Higher-Order Abstract Syntax . . . . . . . . . . . . . . . . . . . 546 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 576.1 Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 576.2 Internal Workings . . . . . . . . . . . . . . . . . . . . . . . . . . 586.3 The Compilation Passes . . . . . . . . . . . . . . . . . . . . . . . 596.4 Adding New Translation Targets . . . . . . . . . . . . . . . . . . 627 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 657.1 Automatic Code Generation . . . . . . . . . . . . . . . . . . . . 657.1.1 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . 677.2 Properties of the Simply Typed Lambda Calculus . . . . . . . . . 687.2.1 Progress . . . . . . . . . . . . . . . . . . . . . . . . . . . 72vii7.2.2 Preservation of Types under Substitution . . . . . . . . . 727.2.3 Preservation . . . . . . . . . . . . . . . . . . . . . . . . . 737.2.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . 757.3 Unsuccessful Proof Attempts . . . . . . . . . . . . . . . . . . . . 767.3.1 Properties of STLC using the Locally Nameless Binding . 767.3.2 Properties of System F . . . . . . . . . . . . . . . . . . . 767.4 Automatic Solving with SMT Solvers . . . . . . . . . . . . . . . 777.4.1 Limitations of SMT Solvers . . . . . . . . . . . . . . . . 778 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 828.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 828.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85A Evaluation Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90A.1 Coq Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91A.1.1 Progress . . . . . . . . . . . . . . . . . . . . . . . . . . . 91A.1.2 Auxiliary Lemmas for Substitution Lemma . . . . . . . . 91A.1.3 Substitution Lemma . . . . . . . . . . . . . . . . . . . . 95A.1.4 Preservation . . . . . . . . . . . . . . . . . . . . . . . . . 96A.2 Agda Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97A.2.1 Progress . . . . . . . . . . . . . . . . . . . . . . . . . . . 97A.2.2 Auxiliary Lemmas for Substitution Lemma . . . . . . . . 97A.2.3 Substitution Lemma . . . . . . . . . . . . . . . . . . . . 99A.2.4 Preservation . . . . . . . . . . . . . . . . . . . . . . . . . 100viiiList of TablesTable 6.1 Compilation passes for all REDEX-PLUS statements and tar-gets. “©” means this pass is a part of the translation processfor the target; “|” means it is not; “4” means it depends onuser setting; “⊕” means only one of the passes marked as so isincluded, depending on user settings; and “×” means this state-ment is not supported by the target. The targets (Coq, Agda,Beluga, and SMT-LIB) are abbreviated to their initial letters. . 63Table 7.1 Breakdown of the amount of generated code, in terms of linesof code. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66ixList of FiguresFigure 3.1 The Redex language definition for the F language. . . . . . . . 13Figure 3.2 Additional metafunction and judgement form definitions usedto define the typing relation in the F language. . . . . . . . . . 14Figure 3.3 The typing judgement and reduction relation for the F language. 15Figure 3.4 Racket code for generating the list of derivations (ds) and dis-playing them. Only one derivation is shown as in this examplethere is only one possible derivation. . . . . . . . . . . . . . . 16Figure 3.5 Pattern language supported by REDEX-PLUS. . . . . . . . . . 19Figure 4.1 The Tree language model. . . . . . . . . . . . . . . . . . . . 22Figure 4.2 Using for-language to separate statements belonging to dif-ferent Redex languages. . . . . . . . . . . . . . . . . . . . . 24Figure 4.3 Defining a binary tree type with define-types. . . . . . . . . 26Figure 4.4 The Redex metafunction that mirrors a binary tree. . . . . . . 26Figure 4.5 The generated IR of the statement in figure 4.4, with all argu-ments annotated. All user-defined metafunctions will have thelanguage name prefixed to the function name. . . . . . . . . . 27Figure 4.6 The Redex metafunction that compares two binary trees. Thefirst case, which returns true, is only matched when both ar-guments are syntactically the same. If they are not, then thefunction falls back to the second case and returns false. . . . . 28Figure 4.7 The IR of the same-tree function definition. Notice the #:ifexpression inside the top level #:match, in which the two ar-guments are compared. . . . . . . . . . . . . . . . . . . . . . 29xFigure 4.8 The function body of same-tree after simplification. . . . . . 29Figure 4.9 The Redex judgement representing the “less-than” relation be-tween Peano numbers. . . . . . . . . . . . . . . . . . . . . . 30Figure 4.10 The generated IR of the statement in figure 4.9. The first twoarguments of define-proposition declares the name and sig-nature, in terms of type names, of the judgement. A list ofrules follows, in which each rule contains a list of (implicitly)bound variables used in the rule, the judgement constructed bythe rule, and a potentially empty (in the case of axioms) listof premises. The #:term keyword helps the later translationprocess distinguish judgement forms from terms. . . . . . . . 30Figure 4.11 The Redex definition of β -reduction in System F. . . . . . . . 31Figure 4.12 The function definition corresponding to the subst reductioncase. The argument type (#:well-bound e) means an e thathas a type-level guarantee of its well-boundedness. The well-boundedness requirement is only relevant when using bind-ing representations that can express well-boundedness, suchas shifted names. When using other binding representations,the requirement is ignored. . . . . . . . . . . . . . . . . . . . 32Figure 4.13 β -reduction of System F represented as a proposition. . . . . 33Figure 4.14 Compatible closure of β -reduction of System F represented asa proposition; abridged. . . . . . . . . . . . . . . . . . . . . . 34Figure 4.15 The Coq definition of a binary tree generated by REDEX-PLUS 37Figure 4.16 The “less than” relation defined in figure 4.9 translated intoCoq, and the associated autoderive definitions. . . . . . . . 39Figure 4.17 Proving that a natural number is less than itself plus two byinduction on natural numbers. Both induction cases can betrivially solved by autoderive. . . . . . . . . . . . . . . . . 39Figure 4.18 The Agda definition of a binary tree, as well as the “less than”relation between Peano numbers. . . . . . . . . . . . . . . . . 40Figure 4.19 System F represented in Beluga. The natural number type natis defined in the prelude. . . . . . . . . . . . . . . . . . . . . 41xiFigure 5.1 The Coq definition of the system F language using the namedbinding representation. . . . . . . . . . . . . . . . . . . . . . 45Figure 5.2 The Coq definition of substitution of type variables in expres-sions in System F. This is a part of a larger definition that alsodefines substitution of e in e and substitution of t in t. . . . . 46Figure 5.3 Binding relations in System F. . . . . . . . . . . . . . . . . . 47Figure 5.4 A Coq example of variable capturing during substitution. . . . 48Figure 5.5 The Coq definition of the LN variable type. . . . . . . . . . . 50Figure 5.6 The Coq definition of the system F language. . . . . . . . . . 50Figure 5.7 The Coq code generated for the LN operation “open t in e”.Notice that 1) since this operation is about type variables (vari-ables in the F_t type), the F_var constructor for term variablesis not affected despite it taking a variable as an argument, 2)because a type variable is bound in F_tlam, the binding level kis incremented in the recursive call, and 3) since F_lam binds aterm variable rather than a type variable, the binding levels arenot changed in recursive calls. . . . . . . . . . . . . . . . . . 52Figure 5.8 The Church boolean “true” written using LN operations andnamed variables. It is equal to church_true_bound, writtendirectly using de Bruijn indexing in bound variables. . . . . . 53Figure 5.9 The Redex definition and its corresponding Coq translationof the “abstract” typing rule, for λ -abstractions, in System F.Here v__a, the name of the variable bound in F_lam, is a string. 53Figure 5.10 The Coq definition of simply typed λ -calculus using shiftednames. Note that the type of second argument to STLC_lamhas (S V) instead of just V as its level argument. . . . . . . . 55Figure 5.11 The Beluga definition of simply typed λ -calculus using HOAS.Notice that the constructor for term variable has been removed. 56Figure 6.1 require’ing the REDEX-PLUS library, configuring it, and us-ing it to define system F. . . . . . . . . . . . . . . . . . . . . 58xiiFigure 7.1 Breakdown of the amount of generated code, in terms of linesof code. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67Figure 7.2 The Redex language definition of STLC and β -reduction. . . . 68Figure 7.3 The Redex definition of the typing judgement in STLC. . . . . 70Figure 7.4 Notation definitions for STLC, in Coq and Agda. . . . . . . . 71Figure 7.5 Definitions of β -reduction and the associated notation in Coqand Agda. The rule for reducing the body of an lambda ab-straction has been removed, and the left sub-expression of afunction application is not required to be a value before theright sub-expression could reduce. . . . . . . . . . . . . . . . 74Figure 7.6 The Redex definition of the a simple arithmetic expression lan-guage and its reduction relation. . . . . . . . . . . . . . . . . 78Figure 7.7 SMT-LIB code for proving two reduction relations. The “push”and “pop” commands are for delimiting each of the two proofs. 79Figure 7.8 SMT-LIB code for finding what the expression (add 1 1) re-duces to, and the Z3 output from running the code. Notice thatthe model Z3 came up with states that Arith-eval-single-stepis always true (i.e. every term reduces to every other term),and Arith-eval is true as long as the reduction result is zeroor two, which are both clearly nonsensical. . . . . . . . . . . 80Figure 7.9 The Redex definition of natural numbers and two relations. . . 81Figure 7.10 SMT-LIB code for checking the correctness of two simple the-orems about natural numbers. . . . . . . . . . . . . . . . . . 81xiiiAcknowledgmentsFirst and foremost, I would like to thank Professor William Bowman, my supervi-sor, for guiding me through not only the REDEX-PLUS project but also my life asa graduate student.I would also like to thank Professor Ronald Garcia for his valuable commentson this thesis.Last but not least, I would like to thank Paulette Koronkevich for her adviceon writing proofs, and to thank Professor Margo Seltzer, and my friends Emily,Fangyi Zhou, and Molly, for their support throughout my journey.xivChapter 1IntroductionWho Formalizes the Formalization?1.1 “The Most Popular Programming Language”To study programming languages (PL), we often first formalize them. Usually,this means using a terse, unambiguous abstract notation to represent an existinglanguage, or to define a new language. Then, we give this abstract notation ameaning using a set of well-defined mathematical rules.To do so, researchers rely on some metanotations: the notations used to de-fine and specify programming languages. These metanotations are not monolithicproducts of some conscious design process. Instead, they are conglomerates con-sisting of many notations with origins in computer science and logics. For ex-ample, Backus-Naur Form (BNF), originally used to describe the concrete syntaxof ALGOL [4], is commonly used for defining the abstract syntax of languages;and Gentzen’s syntax for derivation rules [22] is used for inferring properties oflanguage terms.Despite the diversity of the metanotations, they are used to accomplish similarsets of goals. In existing PL literature and related tools, people use these metano-tations to:• define a formal syntax of a language, with either BNF, or more commonly,1one of the extended variants of BNF.• designate some terms as “variables”, and to safely substitute a variable witha term;• define a reduction semantics for the language, that describes how one lan-guage term can be “reduced” or “evaluated” to another. Often, the order ofreduction is also defined; and• reason about and prove properties of terms, usually by incorporating thelanguage into a logical representation, such as first-order logic.The wide usage of such metanotations led Guy Steele to call them “the mostpopular programming language” in a 2017 lecture [39]. However, as Steele argued,the metanotations used for formalizing programming languages have, ironically,not received enough formal examination themselves. One significant issue is theinconsistent use of notations: a survey carried out by Steele and his students iden-tified 28 ways to express substitution, including a pair of notations that mean theopposite thing, but are impossible to distinguish by their appearances [39]. He alsomentioned some problems with using overlines to mark repetition.This frustration with the state of metanotations is what led me to write down“who formalizes the formalization?” as the subtitle of this chapter. It may be truethat the inconsistencies highlighted in Steele’s talk do not do hinder PL research.Yet, I still believe we can do better, by bringing a more precise, more consistentmetanotation into existence.1.2 Dreaming of a Computer Science MetanotationIn the aforementioned lecture, Steele suggested that we make Computer ScienceMetanotation (CSM) “an explicit object of study”: we should formalize CSM, justlike we formalize other languages [39]. This is perhaps not a very difficult task:we can incorporate existing formal definitions for CSM elements such as BNF,capture-free substitution, and reduction semantics into a coherent, standardizedCSM, so that when researchers try to define their languages, they can use thisstandardized metanotation.2However, Steele’s outlook has a second component: he suggests that we shouldalso build compilers and other tools for CSM [39], just like we build these tools forother languages. This poses a far greater challenge: many concepts and propertiestrivial to express in human language are difficult to put into precise, mechanicalterms. Name binding and capture-free substitution are perhaps the poster childrenof this difficulty, spawning a number of wildly different solutions to their model-ing, including de Bruijn’s “namefree” expression [14], higher-order abstract syntax(HOAS) [31], and abstract binding trees [23, p. 6-11].When implementing a “compiler” for CSM, it may be tempting to target proofassistants such as Coq, as they are often used by PL researchers to reason abouttheir languages formally. Unfortunately, the intersection of CSM and proof assis-tants brings more challenges. In order to express, for example, substitution, theusers need to write the entire substitution function by hand in the proof assistantlanguage. The tedious task of writing language-specific boilterplates not only dis-tracts the users from more worthwhile tasks, but also immobilizes them, by tyingthe abstract syntax of a language to a particular proof assistant implementation,and to one particular representation of variable binding. Tying the CSM to any par-ticular proof assistant may also drive away users who are more familiar with othertools, or wish to approach the same problem with different underlying theories.There are already many tools that meet many of Steele’s objectives, but fallshort of the others. Some, like Ott [38] and Lem [30], handle “compliation” toproof assistants and LATEX well, but do not provide expressive binding representa-tions. Spoofax [24] and Redex [20, 26] can model complex semantics and reduc-tion rules, but offers limited supports for formal proofs. Perhaps, the lack of anagreed-upon metanotation is exactly the result of the lack of a well-rounded im-plementation capable of both helping users reason about languages (using formalproofs, for example), and expressing complex language features. The developmentof a CSM implementation that can both express programming languages defini-tions with wide ranges of features, and to translate these language definitions toproof assistants may thus be a crucial step on the way towards a standardized CSM.31.3 REDEX-PLUSLearning from the metanotations in common usage, and past attempts at imple-menting metanotations, the objective of this project is to bridge the gap betweenthe intuitive modeling languages such as the ones people write in LATEX, and theirimplementation as proof assistant code.In this thesis, I present REDEX-PLUS, a CSM implementation. Built upon theRedex library (see section 3.1), REDEX-PLUS translates programming languagemodels written in Redex into proof assistant code. The main goal is to allow re-searchers to define language models, which includes the syntax, reduction rules,and properties of a language, in REDEX-PLUS, then use REDEX-PLUS to generateproof assistant definitions of their models as well as associated boilerplate, so thatthey can carry out formal proofs without manually implementing the model in allproof assistants they are using.REDEX-PLUS strives to• be compatible with Redex, so REDEX-PLUS language models are also validRedex models, allowing Redex’s various useful features, such as reductionevaluation, graphical interfaces, and LATEX generation, to remain available toREDEX-PLUS users;• target multiple proof assistants, so a particular model is not tied to one par-ticular proof assistant representation; and to• support multiple representations of variable bindings in generated code. Thedifferences in binding representations have a significant impact on how for-mal proofs about a language are written. By providing multiple binding rep-resentations, the users may choose the ones most suitable for their particularmodels and proofs.REDEX-PLUS is open-sourced under the MIT licence. The code repository ofREDEX-PLUS is publicly available at https://gitlab.com/xujunfeng/redex-plus, andon Zenodo [41].41.3.1 Structure of this ThesisIn chapter 2, I evaluate some existing metanotations, including Redex, and discusswhat we can learn from them. I then introduce the metanotation of REDEX-PLUS,which is a subset of Redex, in chapter 3. After that, I discuss how REDEX-PLUStranslates the Redex subset into different proof assistant languages in chapter 4, andthe various binding representations it supports in chapter 5. In chapter 6 I discusssome implementation details of REDEX-PLUS. Then, I evaluate REDEX-PLUS inchapter 7, and conclude my thesis with chapter 8.5Chapter 2BackgroundExisting Metanotation ImplementationsThere are a number of metanotation implementations that meet many of CSM’sobjectives. Despite the different goals driving the development of these metan-otations, in general, they support BNF-like syntax definitions, and various formsof semantic definitions. Some of them also support “compiling” the definition toother languages.In this chapter, I give a brief description of these metanotations, and evaluatetheir advantages and drawback. Redex, the metanotation implementation REDEX-PLUS is based upon, is explained in further detail in section 3.1.To summarize, these are some of the lessons learned from the existing systems:• For metanotations that can compile to some target languages, the diversityof compilation backends is highly appreciated.• Modelling safe variable binding in the metanotation is not easy. As Ott(section 2.1) shows, implementing binding in an idiomatic way may requiretarget-specific code.• Some features not directly related to language modelling are also useful forusers: support for IDEs and editors, and generation of LATEX code are twosuch examples.62.1 OttOtt is a metalanguage and tool for writing semantic definitions of programminglanguages [38]. Language specifications in Ott can be “compiled” into a varietyof proof assistant languages, including Coq, HOL, and Isabelle, as well as Lem(see section 2.2), and OCaml [37, sec. 1]. Generation of LATEX representations isalso supported. Ott uses a BNF-like syntax for syntax definitions, but allows (andsometimes requires) extra information in the definitions. It also supports relationsas “semantic judgements”, defined in a way similar to Gentzen’s derivation trees.By default, Ott handles binding using a “fully concrete” representation. Theuser specifies the types (usually strings or natural numbers) used to represent vari-ables in the target proof assistant language, and Ott translates variables in the user-defined model into terms of that type. Ott also generates substitution functionsautomatically, according to the binding information in syntax definitions. Thesesubstitution functions are not capture-avoidant, and there is no “notion of alphaequivalence” [37, sec. 5.3]. As the authors showed in case studies, however, Ott isstill able to model many languages, despite the limitations of its binding represen-tation.Ott comes with experimental support for the locally-nameless (see 5.2) bindingrepresentation [37, sec. 11]. An external tool, LNgen (see 2.1.1) can also generatelocally-nameless Coq definitions from Ott code.Among all existing metanotations, Ott fullfils perhaps the largest number ofCSM objectives. However, it lacks a built-in notion of reduction or evaluation, sothe user must define reductions as relations. While Ott’s syntax is largely similar tofunctional programming and CSM definitions, the large amount of necessary anno-tations may clutter the source code. The need to write target-specific annotationsalso distracts the user from working on models.2.1.1 LNgenLNgen is a tool for generating locally nameless (see section 5.2) definitions in Coqfrom Ott source code [2]. It generates not only definitions of binding operationssuch as “open” and “close”, but also dozens of useful binding lemmas as well astheir proofs. LNgen takes a only subset of Ott as its input. Constructors of variable7arity or non-terminals that are subsets of another non-terminals are not supported.It only accepts binding specifications where “a single metavariable binds in a singlenonterminal”.2.2 LemLem is a “language for engineering reusable large-scale semantic models” [30].Like Ott, it supports compilation of language models into Coq, HOL, Isabelle, andalso OCaml. Lem can also serves as a compilation target of Ott [37, sec. 1] (seesection 2.1).An issue Lem aims to solve is “proof-assistant lock-in”: porting language mod-els between proof assistants is difficult, even though the semantics of the modelscan be expressed in all these proof assistants. Lem’s metalanguage, whose syntaxis “similar to that of a functional programming language”, achieved a “balance”between expressiveness and translatability [30], making definitions written in thismetalanguage “reusable”.Another focus of Lem is human-readability of generate code, in which thewhitespaces and comments in the Lem source are preserved, so that the layoutof the generated code matches the original. Like Ott, Lem can also target LATEX,preserving “typeset layout” in the generate definitions as well. In addition, Lemprovides a library of functions, including safely portable ones and some “extra”functions only translatable to some backends.Compared to Ott, which also targets multiple backends but requires excessivetarget-specific annotatations in the source code, Lem source code is less noisy sinceannotations are in general not necessary (although there are various target-specifcannotations available). This allows users to focus on semantics of the models them-selves without paying too much attention to target-specific implementation details.The clarity of the generated code makes them easier to work with. However, Lem’ssyntax support is weaker than Ott. It does not provide support for safe bindings inthe object language, although users may define a language model with bindingspecifications in Ott, and compile the Ott code to Lem. 1.1An example of this is included in Lem’s GitHub repository: https://github.com/rems-project/lem/tree/master/examples/ocaml light82.3 SpoofaxSpoofax is a “language workbench” for building DSLs [24]. It uses the existingSyntax Definition Formalism language to define language grammars, and Stratego,a framework based on term rewriting [11], to define the semantics of languages.Spoofax is mainly intended for developing new languages and supporting tools.There is little support for writing formal proofs.A distinct feature of Spoofax is its focus on IDE integration. Spoofax can“automatically derive efficient implementation for various IDE features” from lan-guage definitions, and also generate a “stand-alone Eclipse plugin for a language”[24]. This saves the language designer from having to implement IDE support oreditor plugins manually.9Chapter 3REDEX-PLUSA Computer Science MetanotationREDEX-PLUS is a computer science metanotation implementation based on Redex,an existing Racket-based metanotation. REDEX-PLUS translates Redex languagemodels into proof assistant code. However, because Redex has many features thatare either very difficult or outright impossible to translate to target proof assistantlanguages, REDEX-PLUS chooses to support only a well-defined translatable sub-set of Redex. 1In this chapter, I first introduce Redex and describe its capabilities, and then Idefine the translatable subset. I also give an explanation of Redex binding forms,which are important for understanding how REDEX-PLUS handles binding.3.1 RedexRedex is a Racket library providing a domain-specific language for defining andworking with semantic models [20, 26]. A Redex language model definition usu-ally consists of the following parts:Language definitions which defines the syntax of terms in a language.Each language definition contains a list of non-terminal definitions; and each1I discuss some possible future extensions to this translatable subset in section 8.2.10non-terminal definition contains a set of patterns. A term is considered to be-long a non-terminal if it matches one of the non-terminal’s patterns. Multiplenon-terminals can have overlapping sets of patterns, and a term can belongto several non-terminals simultaneously. The language definition also con-tains a list of binding forms, which specify variable binders in the objectlanguage. Object language terms are written in S-expression based concretesyntax: they may have extraneous symbols or brackets. The use of concreteinstead of abstract syntax allows greater readability and closer adherence tosyntactic norms.Metafunctions (MF), which are functions between terms. Metafunction are notfunctions in the object language. Instead, they are functions about the termsin the object language, hence the prefix “meta”. A metafunction definitionhas a list of pattern-matching cases, which are matched against argumentsduring evaluation. Metafunctions can be recursive. Metafunctions are oftenused in reduction relation and judgement form definitions.Redex comes with a built-in substitute metafunction which substitutes avariable with a term. substitute is capture-avoiding.Reduction relations (RR) between terms, representing reduction or evaluation inthe object language. Each RR definition contains a list of possible reduc-tions. If a term matches the pattern on the left-hand-side, then it reduces tothe term on the right-hand-side.Given an existing RR, Redex can also automatically construct its closures.The closure can be either a compatible closure, in which all reducible sub-terms of a term can be reduced; or a context closure, which only allowsterms that are in a certain reduction context (defined as a non-terminal) to bereduced.Judgement forms 2 (JF) which are essentially relations over terms. A JF defini-tion contains a set of inference rules from which a true judgement can be2The original spelling is “judgment form”. This thesis uses the “judgement” spelling. REDEX-PLUS provides both define-judgement-form and define-judgment-form which are identical ex-cept for their names.11derived. A JF can be proven by using the rules to construct a derivation treeeither manually or, in some cases, automatically.With the language model defined, the user may reason about the model in anumber of ways: for example, checking a judgement form using judgment-holdsand automatically finding its derivation trees using build-derivations; or call-ing apply-reduction-relation on a term which returns all terms the term mayreduce to. Redex also provides a GUI tool for tracing reductions, and proceduresfor typesetting language models into images or PostScript.All Redex features involve pattern matching: language definitions use patternsto describe terms’ syntax, while JF, MF and RR definitions work by pattern match-ing terms against the left-hand-side of rules. Patterns are written using Redex’spowerful pattern language in which many more advanced syntactic features in theobject language can be expressed succinctly: equality of metavariables is impliedby giving them the same “subscript”; and repetition of sub-patterns is denoted byellipses (...). Redex also allows “unquoting” into the Racket language, so thatterms can contain arbitrary Racket expressions, and Racket expressions can beused as side-conditions in patterns and RR or JF rules. Racket expressions areuseful when computations are required, when expressing arithmetic operations andcomplicated side-conditions.3.1.1 A Basic ExampleIn this chapter and the rest of the thesis, I use as an example the PolymorphicLambda Calculus (System F), as described in Types and Programming Languagesdefinition [33, p. 343], extended with natural numbers. Figure 3.1 shows an an-notated definition of an object language named F, which represents the concretesyntax of System F. In figure 3.3, two pieces of System F’s semantics, the typ-ing relation and β -reduction, are defined as Redex judgement forms and reductionrelations. An additional judgement form and two metafunctions, shown in figure3.2, are also defined to help express some of the typing rules. Together, the Redexstatements in the three figures define the entire language model of System F.To demonstrate how Redex can (visually) help reason with models, figure 3.4shows the Racket code for generating derivations for the typing judgement “f :N→12; defining a language named "F"(define-language F; a list of non-terminal specifications:[t ::= ; the non-terminal "t" can be...; anything that matches the following; patterns:(tvar tv) ; a literal "tvar" followed by a; "tv" which is defined laternat ; a literal,; representing the natural number type(-> t t)(forall tv t)][e ::=(var v) (lam (v : t) e) (app e e) natural(tlam (tv) e) (tapp e t)][env ::= (cons (v : t) env) (tcons tv env) nil]; defines "v" and "tv"; as two distinct types of variables[v ::= variable][tv ::= variable]#:binding-forms ; a list of binders:; specifies that lamdba-abstraction is a binder,; and that the lambda argument "v" is bound; in "e", the function body(lam (v : t) e #:refers-to v)(tlam (tv) e #:refers-to tv)(forall tv t #:refers-to tv))Figure 3.1: The Redex language definition for the F language.13(define-metafunction Fdiff : e v -> boolean[(diff (var v_1) v_1) #f][(diff e v_2) #t])(define-metafunction Ftdiff : t tv -> boolean[(tdiff (tvar tv_1) tv_1) #f][(tdiff t tv_2) #t])(define-judgement-form F#:mode (In I I O)#:contract (In env v t)[(In (cons (v : t) env) v t) "axiom"][(In env v_1 t_1)(side-condition (tdiff v_1 v_2))--------------------------------------------- "cons"(In (cons (v_2 : t_2) env) v_1 t_1)][(In env v t)------------ "tcons"(In (tcons tv env) v t)])Figure 3.2: Additional metafunction and judgement form definitions used todefine the typing relation in the F language.N ` f 10 :N” 3. When executed in an environment that supports a GUI, such as theDrRacket IDE, a window will pop up, showing all possible derivations Redex hasfound.3.1.2 Problems with Translating RedexAs the proof assistant targets are less expressive than Redex, accurately trans-lating some Redex features can be difficult if not outright impossible, or requireworkarounds that may not be worthwhile. Notably, many common idiomatic con-structs in Redex’s pattern language are, despite being intuitive for human users tounderstand, surprisingly difficult to express in proof assistant languages.When metavariables at different locations in a Redex pattern have the samesubscript, the pattern will only match if all such metavariables match the same3“applying f, a function from natural numbers to natural numbers, to 10, produces a naturalnumber.”14(define-judgement-form F#:mode (T I I O)#:contract (T env e t)[(In env v t)------------------- "context"(T env (var v) t)][--------- "natural"(T env natural nat)][(T (cons (v_a : t_a) env_t) e_b t_b)------------------------------------------- "abstract"(T env_t (lam (v_a : t_a) e_b) (-> t_a t_b))][(T env e_f (-> t_1 t_2)) (T env e_a t_1)--------------------------------------- "apply"(T env (app e_f e_a) t_2)][(T (tcons tv env) e t)----------------------------------- "Tabstract"(T env (tlam (tv) e) (forall tv t))][(T env e (forall tv t_a))------------------------------------------- "Tapply"(T env (tapp e t_b) (substitute t_a tv t_b))])(define beta(reduction-relationF#:domain e[--> (app (lam (v : t) e_b) e_a)(substitute e_b v e_a) "subst"][--> (tapp (tlam (tv) e) t)(substitute e tv t) "type-subst"]))Figure 3.3: The typing judgement and reduction relation for the F language.15(define ds(build-derivations(T (cons (f : (-> nat nat)) nil)(app (var f) 10)nat)))(show-derivations ds)Figure 3.4: Racket code for generating the list of derivations (ds) and dis-playing them. Only one derivation is shown as in this example there isonly one possible derivation.term. This notation of equality, which can be used in all Redex statements, doesnot exist in any of the translation targets. Generally, this means the equality con-straints must be made explicit in the target code. For language definitions, whichare commonly expressed as data structure definitions, the constraint may take theform of either requiring a proof of equality as an argument to a constructor if thelanguage is dependently-typed, or an additional “well-formed” relation that onlyholds for terms where the equality is respected. Either implementation makes us-ing the translated language definition more difficult.Ellipses in patterns, which denote lists of sub-patterns, also pose a challenge.In language definitions, ellipses patterns can be relatively easily translated into listsof data structures representing the sub-patterns. Elsewhere, however, working withthe lists in the syntax is difficult, especially when it requires breaking down or16constructing the sub-patterns in lists. For example, a JF rule may state[(P (l expr_1 ...)) (P (l expr_2 ...))------------------------------------ "zip"(P (lp (expr_1 expr_2) ...))]that is, if P holds for two lists ((l expr 1 ...) and (l expr 2 ...)), then P alsoholds for a list of pairs ((lp (expr 1 expr 2) ...)) formed by “zipping” togetherthe two lists. Representing this rule in the target language would require the useof an ad-hoc “zipping” operation, which, while easy to define in this case, wouldincrease in complexity should the ellipses patterns become more sophisticated. Inaddition, the two lists are implicitly required to be of the same length, adding anadditional constraint that must be caught and preserved by the translation process.Combining implicit metavariable equality and ellipses patterns, it is possible toexpress the recurrence of sub-patterns in a list. For instance, the pattern (expr 1expr 2 ... expr 1 expr 3 ...) matches a list in which the first sub-pattern(expr 1) appears again later. Matching such patterns in the target language mayrequire traversing the list.As mentioned before, multiple Redex non-terminals can have overlapping setsof patterns. This makes it possible to, for instance, in a manner similar to the infor-mal notations commonly seen in PL literature, define a “value” non-terminal whosepattern set is a strict subset of the “term” non-terminal’s, so that every “value”(which usually means “a term that cannot be further reduced”) is also syntaticallya term. This works in Redex where object language terms do not carry “types”intrinsically. Unfortunately, in all backends REDEX-PLUS targets, object languageterms are idiomatically represented by typed data structures, thus each term canonly be of one type 4Apart from the hard-to-translate patterns, another difficulty is translating ar-bitrary Racket expressions that can appear in terms in the object language or asside-conditions. Because Racket is a full-fledged language with a large stan-dard library that is never formalized, it is difficult to faithfully translate Racket4In some targets this can be worked around using subtyping possibly in conjunction with typeclasses, but this is not idiomatic.17expressions into proof assistant targets.3.2 The Supported Redex SubsetREDEX-PLUS supports a subset of Redex with most of Redex’s hard-to-translatefeatures removed. This translatable subset is sufficiently well-defined to allowaccurate translation into different proof assistant targets, and at the same time,sufficiently expressive to represent a wide range of language models. Notice thatthe aforementioned Redex model of System F (shown in figure 3.1) is defined usingonly features from the supported subset.REDEX-PLUS supports all the four main Redex statements for defining lan-guage models, described at the beginning of section 3.1. Macros for reason-ing about models, like judgment-holds, are not supported, as to translate themamounts to generating the code that carries out the reasoning tasks in the targetproof assistant. Because the purpose of REDEX-PLUS is translate language mod-els, rather than doing the proofs, these macros are beyond the scope of this project.Some possible extension to the translatable subset are discussed in section 8.2.Patterns and TermsREDEX-PLUS uses a small, strict subset of the original pattern language as shownin figure 3.5. Most of the Redex pattern language, including ellipses patterns(pattern-sequence as known in the Redex pattern language), side-conditions,all patterns related to holes or closures, strings, and Racket numbers5, are removed.natural and integer, the two basic numerical types supported across a widerange of targets, are however still supported.5Racket implements the full Scheme numerical tower including arbitrarily large and complexnumbers, which are not well-supported across targets. However, not supporting the full numericaltower has only marginal impact on language modeling.18pattern = natural| integer| variable| (variable-prefix id)| symbol| other-literalFigure 3.5: Pattern language supported by REDEX-PLUS.REDEX-PLUS still supports using unquote to include Racket expressions interms. However, the Racket expressions can only contain four basic arithmetic op-erations: addition, subtraction, multiplication, and division. Division is supportedonly for the SMT-LIB target, as other targets do not support non-total operations.Language DefinitionsREDEX-PLUS imposes some additional restrictions on language definitions. Thepattern set for each non-terminal must be disjoint, in other words, no pattern canbelong to multiple non-terminals at the same time. In non-terminal definitions,REDEX-PLUS requires each pattern that is not a binder specified by a binding formto contain no more than one potentially-bound variable. In addition, in bindingforms, only one variable may be bound at one time. A pattern with one variableas its only argument is called a variable constructor. In the generated target code,when substituting a variable for a term, the entire term constructed by the variableconstructor (instead of just the variable inside the term, as is the case with Redex)will be replaced .The statement define-extended-language which creates a new definition by“extending” an existing one with additional non-terminal patterns, is not supported.This is because in Redex a term can belong to both the original and the extendedlanguage at the same time, but the target languages, it is not possible to “extend”a data structure definition defining the syntax of a language; and if the extendedlanguage is defined as a new language, then a term cannot be in both languages atthe same time, as the “same” term will be represented differently in the originaland the extended language.19Notice that many of REDEX-PLUS’s restrictions on bindings, overlapping non-terminals, as well as the previously mentioned ones on ellipses in patterns, aresimilar to the restrictions imposed by LNgen on Ott (see 2.1.1).Judgement FormsRedex allows use of ellipses in judgement form definitions in a way similar toellipses in patterns. REDEX-PLUS does not support these ellipses. However, al-though while clauses and side-conditions are not supported in either patternsor as a part of MF and RR cases, they are allowed in JF cases.MetafunctionsThe range of a Metafunction’s signature must be either a non-terminal in the objectlanguage, or boolean. Disjunctive (or) ranges are not supported. The signaturemay not contain pre- or post-conditions. MF cases cannot have extra conditionsdenoted using where, side-condition, or judgement-holds.Importantly, MFs are required to be total. Redex allows non-total MF defi-nitions, only raising errors during runtime when the MF is applied to undefinedarguments. However, most of the target languages forbid non-total function defini-tions outright. While REDEX-PLUS does not come with a totality checker for MFs,non-total MF definitions will almost certainly be translated into illegal definitionsin the targets where functions must be total.Reduction Relations and ClosuresOnly the very basics of reduction relation definitions are supported. Like MFcases, RR cases are not allowed to have extra conditions denoted using where,side-condition, or judgement-holds. They cannot use fresh to generate freshvariables either. In terms of syntax of the RR statement, this means all of red-extrasexcept rule-name are not supported. Shortcuts in definitions are not supported ei-ther.The macro compatible-closure is also supported, but context-closure isnot supported. This is because a context-closure requires a reduction context.Redex uses special non-terminal definitions as reduction contexts, and these non-20terminal definitions are difficult to translate, due to aforementioned problems withoverlapping non-terminal patterns. Some possible workarounds are discussed insection 8.2.21Chapter 4Translating Language Models,and Generating CodeREDEX-PLUS can translate a Redex language model into one of the target proofassistant languages, so the properties of a language model can be proven or veri-fied using the proof assistants. In this chapter, I will describe how aspects of theRedex language models are represented in the target languages, with an emphasison various ways of representing variable bindings.Throughout this chapter, I will use the following two language models as ex-amples:The Tree language defines Peano numbers and a binary tree containing Peanonumbers. As a simple language with no variable bindings, it will be used inthe description of the basic translation procedure.The F language introduced in section 3.1 and defined in figure 3.1. The F lan-(define-language Tree[n ::= z (s n)][bt ::= (leaf n) (bt_l branch bt_r)])Figure 4.1: The Tree language model.22guage represents Polymorphic Lambda Calculus or System F, with supportfor natural numbers. It involves almost all of REDEX-PLUS’s features, in-cluding, most importantly, multiple variable types and their binding rules.4.1 Language Models to Intermediate RepresentationREDEX-PLUS translates a language model in two steps. First, it translates themodel into Poultry, a target-independent intermediate representation (IR). Andthen, it generates code in the target proof assistant languages from the IR. Com-pared to translating Redex language models into target languages directly, using anIR allows much of the code to be shared between the translation processes for dif-ferent targets, while also making the development of new translation targets faster.I will describe the implementation in more detail in chapter 6.4.1.1 Poultry: The Intermediate RepresentationThe intermediate representation Poultry 1 provides the following constructs:for-language defines an environment in which Poultry statements refer to a cer-tain Redex language. Since all Redex definitions supported by REDEX-PLUSmust declare the Redex language they refer to, all Poultry statements mustbe enclosed in for-language environments as well.For the sake of simplicity the for-language environment is omitted fromcode examples. This would not cause confusion as all the code in an example(other than the one in figure 4.2) belongs to the same Redex language.define-type defines a new type in a language, and the constructors that constructterms of this type. The constructors of a type can be recursive, but it must bepossible to construct a finite term for every type. Some recursive construc-tors can construct a term that binds the variables in its subterms, and someconstructors may be bound variables.One can use define-types to define multiple types at once. Types definedtogether in this way can have mutually recursive constructors.1Named so because Coq and Agda, two important translations targets, are avian.23; Simply-Typed Lambda Calculus(for-language STLC; These types belong to the STLC language(define-types ...); ... so is this proposition(define-proposition ...)); System F(for-language F; These types belong to the F language(define-types ...))Figure 4.2: Using for-language to separate statements belonging to differ-ent Redex languages.Function and proposition definitions must only use types already defined.define-function defines a function from a term in the language to either anotherterm in the language, or a boolean value. It supports pattern matching whichcan be used to deconstruct terms, conditional expressions, and some basicarithmetic operations.A function definition must be total. Otherwise, the function definition is mal-formed, and the generated proof assistant representation can be erroneous.define-function can also be used to define nullary “functions”. This fea-ture is used in parts of the translation processes to define constants.define-proposition defines a first-order predicate over terms in the language,as well as the conditions under which the predicate is true, which can berecursive. The conditions can refer to functions previously defined usingdefine-function.These three Poultry definitions are sufficiently expressive to represent all ma-jor features of Redex language models, namely, language definitions, judgement24forms, metafunctions, and reduction relations and their closures. At the same time,they are basic, generic concepts not tied to any particular representation, supportedby proof assistants and other tools built upon different background theories rangingfrom dependent types to many-sorted logics, which makes the final translation stepfrom Poultry to target code straightforward and relatively easy to implement.As Poultry definitions are intended to be used only in the automated translationprocess rather than being hand-written, they are not accessible to REDEX-PLUSusers.I will describe in further detail how the definitions translate into target code insection 4.2.4.1.2 From Redex To PoultryLanguage DefinitionsA define-language statement, which defines a new Redex language with one ormore non-terminals, is translated into a single define-types definition in Poul-try, in which each type definition corresponds to one non-terminal. Here a singledefine-types statement is used instead of multiple define-type statements, be-cause the latter does not support mutually recursive non-terminal definitions.Each Redex non-terminal definition contains a list of patterns of valid terms.REDEX-PLUS represents each of these patterns as a constructor. The name of eachconstructor is derived from the literals in the pattern or, if no literal exist, the namesof the non-terminals in the pattern. The Redex patterns represent the concrete syn-tax of the language. They may contain parentheses and multiple literal symbols,which improves readability when designing and presenting language models, butthey are poorly supported by REDEX-PLUS’s targets. REDEX-PLUS process sim-plifies patterns by taking out the parentheses, and removes all literals, leaving onlyother non-terminals as the types of constructor arguments, effectively transformingthe concrete syntax definitions into an abstract syntax. All terms and patterns inother Redex definitions are simplified using the same process.When a non-terminal is defined with more than one names in Redex, the firstname will be considered canonical and be used in the generated IR, and the other25(define-types (bt n)(((leaf (n))(branch (bt bt)))((z ()) (s (n)))))Figure 4.3: Defining a binary tree type with define-types.(define-metafunction Treemirror : bt -> bt[(mirror (leaf n)) (leaf n)][(mirror (bt_1 branch bt_2))((mirror bt_2) branch (mirror bt_1))])Figure 4.4: The Redex metafunction that mirrors a binary tree.names, or aliases, will be replaced by the first canonical name.Figure 4.3 shows how the Poultry type definition corresponding to the RedexTree language definition. Notice that the branch constructor is placed before itsarguments like all other constructors, rather than between two sub-trees like in theoriginal language model.MetafunctionsA define-metafunction definition is translated into a define-function state-ment. The body of the metafunction, which is a list of patterns, is translated intoa single pattern-#:match expression as the body of the definition. The type sig-nature of the original statement is preserved in the generated definition, and someadditional properties are passed into the definition, as they will later be used forgenerating proof assistant code.Figure 4.4 and 4.5 shows how a simple binary tree mirroring function is trans-lated.In Redex, if a pattern variable appears more than once in a pattern, then the26(define-function mirror#t ; should the language name be prefixed?#f ; does the language have binding?#f ; is the function recursive?(t1) ; list of argument names(bt) ; list of argument types; the function body(#:match (t1)(((leaf n))(leaf n))(((branch bt_1 bt_2))(branch (mirror bt_2) (mirror bt_1))))bt ; the return type)Figure 4.5: The generated IR of the statement in figure 4.4, with all argu-ments annotated. All user-defined metafunctions will have the languagename prefixed to the function name.pattern will only be matched if all occurrences of the pattern variable matchesthe same term. This is not directly supported by Poultry or any of the targets, soREDEX-PLUS must make the implied equality of patterns explicit during transla-tion.Given a metafunction case whose pattern contains multiple occurences of thesame pattern variable, REDEX-PLUS translates it by first pattern matching nor-mally, and then replacing the result of the pattern match with an #:if expressionwith the equality between patterns as its condition. The true branch of the #:ifexpression, which is returned when the equality condition is satisfied, is the termto be returned should this case match; and the false branch is another pattern matchwith rest of the patterns in the list translated similarly.Sometimes, the generated function body contains unnecessary #:match ex-pressions. REDEX-PLUS is able to detect and simplify these expressions beforegenerating target code, to keep the language definition as simple as possible.27(define-metafunction Treesame-tree : bt bt -> boolean[(same-tree bt_1 bt_1) #t][(same-tree bt_1 bt_2) #f])Figure 4.6: The Redex metafunction that compares two binary trees. Thefirst case, which returns true, is only matched when both arguments aresyntactically the same. If they are not, then the function falls back to thesecond case and returns false.An example of a function with multiple occurrences of the same pattern vari-able and the corresponding Poultry definition is shown in 4.4 and 4.5. Notice thatin the generated function body, there are two useless #:match expressions. Figure4.8 shows that, after simplification, both #:match expressions are removed and thefunction body is reduced to one simple conditional expression.Judgement FormsEach define-judgement-form statement in the language model is translated intoone single Poultry define-proposition definition. Each rule for constructing ajudgement in the Redex statement corresponds directly to a rule in the IR. Figure4.9 and 4.10 shows a definition representing the “less-than” relation between twoPeano numbers in the Tree language, and the resultant IR.For simple judgement form rules such as the ones in figure 4.9, the translationfrom Redex rules into Poultry is straightforward, requring little processing apartfrom term simplification. Some language models make use of side conditions andwhere clauses, which require additional processing:• Each side-condition, which evaluates to a term-level 2 boolean value, iswrapped up in a #:is-true? term, elevating it to the proposition level in thetarget language.2In dependently-typed proof assistants, the boolean data type is the term-level boolean, andpropositions are proposition-level. In SMT-LIB, both term- and proposition-level booleans are rep-resented by the native boolean type.28(define-functionsame-tree#t ; should the language name be prefixed?#f ; does the language have binding?#t ; is the function recursive?(t4 t5) ; list of argument names(bt bt) ; list of argument types; the function body(#:match(t4 t5)((a0 a1)(#:if(#:bool-and (#:bool-equal? bt a0 a1)); returns true if the trees are equal(true3844); returns false otherwise(#:match (t4 t5) ((bt_1 bt_2) (false3845))))))#:bool ; the return type)Figure 4.7: The IR of the same-tree function definition. Notice the #:ifexpression inside the top level #:match, in which the two argumentsare compared.; the simplified function body of same-tree(#:if (#:bool-and (#:bool-equal? bt t2 t3))(true3818) (false3819))Figure 4.8: The function body of same-tree after simplification.29(define-judgement-form Tree#:contract (Le n n)[------------ "Le-zero"(Le z (s n))][(Le n_1 n_2)------------ "Le-succ"(Le (s n_1) (s n_2))])Figure 4.9: The Redex judgement representing the “less-than” relation be-tween Peano numbers.(define-propositionLe (n n)(("Le-zero"#:implicit (n)#:result-type (Le (#:term (z)) (#:term (s n)))())("Le-succ"#:implicit (n_1 n_2)#:result-type (Le (#:term (s n_1))(#:term (s n_2)))((Le (#:term n_1) (#:term n_2))))))Figure 4.10: The generated IR of the statement in figure 4.9. The first twoarguments of define-proposition declares the name and signature,in terms of type names, of the judgement. A list of rules follows, inwhich each rule contains a list of (implicitly) bound variables used inthe rule, the judgement constructed by the rule, and a potentially empty(in the case of axioms) list of premises. The #:term keyword helps thelater translation process distinguish judgement forms from terms.30(define beta(reduction-relationF#:domain e[--> (app (lam (v : t) e_b) e_a)(substitute e_b v e_a) "subst"][--> (tapp (tlam (tv) e) t)(substitute e tv t) "type-subst"]))Figure 4.11: The Redex definition of β -reduction in System F.• Each where clause, which compares two terms of the same type, is turnedinto a proposition-level comparison between the two terms.Reduction Relations as FunctionsReduction relations can be considered as functions that take terms and return apotentially empty list of possible reduction results. This representation of reductionrelations is closer to Redex’s way of representing reduction relations: as reductionsteps that can be evaluated (see section 3.1).When treating reduction relations as functions, each reduction case is translatedinto an individual function definition, named after the reduction case. If the argu-ment to the function matches the left-hand-side of the reduction case, the functionreturns a list with the right-hand-side as its sole element. Otherwise, it returns anempty list. The reduction relation itself is then represented by the list of reductioncase functions.The final generated proof assistant code may come with a helper function thatapplies the list of functions to a term, returning a list of all possible reductionoutcomes. The generated code may also provide a relational definition of the re-duction relation, by defining the relation as “t reduces to t ′ if t ′ is in the list ofpossible reduction outcomes of t”.Figure 4.11 shows the Redex definition of β -reduction for System F; figure4.12 shows the function definition corresponding to the subst case.31(define-function beta-subst#f ; language name should not be prefixed#t ; the language has binding#f ; the function is not recursive(t) ; list of argument names; the argument should be a well-bound expression((#:well-bound e)); the function body(#:match (t)(((app (lam t e_b) e_a)); #:substitute is a special function definition(#:list (#:substitute e_b v e_a))); the #:any pattern matches all terms((#:any) (#:list))); returns a list of well-bound expressions(#:list-of (#:well-bound e)))Figure 4.12: The function definition corresponding to the subst reductioncase. The argument type (#:well-bound e) means an e that has atype-level guarantee of its well-boundedness. The well-boundednessrequirement is only relevant when using binding representations thatcan express well-boundedness, such as shifted names. When usingother binding representations, the requirement is ignored.Reduction Relations as RelationsAlternatively, reduction relations can be understood as relations between terms andtheir possible reduction outcomes. This results in a simpler representation that iseasier to work with in proofs, but cannot be evaluated like functions.Similar to Redex judgement forms, each reduction relation is translated intoa single define-proposition definition. Each reduction rule corresponds to onerule in the IR, with no premises, and “the left-hand-side of the original rule re-duces to the right-hand-side of the original rule” as the conclusion. Figure 4.1332(define-propositionbeta (e e)((beta-subst#:implicit (t e_b e_a)#:result-type(beta (#:term (app (lam t e_b) e_a))(#:term (#:substitute e_b v e_a)))())(beta-type-subst#:implicit (e t)#:result-type(beta (#:term (tapp (tlam e) t))(#:term (#:substitute e tv t)))())))Figure 4.13: β -reduction of System F represented as a proposition.shows how β -reduction for System F, defined in Redex in figure 4.11, can be thustranslated into a proposition definition.Compatible Closures as RelationsSimilarly, compatible closures can also be represented as relations, and translatedinto define-proposition definitions. Represented as a relation, the compatibleclosure of an existing reduction relation on a non-terminal e contains all rules inthe define-proposition statement representing the original reduction relation aswell as new rules covering reduction of sub-terms. Each new rule covers one re-cursive occurrence of e as an argument to a constructor of e, with “e from reducesto e to” as its sole premise, and “(c a 1 ... e from ... a n) reduces to (c a 1... e to ... a n)” as its conclusion, where c is a constructor of e. Both e fromand e to, and the other arguments in the constructors are universally quantified.Figure 4.14 shows how the compatible closure of β -reduction for System F,defined in 4.11 and translated into a relation in 4.13, is represented as a relationdefinition. Note that there are two rules covering the reduction of sub-terms in theapp (function application) constructor, as app takes two es as arguments.33(define-propositionbeta(e e); The original rules((beta-single-subst-cc#:implicit (t e_b e_a)#:result-type(beta (#:term (app (lam t e_b) e_a))(#:term (#:substitute e_b v e_a)))()); beta-single-type-subst-cc ...; the new rules("beta-cc-lam"#:implicit (e_from e_to t_i1)#:result-type(beta (#:term (lam t_i1 e_from))(#:term (lam t_i1 e_to)))((beta e_from e_to))); two rules for the "app" constructor; as there are two es in it("beta-cc-app"#:implicit (e_from e_to e_i1)#:result-type(beta (#:term (app e_from e_i1))(#:term (app e_to e_i1)))((beta e_from e_to)))("beta-cc-app-2"#:implicit (e_from e_to e_i0)#:result-type(beta (#:term (app e_i0 e_from))(#:term (app e_i0 e_to)))((beta e_from e_to))); other constructors follow)Figure 4.14: Compatible closure of β -reduction of System F represented asa proposition; abridged.344.2 Generating CodeAfter the first translation step during which a Redex model is translated to Poultry,the Poultry IR is then translated into target proof assistant code in the second step.At a high level, the three Poultry constructs are translated as follows:define-type translates to a data definition in the target.define-function translates to a function definition in the target language.define-proposition translates to something that can be proven to be true by thetarget.The above describes the intent of each Poultry construct that should be pre-served in the translated proof assistant code, rather than concrete ways in whichthe translation is carried out, because REDEX-PLUS targets proof assistants with awide range of background theories, making it difficult to strictly specify what eachPoultry construct corresponds to in the target language. For example, propositionscan be expressed idiomatically as type definitions in dependently-typed languages,but not in SMT solvers.When translating a Redex source file, on top of translating each Poultry defini-tion, a predefined prelude is inserted at the beginning of the output target code. Thecontent of the prelude differs between different proof assistant targets and bindingrepresentations, but, in general, the prelude imports libraries, standard library datatypes, and defines data structures and helper functions that might be used by thegenerated code.To help distinguish identifiers from different Redex languages from one an-other, the names of the Redex language they belong to are prefixed to the names oftypes, constructors, functions, et cetera in the target code. In addition, if an identi-fier contains characters not allowed in identifier names in the target language, thecharacters are replaced during code generation.In the rest of this section, I explain how Poultry constructs are translated intodifferent proof assistant targets, as well as the differences in the generated codearising from the different underlying theories used by the targets.354.2.1 Dependently Typed Proof AssistantsThe translation processes from Poultry IR into Coq, and Agda, the two dependently-typed targets, are largely similar, despite the numerous differences in the targets’syntax, theorem-proving style, and underlying theories. In this section I describehow Poultry constructs are translated into dependently-typed target languages, be-fore explaining some target-specific quirks and treatments.Type DefinitionsPoultry type definitions are translated to idiomatic data structure definitions independently-typed targets. Native types in constructor arguments are replacedby types supported by the target’s standard library, and variables are replacedby target- and binding-representation-specific data structures containing necessarybinding information. There is little complexity in the translation process as the cor-respondence between the Poultry define-type definition and target code is almostone-to-one.For each type definition, REDEX-PLUS also generates the boolean equality(eqb 3) definition for terms of the type. For a type t, its boolean equality defi-nition is a function with the signature eqb : t → t → Boolean, where Boolean isthe standard boolean type in the target language, returning true if the two termsare the same and false if otherwise. The boolean equality definition is used whentranslating metafunction definitions with implied equality conditions, previouslydiscussed in section 4.1.2.If the type definition contains bound variables, REDEX-PLUS also generateshelper functions for binding variables, as well as substituting terms. This is dis-cussed in detail in chapter 5.Function DefinitionsPoultry function definitions are translated into function definitions relatively straight-forwardly. However, there are major differences in how pattern matching, which isnecessary for representing Redex metafunctions, is handled in different targets, asdiscussed later in this section.3Borrowed from Coq.36Inductive Tree_bt : Type :=| Tree_leaf : Tree_n -> Tree_bt| Tree_branch : Tree_bt -> Tree_bt -> Tree_btwith Tree_n : Type :=| Tree_z : Tree_n| Tree_s : Tree_n -> Tree_n.Figure 4.15: The Coq definition of a binary tree generated by REDEX-PLUSProposition DefinitionsIn dependently typed languages, propositions are idiomatically defined as datastructure types, where the constructors can be used to construct proofs of the propo-sition. This closely corresponds to the Poultry define-proposition statementwhich contains a list of rules for proving the proposition. The translation is there-fore straightforward: The judgement form itself is translated into a type definition,parameterized by the non-terminals in the signature of the proposition definition;and each rule is translated into a constructor, with the name of the rule as the nameof the constructor, the list of #:implicitly bound variables as the list of argumentstaken by the constructor, and the #:result-type, i.e. the judgement constructedby the rule, as the return type of the constructor.Targeting Specific Dependently-Typed TargetsCoq is a proof assistant with the calculus of inductive constructions, a dependenttype system, as its underlying theory [9]. Due to Coq’s popularity in thewider ecosystem, Coq is the most important translation target, with the mostfeatures supported.When multiple types are defined at once using define-types, the type def-initions are joined together using with so that they may be mutually depen-dent.Proofs in Coq are idiomatically written as sequences of proof steps calledtactics. Tactics can be combined and reused to simplify proofs, and to al-low some degree of automation [17]. Whenever a proposition named x is37translated into Coq, a new tactic named autoderive_x is generated. As itsname suggests, the tactic automatically derives a proof, by making repeatedattempts at applying the proposition’s rules to the goal. It succeeds if itmakes any progress, and fails if it does not. REDEX-PLUS also generates anautoderive (without suffix) tactic, which tries to apply all previously de-fined proposition-specific autoderive tactics, saving the user from havingto type out the full name of the autoderive tactic they wish to use.The autoderive tactic is generated for all propositions, including not onlythe ones representing judgement forms, but also the ones representing reduc-tion relations and metafunctions.Figure 4.16 shows the “less than” relation between natural numbers, as de-fined in figure 4.9, translated into Coq, along with the generated autoderivedefinition. Figure 4.17 shows how autoderive can be used to write succinctproofs. Note that the user needs to perform induction, and to introduce newassumptions or variables manually, as autoderive makes no attempt at theseactions.Agda is a dependently typed language based on Martin-Lo¨f type theory that isalso a proof assistant [10]. Figure 4.18 shows the type definitions for Peanonumbers and binary tree, as well as the “less than” relation between numbers.Functions are translated into declarations followed by definitions, where thedefinitions are translated differently depending what is inside the functionbody. In simple cases, where the body has only one top-level pattern match-ing expression, the entire function body is translated into one anonymouslambda abstraction expression. In more complicated cases, where thereare pattern matches inside the function body, REDEX-PLUS extracts patternmatches into helper functions, places the helper functions in a where clause,and replaces their occurences with calls to the helpers.The extraction of inner pattern matches is necessary because Agda does nothave a pattern-matching expression, so pattern matching has to be done infunction definitions, and while Agda does support pattern maching in lambdaexpressions, it has problem type checking the expressions if they are inlined38Inductive Tree_Le : Tree_n -> Tree_n -> Prop :=| TreeProp_Le_zero {n} :(Tree_Le (Tree_z ) (Tree_s n))| TreeProp_Le_succ {n__1 n__2} :(Tree_Le n__1 n__2) ->(Tree_Le (Tree_s n__1) (Tree_s n__2)).Ltac autoderive_Tree_Le :=(apply TreeProp_Le_zero; autoderive_Tree_Le) +(apply TreeProp_Le_succ; autoderive_Tree_Le) +(progress auto; autoderive_Tree_Le) +(progress compute; autoderive_Tree_Le).Ltac autoderive := first [autoderive_Tree_Le].Figure 4.16: The “less than” relation defined in figure 4.9 translated into Coq,and the associated autoderive definitions.Theorem N_Less_Than_N_Plus_Two :forall n, Tree_Le n (Tree_s (Tree_s n)).Proof.intro n.induction n.all: autoderive.(* The alternative proof body:- apply TreeProp_Le_zero.- apply TreeProp_Le_succ.auto. *)Qed.Figure 4.17: Proving that a natural number is less than itself plus two byinduction on natural numbers. Both induction cases can be triviallysolved by autoderive.39data Tree-bt : Setdata Tree-n : Setdata Tree-bt whereTree-leaf : Tree-n → Tree-btTree-branch : Tree-bt → Tree-bt → Tree-btdata Tree-n whereTree-z : Tree-nTree-s : Tree-n → Tree-ndata Tree-Le : Tree-n → Tree-n → Setdata Tree-Le whereTreeProp-Le-zero : { n : Tree-n } →(Tree-Le (Tree-z ) (Tree-s n))TreeProp-Le-succ : { n:1 : Tree-n } →{ n:2 : Tree-n } →(Tree-Le n:1 n:2) →(Tree-Le (Tree-s n:1) (Tree-s n:2))Figure 4.18: The Agda definition of a binary tree, as well as the “less than”relation between Peano numbers.in the main function body, so these helper functions must be explicitly de-clared and defined in a where clause.4.2.2 BelugaBeluga is a programming language for reasoning about formal systems. In Bel-uga, bindings are represented using higher-order abstract syntax (HOAS), in whichbindings in the object language being modelled are represented by bindings in itsBeluga representation [32].Since the idiomatic Beluga representations of propositions and functions differtoo much from Redex and other targets, currently REDEX-PLUS can only translate40F_e : type.F_t : type.F_app : F_e → F_e → F_e.F_e_natural : nat → F_e.F_tapp : F_e → F_t → F_e.F_tlam : (F_t → F_e) → F_e.F_lam : F_t → (F_e → F_e) → F_e.F_nat : F_t.F___arrow__ : F_t → F_t → F_t.F_forall : (F_t → F_t) → F_t.Figure 4.19: System F represented in Beluga. The natural number type natis defined in the prelude.type definitions into Beluga.Translating types and propositions into Beluga is straightforward and largelysimilar to corresponding translations into dependently-typed targets. Both type andproposition definitions are translated into type declarations, followed by construc-tor declarations that corresponds to the type constructors, or the proposition rules.What is unique about the Beluga target is that it only supports HOAS binding rep-resentations, which is discussed further in section 5.4.4.2.3 SMT-LIBSatisfiability modulo theories (SMT) solving is about determining the satisfiabilityof logic formulae with regard to certain logic theories [6] such as arithmetics orquantifiers [15]. As an extension of traditional satisfiability (SAT) solvers with ad-ditional theories, SMT solvers can be implemented by “interfacing” an SAT solverwith solvers for the theories involved [16]. Like SAT solvers, SMT solvers can beused to find models that satisfy certain properties (for example, that the programcan reach an illegal state) and prove the correctness of a formula by showing thatits negation is not satisfiable. Use cases of SMT solvers include model checking[1] [13], and optimization [29].41Compared to other translation targets, SMT solvers are unique in their capabil-ity for:• Reasoning about arithmetic properties efficiently;• Coming up with models that satisfy certain properties; and• Operating automatically, requiring little user input for finding proofs.Many modern SMT solvers, such as Z3 [15] and CVC5 [5] accept inputs in the2.6 version of the SMT-LIB language [7]. The SMT-LIB 2.6 standard defines ans-expression-based language which is used to both define the model to be checkedand to instruct the SMT solver to check the model. SMT-LIB 2.6 supports not onlyvarious arithmetic theories, but also features useful for modeling computer pro-grams, such as recursive data types and functions. REDEX-PLUS supports translat-ing type and proposition definitions into SMT-LIB.Translation into SMT-LIBPoultry types are translated into SMT-LIB datatypes using the declare-datatypescommands. Like with Coq, when multiple types are defined together in a singledefine-types statement, they are declared together so the types can be mutuallyrecursive. Unlike in other targets, constructor arguments in SMT-LIB are named,so REDEX-PLUS automatically generate unique names for them.Proposition definitions are translated into uninterpreted functions. First, aproposition is declared as a function from its arguments to a boolean using thedeclare-fun statement. Then, the rules in the proposition definition are repre-sented as assertions, stipulating that the function returns true for certain inputsif certain premises are true. Uninterpreted functions are used because due to dif-ference between SMT-LIB’s function definition syntax and that of Redex, as wellas SMT-LIB’s lack of a pattern-matching expression, it is difficult to represent theRedex definitions as concrete SMT-LIB functions.42Chapter 5Variable BindingRepresentation & ImplementationThus was he given his name by one very wise in the uses of power.(Le Guin, A Wizard of Earthsea [27])Building upon Redex’s binding forms discussed in section 3.1, REDEX-PLUSis capable of expressing variable bindings and translating them in a variety of ways.In this chapter, I describe the binding representations REDEX-PLUS supports, howsubstitution and other binding-related operations are implemented, and how eachof these representations look like in generated target code.For this chapter, I use the F language defined in figure 3.1 as the example.The F language defines System F [33, p. 343] with two variable types (term vari-ables v, and type variables tv). To my knowledge, so far REDEX-PLUS is the onlymetanotation capable of generating binding implementations that 1) involve mul-tiple variable types, 2) are target agnostic, requiring no target-specific code in thelanguage model 1, and 3) target multiple proof assistant languages.Prequel: De Bruijn IndexingDe Bruijn indexing [14] is one of the earlier binding representations. Because lan-guage models using de Bruijn indexing often need to formulate judgement form1Contrast LNGen (see 2.1.1).43definitions in specific ways incompatible with other binding representations, it isoften not possible to use de Bruijn indexing as a drop-in replacement for other bind-ing representations. In contrast, the named, locally nameless, and shifted namesrepresentations, discussed later in this chapter, are drop-in replacements for eachother. For this reason, REDEX-PLUS does not support de Bruijn indexing. Butbecause de Bruijn indexing forms the basis upon which some other representationsare built, I introduce this approach here for the sake of clarity.With de Bruijn indexing, all variables are represented as natural numbers, andnames are erased from variable references and binders. The index representing avariable is the number of binders in the syntax tree between a variable and its ownbinder. If the index is greater than the number of bindings in existence, then thevariable is free, and its name is kept in a “free variable list” which is not a part ofthe syntax tree.Two terms written using de Bruijn indexing are α-equivalent if and only ifthey are syntactically identical. This greatly simplifies checking for α-equivalence.However, it is difficult for human users to read and understand terms written usingde Bruijn indexing. The locally nameless and shifted names representations, bothbased on de Bruijn indexing, both try to improve human usability while preservingthe α-equivalence property.5.1 NamedA simple way to deal with variables is to represent them as their textual names.Substitution would be defined as a function that takes the name of the variable tobe substituted for, the term to be substituted with, the term in which the substitutionhappens, and returns the term with all free occurrences of the variable replaced. Itis crucial that substitution changes only the free occurrences of a variable but notbound ones, as they are supposed to denote different things despite possibly sharinga name.When translating language models using this named approach, all variablesin patterns are represented by native string types in the target. This includes vari-ables in variable constructors, variables in binding forms, and variables with nobinding involved. Figure 5.1 shows the System F definition translated into Coq us-44Inductive F_e : Type :=| F_var : string -> F_e (* var. constructor for F_e *)| F_app : F_e -> F_e -> F_e| F_e_natural : nat -> F_e| F_tapp : F_e -> F_t -> F_e| F_tlam : string -> F_e -> F_e (* Binds F_tvar *)| F_lam : string -> F_t -> F_e -> F_e (* Binds F_var *)with F_t : Type :=| F_tvar : string -> F_t (* var. constructor for F_t *)| F_nat : F_t| F___arrow__ : F_t -> F_t -> F_t (* binds F_tvar *)| F_forall : string -> F_t -> F_twith F_env : Type :=(* F_cons and F_tcons contain variables,but are not under any binding. *)| F_cons : string -> F_t -> F_env -> F_env| F_tcons : string -> F_env -> F_env| F_nil : F_env.Figure 5.1: The Coq definition of the system F language using the namedbinding representation.ing named variable binding. Simple binding is also supported for the Agda target,and the code generated is functionally identical.Then, for every language definition with bindings, REDEX-PLUS also gener-ates the substitution function, and a “closed” relation which holds when a term hasno free variables (of a certain type). Both the substitution function and the “closed”relation are indexed by two non-terminal names: the first being the non-terminalwhose variables are being affected, and second being the non-terminal in whichthese variables appear.For example, the “substitute t in e” function in the System F language has thefollowing signature:sub_F_t_in_F_e : string -> F_t -> F_e -> F_eIt takes three arguments: a variable name, a t (type), and an e (expression), and45(* ... *)(* substitute "x" with "to" in term "e" *)with sub_F_t_in_F_e x to e :=match e with| F_var a0 => F_var a0| F_app a0 a1 =>F_app (sub_F_t_in_F_e x to a0) (sub_F_t_in_F_e x to a1)| F_e_natural a0 => F_e_natural a0| F_tapp a0 a1 =>F_tapp (sub_F_t_in_F_e x to a0) (sub_F_t_in_F_t x to a1)| F_tlam a0 a1 =>F_tlam a0 (if String.eqb x a0then a1 else (sub_F_t_in_F_e x to a1))| F_lam a0 a1 a2 =>F_lam a0 (sub_F_t_in_F_t x to a1) (sub_F_t_in_F_e x to a2)end(* ... *)Figure 5.2: The Coq definition of substitution of type variables in expres-sions in System F. This is a part of a larger definition that also definessubstitution of e in e and substitution of t in t.substitutes the t for free variables of type t inside the e with that variable name.It only affects type variables in the t non-terminal; term variables in the e non-terminal are not affected. Notice that if it tries to replace variables of type e with at, it would result in a type error.Figure 5.2 shows the definition of sub_F_t_in_F_e. Notice that it recursivelycalls sub_F_t_in_F_t when encountering a subterm of type t in the F_lam andF_tapp cases. Also notice that the substitution functon does not recurse into thesubterm in the F_tlam case if the variable to be replaced has the same name asthe variable bound by F_tlam. This is because substitutions should only replacefree occurrences of a variable, but since all occurrences of the variable inside thesubterm are bound, substitution should not happen to those variables.46e t envFigure 5.3: Binding relations in System F.5.1.1 Determining when to Generate Binding OperationsREDEX-PLUS generates a function for substituting t in e, but it does not generatefunctions for, for example, substituting e in t. This is because not all pairs ofnon-terminals need the substitution function. Given two non-terminals a and b,substitution for a in b is only needed if a may appear bound in b, that is, thereexists some non-terminal c such that1. A binding form in c binds a, and;2. b is c, or b can appear as a subterm of c, and;3. a is b, or a can appear as a subterm of b.Figure 5.3 shows the binding relations in System F, where a→ b means that “amay appear bound in b”, indicating that a substitution function for a in b is needed.The rationale for the relations in System F are:e→ e because e is bound by lam in e.t→ t because t is similarly bound by forall in t.t→ e because t is bound by tlam in e, and t appears in e (in lam).There are no outgoing arrows from env as an env term cannot contain a boundterm as its immediate subterm. Even though t, which has bindings, can appear inenv, env does not have any binding forms itself, and cannot appear as a subterm inother terms with binding forms, t cannot appear bound inside env.5.1.2 Variable CapturingThis representation is simple, but suffers from one major drawback: if the expres-sion being substituted with contains a variable bound in a binder, then that variable47will be captured by the binder. For example, as shown in the code example in fig-ure 5.4, substituting the variable x with the variable y in the function (lam (y :nat) x) gives (lam (y : nat) y): the variable y is being captured by the lambdaexpression.Compute sub "x" (F_var "y") (F_lam "y" F_nat (F_var "x")).(* computes to:= F_lam "y" F_nat (F_var "y"): F_e*)Figure 5.4: A Coq example of variable capturing during substitution.While not always deal-breaking, variable capturing is often undesirable, andthere exists a number of possible mitigations:• The user may require the expression being substituted with to be closed. Ifthe expression is closed, then it contains no free variables that can get cap-tured. The language model and the definition of substitution does not needto be changed, but extra constraints will likely be needed when expressingproperties about the language. See section 7.2.2 for a lemma involving sub-stitution that has an implicit closedness constraint.• The substitution function may rename the variable bound at a binder to afresh variable whenever it encounters a binder. This essentially ensures allvariables bound at binders to have names not used anywhere else, so that nofree variable can be captured. This approach is related to convention 5.3.4in Types and Programming Languages [33, p. 71], and also similar to howsubstitution operates in Racket. However, coming up with fresh variablenames is tricky in a proof assistant, considering a variable name not used ina term may still be present elsewhere in a theorem.• The user may assume all variable binders to use distinct names. This as-sumption is often made in informal model definitions and proofs 2. But for2In Types and Programming Languages, the typing rule for type abstractions in System F carries48formal proofs, stating the assumption and carrying it around in proofs be-comes much more difficult.• Use a capture-avoidant binding representation, which I discuss in the rest ofthis chapter.5.2 Locally NamelessThe locally nameless (LN) representation represents bound variables as de Bruijnindices. However, with LN, free variables are expressed in a more human read-able way as named variables, and de Bruijn indexing is only used when dealingwith bound variables. Like with de Bruijn indexing, terms written using LN areα-equivalent if and only if they are syntactically the same. The user does not needto work exclusively with numerical index, which is considered confusing and un-readable especially for larger terms [3, 8].The tool LNgen (see 2.1.1) can be used to generate LN-based Coq definitionsgiven a language defnition in Ott.REDEX-PLUS supports LN for all dependently typed targets. In this sectionI use Coq for demonstration, but similar code is generated for other dependentlytyped backends as well.When generating code using LN, REDEX-PLUS first defines LN variables asa datatype in the prelude (see section 4.2), with one constructor for free variableindexed by names, and another one for bound variable indexed by a number 3. Itthen defines the binding operation functions for the variable datatype, and booleanequality which is needed when defining the boolean equality functions on languageterms.When translating language definitions with variable bindings, three changes aremade: variable constructors take an LN variable as their sole argument; variablessuch an assumption [33, p. 342]; and the proof of lemma 9.3.8 (the substitution lemma in SimplyTyped Lambda Calculus) assumes two bound variables to be distinct.3This differs from the more common approach used in the LN paper [12], where the abstractsyntax of the language is modified and the language term for variables is split into one term for freeand another for bound variables. I choose to introduce a distinct variable type and keep the languageintact since modifying the language syntax necessitates changes to elsewhere in the language modelwherever the variable constructor is used, complicating the translation process too much.49Inductive Ln : Type :=| fv : string -> Ln| bv : nat -> Ln.Figure 5.5: The Coq definition of the LN variable type.Inductive F_e : Type :=| F_var : Ln -> F_e (* var. constructor for F_e *)| F_app : F_e -> F_e -> F_e| F_e_natural : nat -> F_e| F_tapp : F_e -> F_t -> F_e| F_tlam : F_e -> F_e (* binds F_tvar *)| F_lam : F_t -> F_e -> F_e (* binds F_var *)with F_t : Type :=| F_tvar : Ln -> F_t (* var. constructor for F_t *)| F_nat : F_t| F___arrow__ : F_t -> F_t -> F_t| F_forall : F_t -> F_t (* binds F_tvar *)with F_env : Type :=(* F_cons and F_tcons are not under any binding *)| F_cons : string -> F_t -> F_env -> F_env| F_tcons : string -> F_env -> F_env| F_nil : F_env.Figure 5.6: The Coq definition of the system F language.in non-terminals without bindings are turned into strings; and the variables beingreferred to in binding forms are removed, as the variables they bind are representedas de Bruijn indices rather than names. Figure 5.6 shows System F automaticallytranslated into Coq by REDEX-PLUS using LN.Next, REDEX-PLUS defines the LN binding operations: one that opens upa binding and takes the term under binding out; one that closes a term inside abinding; one that substitutes a term for a free variable; and one that binds variables50bound at a specific level to a term 4. These operations are defined as functions inthe target language.In addition, REDEX-PLUS also generates a definition of the locally closedproperty of terms. A term is considered locally closed if all bound variables withinthe term are bound by binders within the term. Intuitively, in a locally closed term,the level of every bound variable must be less than the number of binders in the syn-tax tree between the variable and the root of the syntax tree. Conversely, if a vari-able is bound at level greater than or equal to the number of binders, then the entireterm is not locally closed. For instance, the System F expression F_var (bv 2) isnot locally closed, as the bound variable is not bound by any binder outside.Like the substitution function in the previous section, the generated LN oper-ations as well as the locally closed property are also indexed by two non-terminalnames with the same meanings: the first being the non-terminal whose variablesare being affected, and second being the non-terminal in which these variables ap-pear. Likewise, not all pairs of non-terminals need LN operations, and the processdescribed in section 5.1.1 is used to decide which pairs do need them.The functions carrying out the LN operations are defined as Chargueraud de-scribed [12]. An excerpt of generated code is shown in figure 5.7.When writing a term, the user only needs to write variables using textualnames, and insert “close” operations at places where the variables are bound. Simi-larly, REDEX-PLUS inserts LN operations in terms in judgement forms, and replaceRedex substitutions with LN operations. Figure 5.8 and figure 5.9 gives examplesof how LN operations are used in hand-written and REDEX-PLUS-generated coderespectively.A pitfall of LN is that because locally unclosed terms are, while undesirable,syntactically valid, the locally closed property must be stated explicitly, usuallyas a premise to other properties. In addition, “open”ing a binding in LN requiresthe new variable name given to the bound variable to be fresh so that it does not4Only one of sub and bind is needed as both of them can be implemented using the other. A proofof their equivalence is mentioned in section 7.2.3.However, bind has the advantage that when given an already closed term, it can perform substitu-tion without having to first open the term with a fresh variable and then substituting the variable byits name. In addition to simplicity, using bind also eliminates the need for ensuring that the variableused when opening the term is fresh (so it would not capture any existing free variable).51(* ... *)with open_F_t_in_F_e x k e :=match e with| F_var a0 => F_var a0| F_app a0 a1 => F_app (open_F_t_in_F_e x k a0)(open_F_t_in_F_e x k a1)| F_e_natural a0 => F_e_natural a0| F_tapp a0 a1 => F_tapp (open_F_t_in_F_e x k a0)(open_F_t_in_F_t x k a1)| F_tlam a0 => F_tlam (open_F_t_in_F_e x (S k) a0)| F_lam a0 a1 => F_lam (open_F_t_in_F_t x k a0)(open_F_t_in_F_e x k a1)end(* ... )Figure 5.7: The Coq code generated for the LN operation “open t in e”. No-tice that 1) since this operation is about type variables (variables in theF_t type), the F_var constructor for term variables is not affected de-spite it taking a variable as an argument, 2) because a type variable isbound in F_tlam, the binding level k is incremented in the recursive call,and 3) since F_lam binds a term variable rather than a type variable, thebinding levels are not changed in recursive calls.clash with an existing free variable. This freshness requirement may require extraside-conditions when working with terms.5.3 Shifted NamesSimilar to the locally nameless representation, shifted names (SN) [18] uses nu-merical indices for bound variables and textual names for free variables. The usermanipulates terms written with SN using a set of operations similar to those ofLN. However, SN also affixes to each name another numerical index, in order todistinguish between distinct variables with the same name but bound at differentlevels. This gives the convenience of LN but removes the freshness requirementsfor variable names.A Coq implementation of SN is available as the shifted-names library [19].52Definition church_true :=F_tlam (close_F_t_in_F_e 0 "a"(F_tlam (close_F_t_in_F_e 0 "b"(F_lam (F_tvar (fv "a"))(close_F_e_in_F_e 0 "t"(F_lam (F_tvar (fv "b"))(F_var (fv "t")))))))).Definition church_true_bound :=F_tlam (F_tlam (F_lam (F_tvar (bv 1))(F_lam (F_tvar (bv 0)) (F_var (bv 1))))).Figure 5.8: The Church boolean “true” written using LN operations andnamed variables. It is equal to church_true_bound, written directlyusing de Bruijn indexing in bound variables.[(T (cons (v_a : t_a) env_t) e_b t_b)--------------------------------- "abstract"(T env_t (lam (v_a : t_a) e_b) (-> t_a t_b))]| FProp_abstract {env__t v__a t__a e__b t__b} :(F_T (F_cons v__a t__a env__t) e__b t__b) ->(F_T env__t(F_lam t__a (close 0 v__a e__b))(F___arrow__ t__a t__b))Figure 5.9: The Redex definition and its corresponding Coq translation of the“abstract” typing rule, for λ -abstractions, in System F. Here v__a, thename of the variable bound in F_lam, is a string.53The library provides a predefined variable type, and the SN operations definedas abstract morphisms from variables to language terms. To use the library, theuser needs to use the provided variable type in their language definition, define akleisli function that lifts the morphisms implementing SN operations into mor-phisms from terms to terms, and prove (or state as Axioms) some properties of thefunction. The library also requires all terms to have an implicit type argument in-dicating how many “levels” of binding the term is in. This feature, which is nota standard part of SN, makes undesirable locally unclosed terms, which containsvariables bound at a higher level than there are bindings outside, syntactically im-possible.REDEX-PLUS can generate Coq language definitions using the shifted-nameslibrary. Unfortunately, only a single variable type is supported, as having multiplevariable types requires multiple level arguments in the types of terms containingbindings, which are not supported by the library. This means language models withmultiple variables types, such as System F (see section 3.1.1), cannot be translatedusing shifted names.When using SN, REDEX-PLUS first imports the needed definitions from theshifted-names library, and defines boolean equality for shifted-names vari-ables. When translating type definitions, the extra type argument is added to alltypes. The extra type argument is also added to all other definitions when neces-sary. The var type from the library is used to represent variables in non-terminalswith bindings and the name type used in ones without. Constructor arguments thatare under binding will have their level arguments incremented, to indicate they areunder one extra layer of binding than their parent terms. Next, REDEX-PLUS gen-erates the kleisli function which lifts the SN operations so that the operationscan be used on language terms. The kleisli function is required to have certainproperlies, which REDEX-PLUS defines as Axioms.5.4 Higher-Order Abstract SyntaxHigher-order abstract syntax (HOAS) represents bindings in the language modelusing bindings in the metalanguage [21]. With HOAS, object language variablesare represented as metalanguage variables, and object language binders as meta-54Inductive STLC_e { V : nat } : Type :=| STLC_v : @var V -> @STLC_e V| STLC_app : @STLC_e V -> @STLC_e V -> @STLC_e V| STLC_n : nat -> @STLC_e V| STLC_lam : @STLC_t V -> @STLC_e (S V) -> @STLC_e Vwith STLC_t { V : nat } : Type :=| STLC_nat : @STLC_t V| STLC___arrow__ :@STLC_t V -> @STLC_t V -> @STLC_t Vwith STLC_env { V : nat } : Type :=| STLC_cons :name -> @STLC_t V -> @STLC_env V -> @STLC_env V| STLC_nil : @STLC_env V.Figure 5.10: The Coq definition of simply typed λ -calculus using shiftednames. Note that the type of second argument to STLC_lam has (S V)instead of just V as its level argument.language functions (in REDEX-PLUS’s case, variables and functions in the targetlanguages respectively). There is no need to implement binding operations as theuser can simply reuse existing binding features of the metalanguage.REDEX-PLUS supports representing variable binding using HOAS for the Bel-uga target, in which bindings are idiomatically represented in HOAS. Currently,only language definitions are supported. The encoding in HOAS is mainly carriedout in the following two steps: Before generating the Poultry definitions, variableconstructors are removed from non-terminal definitions. Variable constructors areno longer needed in the syntax definition as they represent variables in the objectlanguage, which, under HOAS, are represented by metalanguage variables instead.And then, when generating the signatures of constructors with binders, argumentsunder binding are required to have a function type from the type being bound tothe type of the term itself. Figure 5.11 shows the generated Beluga definition forthe simply typed λ -calculus.55STLC_e : type.STLC_t : type.STLC_app : STLC_e → STLC_e → STLC_e.STLC_n : nat → STLC_e.STLC_lam : STLC_t → (STLC_e → STLC_e) → STLC_e.STLC_nat : STLC_t.STLC___arrow__ : STLC_t → STLC_t → STLC_t.Figure 5.11: The Beluga definition of simply typed λ -calculus using HOAS.Notice that the constructor for term variable has been removed.56Chapter 6ImplementationAt its core, REDEX-PLUS is a compiler from Redex statements (in the supportedsubset) to target proof assistant language. In this chapter, I describe REDEX-PLUS’s interface and its overall structure, as well as the main translation procedure.6.1 InterfaceREDEX-PLUS is implemented as a Racket library. To use REDEX-PLUS, a userrequires REDEX-PLUS in their Racket code the same way they require otherlibraries. require’ing REDEX-PLUS makes available all of Redex except its GUItool 1, that is, all of redex/reduction-semantics and redex/pict. REDEX-PLUS also provides a handful of macros for configuring REDEX-PLUS, allowingthe user to choose the translation target, binding representation, variable repre-sentation, and metafunction and reduction relation representations as they wish.Figure 6.1 shows how REDEX-PLUS is required and configured to generate Coqcode using the locally nameless representation.The user then writes down the language model using the provided Redex macros.Like any other Redex model, REDEX-PLUS language models are executable Racketprograms, and running a REDEX-PLUS model prints the generated target code tothe standard output. The user is responsible for making sure that only the supported1The Redex GUI tool (from redex/gui) is not re-provided because GUI features are not sup-ported by certain development environments. Users with GUI-compatible environments may importredex/gui separately in their code.57subset of Redex is used in defining the model. Otherwise, the output is undefined.For language models using only Redex features within the supported subset,REDEX-PLUS can be used as a drop-in replacement of Redex: the user can accessREDEX-PLUS features by simply require’ing REDEX-PLUS instead of Redex,and configuring REDEX-PLUS as needed. On the other hand, all REDEX-PLUSlanguage models are also valid in Redex.#lang racket(require redex-plus)(use-backend coq)(use-binding locally-nameless)(define-language F; non-terminal definitions); other definitions followFigure 6.1: require’ing the REDEX-PLUS library, configuring it, and usingit to define system F.6.2 Internal WorkingsREDEX-PLUS’s core compilation procedure consists of the following three steps:1. A statement in a language model, which is a valid Racket syntax object, isparsed using the syntax/parse library. Statements like define-languageand define-judgment-form, which provides multiple ways to define thesame non-terminal or judgement rule, are also normalized in this stage. Af-ter this stage, each statement in the language model is turned into a Racket58data structure which is then passed to the next stage. The parsing stage iscompletely independent of the translation target.2. The statement is passed down a number of compilation passes. Together, thepasses carry out the transformation described in section 4.1. A more detailedexplanation of the passes is given in section 6.3.The exact passes a model goes through depend on the target proof assistant,although the majority of the passes are shared between all targets. The fi-nal pass produces definitions in a target-agnostic intermediate representationnamed Poultry, described in further detail in section 4.1.1.3. The intermediate Poultry statements are translated into concrete target codeand written to the standard output. The detailed translation process is de-scribed in section 4.2. The translation is done in one single step, and littlecould be shared between the translation process for different targets. Thisstep does not only translate the definitions themselves, but also generate theboilerplate code, such as boolean equalities and binding operations, requiredto use the language model.During macro expansion, each statement such as define-language is wrappedin a call to the compilation procedure outlined above. The compilation procedureis run, and target code generated, during the run-time of the Racket program.6.3 The Compilation PassesThe transformation from Redex statements to Poultry definitions is carried out bya sequence of passes. Each pass either checks, records, or modifies the statementdata structure, and passes the modified data structure down to the next pass. Thefinal pass produces target-agnostic, intermediate Poultry definitions which are thentranslated into target code.The decision to use multiple smaller passes instead few large, monolithic passesis inspired by “nanopass” compilers where each of the numerous “nanopasses”does only a single task [25, 36], albeit some of REDEX-PLUS’s passes do morethan one thing. This approach allows great flexibility in the translation process:59some passes can be bypassed or added depending on user configurations; the finalpass can be replaced to generate a different type of Poultry definition; and any newtranslation step can be added as new passes, with little impact to existing passes,as long as it accepts and outputs compatible models.Table 6.1 shows the translation pipelines and their passes for all supportedstatements. While the translation procedure for different statements differ sig-nificantly, all pipelines contains the following types of passes: passes that checkfor errors and missing informations; a pass that normalizes non-terminal aliasesto canonical non-terminal names as defined in section 4.1.2; a pass whose namestarts with simplify-, in which terms and patterns in the statements written in theconcrete syntax of the object language are simplified into the abstract syntax (asdescribed in section 4.1.2); and the final pass which generates Poultry statements.define-language Passes• The first two passes checks for common mistakes in the language definitions andaborts the translation if any is found. check-language-well-foundedness en-sures that recursively-defined non-terminals have non-recursive “base cases”, with-out which one cannot write concrete terms, and the generated language definitionbecomes invalid in some targets; detect-misspelled-non-terminals checks ifa symbol in a non-terminal definition is a likely misspelling of an existing non-terminal name, or is missing an underscore2. Such errors will otherwise be carriedsilently into future translation steps and cause errors that are difficult to debug.• display-prelude prints the prelude (see section 4.2) to the output.• The passes whose names begin with save- or register- stores information aboutthe language for future uses. The saved information is retained after the languagedefinition has been translated as other definitions still use them.Apart from register-and-remove-variable-non-terminals, which removes non-terminals used to solely represent typed variables, most of these passes do not makeany changes to the model.• simplify-constructors simplifies constructors as described in section 4.1.2. Thisstep also generates “simplifiers” which are used to simplify terms and patterns inother statements of the language model in the future.2In a language with a non-terminal named e, for example, e 1 in non-terminal definition matchesa term of the non-terminal e, but e1 would be a literal.60After this pass, all terms are in the normalized and simplified form.• implement-binding-form writes binding information into terms via the followingtransformations: variable constructors in non-terminals with binding are markedas “bound”; variables referred to in binding forms are removed; and terms underbinding in binding forms are marked as “affected”. Non-terminals without bindingsare not changed.After this pass, all bound variables would be represented in the aforementionedform.• order-constructors places non-terminals containing binders and bound variablesfirst.• encode-in-hoas takes language definitions with binding information already writ-ten in and turns them into concrete HOAS representations.define-judgement-form Passes• check-contract-existence checks if a contract, which states the non-terminaltypes of arguments to this judgement form, exists. If there is no contract, an error israised as REDEX-PLUS cannot deduce a contract on its own.• generate-default-rule-names generates names for unnamed rules.define-metafunction-form Passes• replace-booleans replaces all Racket boolean literals in metafunction definitionswith fresh symbols to prevent any potential clashes with non-terminal patterns ofthe same names.• translate-metafunction translates the function into its Poultry representation.• optimize-matches simplifies unnecessary #:match expressions in the Poultry rep-resentation of a metafunction.reduction-relation Passes• The first two passes, as names suggest, deduces the domain and codomain of therelation if they are not specified.61• Depending on user setting, the reduction relation will be represented as either arelation (similar to judgement forms) or a function. (similar to metafunctions; exe-cutable in the target language).The two passes named reduction-relation->...-definition translates reduc-tion relations into the respective Poultry statements. This pass also saves the Poultrydefinition generated, so it can be later used to generated the closure of the reduction.• For proof assistant targets with support for defining custom notations or operators,define-notation generates the notation definition.6.4 Adding New Translation TargetsTo add a new translation target, or to implement a new binding representation, oneneeds to carry out the following steps:1. Implement the translation from normalized, simplified object language termsin Redex into the target language. If the target makes use of types, then thetranslation from these two procedures should be implemented first as theywill be used in the translation of almost all other definitions.In existing translation implementations, these processes are carried out bythe translate-term and translate-type procedures respectively.2. Implement the translation from Poultry definitions into the target language.At the mininum, translation of define-type statements must be implementedin order to represent the syntax of the target language; but other definitionsare not necessary.3. Decide if the translation pipeline needs to be modified. If the target languageis based on a logic system similar to that of an existing target, then there isa good chance that it can reuse most, if not all, passes already implementedfor the existing target. For example, if one wishes to add a dependently-typed target using the locally nameless representation, then it is unlikely thatthey will need a pipeline significantly different from the existing pipelinesfor Coq and Agda.62Table 6.1: Compilation passes for all REDEX-PLUS statements and targets.“©” means this pass is a part of the translation process for the target; “|”means it is not; “4” means it depends on user setting; “⊕” means onlyone of the passes marked as so is included, depending on user settings;and “×” means this statement is not supported by the target. The targets(Coq, Agda, Beluga, and SMT-LIB) are abbreviated to their initial letters.Pass C A B Scheck-definition-well-foundedness © © © ©detect-misspelled-non-terminals © © © ©display-prelude © © © ©save-language-definition © © © ©register-if-has-binding © © © |register-patterns © © © ©register-and-remove-variable-non-terminals © © © ©simplify-constructors © © © ©register-constructors © © © ©implement-binding-form 4 4 4 |register-variable-constructors © © © |register-substitution © © © ©order-constructors © © © ©encode-in-hoas | | © |translate-language-definition © © © ©(a) Compilation passes for define-language.Pass C A B Scheck-contract-existence © © × ©normalize-contract-types © © ©generate-default-rule-names © © ©simplify-rule-patterns © © ©translate-judgement-form-definition © © ©(b) Compilation passes for define-judgement-form.Pass C A B Snormalize-signature-types © © × ×replace-booleans © ©register-mf © ©simplify-patterns © ©replace-wildcards © ©translate-metafunction © ©optimize-matches © ©generate-metafunction-definition © ©(c) Compilation passes for define-metafunction.63Pass C A B Sdeduce-domain | © × ©deduce-codomain © © ©normalize-domain-and-codomain © © ©use-default-arrow-if-not-specified © © ©generate-default-case-names © © ©simplify-patterns © © ©reduction-relation->relational-definition⊕ © ©reduction-relation->functional-definition⊕ | |define-notation © | |(d) Compilation passes for reduction-relations.Pass C A B Scompatible-closure->relational-definition⊕ © × ©(e) Compilation passes for compatible-closure.4. Add new passes, or make modified versions of existing passes, if needed.Since there are almost certainly some existing passes in the new pipeline,one must make sure that the output of the new passes are compatible withthe subsequent existing passes.5. Unless one is expanding REDEX-PLUS’s translatable subset, there is littlereason to change the syntax parser.64Chapter 7EvaluationAs stated in section 1.3, the goal of REDEX-PLUS is to allow users to write lan-guage models in Redex, and use REDEX-PLUS to translate the models to proofassistant languages in which proofs can then be written, without having to man-ually define the language models in a proof assistant language, or to write anyboilerplate. In this chapter, I show that REDEX-PLUS fulfills the aforementionedgoal. First, I show that REDEX-PLUS can translate the same language model usingdifferent binding representations to different targets, and save the user from havingto write large amounts of boilerplate; then, I show that REDEX-PLUS generateslanguage definitions that can be used to prove non-trivial properties of languagemodels. Finally, I discuss some findings about the SMT-LIB translation target andits limitations.7.1 Automatic Code GenerationIn this section, I evaluate REDEX-PLUS’s ability to generate code targeting dif-ferent proof assistants using different binding representations. Here, I look at twolanguage models:• The Simply Typed Lambda Calculus (STLC), whose Redex model has 8lines of language definition and 50 lines of other definitions, excluding im-ports and configurations. The STLC model is used for evaluation proofs laterin this chapter in section 7.2.65Target Model Binding P LD LB BO OD OBCoqSTLCNamed 21 11 20 21 20 53LN 129 11 20 53 20 53System FNamed 21 16 25 67 26 48LN 129 16 25 167 26 48AgdaSTLCNamed 21 17 20 17 38 0LN 57 17 20 31 38 0System FNamed 21 22 25 57 45 0LN 57 22 25 105 45 0Table 7.1: Breakdown of the amount of generated code, in terms of lines ofcode.• The System F, whose Redex model has 18 lines of language definition and63 lines of other definitions. System F, introduced in section 3.1.1, is usedas an example throughout this thesis.I translate the two models into Coq and Agda, using both the named and locallynameless binding representations. Then, for each of the generated code file, I countthe number of lines of code in each of the following categories:Prelude (P) Library imports, and definitions of variable types and operations onthem, all located at the beginning of the file.Language Definition (LD) Data definition of the language’s abstract syntax.Language Boilerplate (LB) Boilerplate for the language definition. Mostly thedefinition of boolean equality.Binding Operations (BO) The substitution function, and operations such as “open”and “close” for the locally nameless representation.Other Definitions (OD) Definitions of judgement forms, metafunctions, and re-duction relations.Other Boilerplate (OB) Boilerplate related to the other definitions, such as autoderivetactic definitions in Coq.Table 7.1 and figure 7.1 shows the numbers of lines of code that falls undereach category for each target, language model, and binding representation.66Redex, STLCRedex, Sys. FCoq, STLC,NamedCoq, STLC,LNCoq, Sys. F, NamedCoq, Sys. F, LNAgda, STLC,NamedAgda, STLC,LNAgda, Sys. F, NamedAgda, Sys. F, LN0200400LinesofCodePrelude Language DefinitionLanguage Boilerplate Binding OperationsOther Definitions Other BoilerplateFigure 7.1: Breakdown of the amount of generated code, in terms of lines ofcode.7.1.1 DiscussionFirst of all, it is worth noting that the two Redex language models used in this sec-tion are target-agnostic: they do not include any target-specific information. In ad-dition, no changes to the language models are needed when chaging the target proofassistant or the binding representation. These two observations show that REDEX-PLUS language models are portable: the user needs to only write the model once,and REDEX-PLUS is able to translate the model to different targets using differentbinding representations without having to modify the language models.As shown by the breakdown of code content, significant proportions of the codegenerated are binding operations, sometimes over 40%. Binding operations alsotake more lines of code to define when there are more than one type of variables,which is the case with System F, or when using the locally nameless representa-67tion, which has more binding operations. In contrast, language definition properuses much fewer lines of code. By automatically generating binding operations aswell as other boilerplates, REDEX-PLUS lets the user focus on the language defini-tions themselves, without having to go through the tedious, error-prone process ofwriting all the binding operations by hand.7.2 Properties of the Simply Typed Lambda Calculus(define-language STLC[t ::= nat (-> t t)][e ::= (v variable) (lam (variable : t) e) (app e e) natural][env ::= (cons (variable : t) env) nil]#:binding-forms(lam (variable : t) e #:refers-to variable))(define beta-single-step(reduction-relationSTLC#:domain e[--> (app (lam (variable : t) e_b) e_a)(substitute e_b variable e_a) "subst"]))(define beta (compatible-closure beta-single-step STLC e))Figure 7.2: The Redex language definition of STLC and β -reduction.The Simply Typed Lambda Calculus (STLC) is a simple language model of-ten used as a basis for developing more sophisticated languages. In this section,I prove some important and well-known properties about typing and reduction inan extension of STLC that includes natural numbers. The language model defini-tion as well as the proofs are largely based on chapters Lambda and Properties ofProgramming Language Foundations in Agda [40], and some of the proofs’ struc-68tures resemble those found in Volume 2 of Software Foundations [34]. The proofsare done in Coq and Agda using language models translated by REDEX-PLUS fromthe Redex definition using the “named” binding representation described in section5.1. Figure 7.2 shows the Redex definition of the STLC syntax and β -reduction,and figure 7.3 shows the typing judgement as well as related definitions.There are a few notable differences between the STLC language model usedhere and more “basic” definitions of STLC such as the one in Types and Program-ming Languages [33, p. 103]:• Natural numbers (natural) are valid expressions. There is also a naturalnumber type (nat), and an associated typing rule (“natural”). The naturalnumber type serves as a necessary “base” type for the type system. If thelanguage does not have a base type, it would be syntactically impossible towrite a well-formed type, and no expression in the language can be well-typed at all.• The Value judgement form determines whether or not an expression is con-sidered a “value”. In many definitions, “value” is defined as a syntacticconstruct that is a subset of expressions, rather than a relation or a property.• The typing environment is expressed as an explicit, nil-terminated list con-structed by cons’ing type statements of the form “variable v has type t”to another environment. The “In” judgement is used to “look up” the typestatement associated with a variable in the environment, “returning” only thefirst matching statement and discarding the rest. If a typing statement statinga variable has a certain type In an environment, then, by the “context” typingrule, the variable, as an expression, has that type given the environment.• β -reduction (beta) is defined as the compatible closure of the reduction offunction application (beta-single-step). This means reduction can hap-pen in any order, and the body sub-expression in an lambda abstraction canreduce on its own. Fortunately, for all but the last proof, allowing lambdaabstractions to reduce on their owns does not matter, and the compatible clo-sure is all I need to prove the theorems. For the final proof, reducing the69(define-metafunction STLCdiff : variable variable -> boolean[(diff variable_1 variable_1) #f][(diff variable_1 variable_2) #t])(define-judgement-form STLC#:contract (Value e)[(Value natural) "natural-is-value"][(Value (lam (variable : t) e)) "lam-is-value"])(define-judgement-form STLC#:contract (In env variable t)[(In (cons (variable : t) env_t) variable t) "axiom"][(In env variable_1 t_1)(side-condition (diff variable_1 variable_2))--------------------------------------------- "cons"(In (cons (variable_2 : t_2) env) variable_1 t_1)])(define-judgement-form STLC#:contract (T env e t)[(In env variable t)------------------- "context"(T env (v variable) t)][--------- "natural"(T env natural nat)][(T (cons (variable_a : t_a) env_t) e_b t_b)------------------------------------------- "abstract"(T env_t (lam (variable_a : t_a) e_b) (-> t_a t_b))][(T env e_f (-> t_1 t_2)) (T env e_a t_1)--------------------------------------- "apply"(T env (app e_f e_a) t_2)])Figure 7.3: The Redex definition of the typing judgement in STLC.70Notation "e >-> e'" := (STLC_beta e e') (at level 20).Notation "env |- e : t" := (STLC_T env e t)(at level 20, e at next level, t at next level).Notation "x : t :: env" := (STLC_cons x t env)(at level 20, t at next level, env at next level).Notation "x : t <- env" := (STLC_In env x t)(at level 20, t at next level, env at next level).[_⇒_]_ = sub-STLC-e-STLC-e {- [ v ⇒ e1 ] e2 = sub v e1 e2 -}_ _ = STLC-beta_∈_::_ = STLC-cons {- v ∈ t :: env = (cons (v : t) env) -}∅ = STLC-nil_3_∈_ = STLC-In {- v 3 t ∈ env = (In v t env) -}_`_∈_ = STLC-T {- env ` e ∈ t = (T env e t) -}Figure 7.4: Notation definitions for STLC, in Coq and Agda.body sub-expressions of lambda abstractions does cause problems. I discussthe problem and my workaround in detail later in section 7.2.3.In Redex, I can use a context closure to forbid the reduction of certain sub-terms, and to impose a reduction order. However, context closures are notsupported by REDEX-PLUS. Alternatively, I can also define the entire reduc-tion relation manually as a judgement form, but that would not be idiomaticin Redex.For the sake of clarity and brevity, I manually defined a number of notationalshorthands as shown in figure 7.4, and used them in the proofs.The Redex language models used can be found in the code repository in examples/coq-stlc-named-explicit.rkt and examples/agda-stlc-named-explicit.rkt.The completed proofs can also be found in code repository inside the proofs di-rectory.717.2.1 ProgressTheorem 1 (Progress). For any expression e and type t, if e has type t under anempty context (i.e. (T nil e t)), then either e is a value (i.e. (Value e)), orthere exists an expression e 2 such that e reduces to e 2.In Coq:Theorem Prog : forall e t,STLC_nil |- e : t -> is_value e \/ exists e', e >-> e'.In Agda:prog : ∀ e {t}→ ∅ ` e ∈ t → STLC-Value e unionmulti ∃[ e' ] (e e')Proof. By induction on the typing relation (T nil e t). Most induction cases areeither vacuous because the typing property does not hold, or trivial as the expres-sion is already a value. In the application case, the proof proceeds by case analysison the induction hypothesis of the first sub-expression. If the sub-expression is avalue, then it must be an lambda abstraction for the expression to be well-typed,in which case the whole expression undergoes β -reduction; otherwise, it reducesto some other expression, and by the compatible closure the entire expression alsoreduces.See section A.1.1 for the Coq proof, and section A.2.1 for the Agda proof.7.2.2 Preservation of Types under SubstitutionLemma 1 (Preservation of Types under Substitution (Substitution Lemma)). Forany environment env, variable x, type xt, expression v and e, and type t, if v hastype xt under an empty context (i.e. (T nil v xt)), and e has type t under (cons(x : xt) env) (i.e. (T (cons (x : xt) env) e t)), then e with all freeoccurences of x substituted with v has type t under env (i.e. (T env (substitutex v e) t)).72In Coq:Lemma Subst :forall env x xt v e t,STLC_nil |- v : xt-> x : xt :: env |- e : t-> env |- sub x v e : t.In Agda:subst : ∀ {env v e to vt t}→ ∅ ` to ∈ vt→ (v ∈ vt :: env) ` e ∈ t→ env ` [ v ⇒ to ] e ∈ tNotice that the first premise in the hypothesis, which states that the expressionv has type xt under a nil context, implies the closedness of v. If v contains anyfree variable, then it would not have a type.Proof. By induction on either the expression e and then inversion of the typingjudgement (T (cons (x : xt) env) e t). Alternatievly, by induction on thetyping judgement directly.See section A.1.3 for the Coq proof, which uses the former approach in orderto obtain a sufficiently strong induction hypothesis, and section A.2.3 for the Agdaproof, which uses the later approach.The proof of lemma 1 makes use of a number of auxiliary lemmas. Most ofthem are about the preservation of types under changes to the typing environment.The rest are about properties about the diff function. The auxiliary lemmas arestates and proven in sections A.1.2 and A.2.2 in Coq and Agda respectively.7.2.3 PreservationFor this theorem instead of using the automatically generated beta reduction re-lation which has some peculiarities as discussed earlier, I use the hand-writtendefinition of β -reduction shown in figure 7.5 instead. The only difference betweenthe hand-written definition and the automatically generated one is that the hand-written definition does not allow the body sub-expression in lambda abstractions toreduce. That reduction rule is problematic because it leads to a case where the in-duction hypothesis is too weak, and strengthening the induction hypothesis wouldrequire a stronger substitution lemma that is significantly more difficult to prove.73It is worth noting that this particular difficulty comes from theorem proving, ratherthan REDEX-PLUS itself, and is thus orthogonal to the evaluation of REDEX-PLUS.Inductive beta : STLC_e -> STLC_e -> Prop :=| beta_single_step_subst_cc {variable t e__b e__a} :(beta (STLC_app (STLC_lam variable t e__b) e__a)(sub variable e__a e__b))| beta_cc_app {e__from e__to e__i1} : (beta e__from e__to)-> (beta (STLC_app e__from e__i1) (STLC_app e__to e__i1))| beta_cc_app_2 {e__from e__to e__i0} : (beta e__from e__to)-> (beta (STLC_app e__i0 e__from) (STLC_app e__i0 e__to)).Notation "t1 --> t2" := (beta_reduction t1 t2) (at level 20).data _−→_ : STLC-e → STLC-e → Setdata _−→_ whereβ−→ : ∀ {`variable t e:b e:a}→ STLC-Value e:a→ ((STLC-app (STLC-lam `variable t e:b) e:a)−→ (sub-STLC-e-STLC-e `variable e:a e:b))app−→*l : ∀ {e:from e:to e:i1}→ (e:from −→ e:to)→ ((STLC-app e:from e:i1) −→ (STLC-app e:to e:i1))app−→*r : ∀ {e:from e:to e:i0}→ STLC-Value e:i0 → (e:from −→ e:to)→ ((STLC-app e:i0 e:from) −→ (STLC-app e:i0 e:to))Figure 7.5: Definitions of β -reduction and the associated notation in Coq andAgda. The rule for reducing the body of an lambda abstraction has beenremoved, and the left sub-expression of a function application is notrequired to be a value before the right sub-expression could reduce.Theorem 2 (Preservation). For any expression e 1 and e 2, and type t, if e 1 hastype t under the empty context (i.e. (T nil e 1 t), and e 1 reduces to e 2, thene 2 has type t under the empty context (i.e. (T nil e 2 t)).74In Coq:Theorem Pres : forall e t e',STLC_nil |- e : t ->e --> e' ->STLC_nil |- e' : t.In Agda:pres : ∀ {e t e'}→ ∅ ` e ∈ t→ e −→ e'→ ∅ ` e' ∈ tProof. By induction on the typing relation STLC_nil |- e : t. Most inductioncases are vacuous or trivial. The only interesting case is that of the typing offunction application, which requires the substitution lemma to prove.See section A.1.4 for the Coq proof, and section A.2.4 for the Agda proof.7.2.4 DiscussionBy proving some important properties of STLC, I show that REDEX-PLUS cangenerate language models suitable for use in practical theorem-proving in multipleproof assistant languages. The proofs follow the conventional styles in the tar-get proof assistants, and are generally easy to work with. For the Coq proof, theautoderive tactic, which automatically searches for the judgement form deriva-tion that proves a goal, has proven useful as it was used multiple times throughoutthe proofs.While most of the theorems (including the auxiliary lemmas) in this sectiondo not require any additional definitions to be manually added to the languagemodel to prove, I still needed to manually define β -redution as shown in figure 7.5.This can be avoided if Redex’s context-closures are supported in the future. Inaddition, while not strictly required, I still added the notation definitions in figure757.4 for better clarity. A future version of REDEX-PLUS may be able to generate thenotation definitions on its own, or, in the case of Agda, follow the original languagesyntax closer when generating language definitions.7.3 Unsuccessful Proof AttemptsI made two other attempts to prove properties of language models using REDEX-PLUS-generated code. However, due to the difficulty of the proofs and time con-straints, I did not finish either of them. I discuss these unsuccessful attempts inthis section to analyze whether these attempts reveal limitations in REDEX-PLUSor not.7.3.1 Properties of STLC using the Locally Nameless BindingI tried to prove the same properties of STLC discussed in section 7.2 using thelocally nameless binding representation instead of the named representation. I wasstuck when proving the substitution lemma. I believe additional lemmas about lo-cally nameless binding operations would have helped me proceed with the proof.One possible future extension to REDEX-PLUS is to generate these lemmas auto-matically, which I discuss in section 8.2.In comparison, the LNgen (see section 2.1.1) authors have successfully provensimilar properties of STLC using a locally nameless version of STLC generatedby LNgen [2]. Notice that LNgen generates many binding lemmas, suggestingthat these lemmas are useful when writing proofs and REDEX-PLUS would benefitfrom being able to generate them.7.3.2 Properties of System FI also attempted to prove the same properties of System F, using the named bindingrepresentation. For System F, the final type preservation proof requires not onlythe (term) substitution lemma, but also a similar lemma about substituting a typevariable with a type:Lemma 2 (Type Substitution Lemma). For any environment env, type variable tv,expression e, and types t 1 and t 2, if all type variables bound within e, env, and76t 2 are distinct, and e has type t 1 under (tcons tv env) (i.e. (T (tcons tvenv) e t 1)), then e with tv substituted by t 2 has type t 1 with tv substitutedby t 2 under the context env with tv substituted by t 2 (i.e. (T (substitute tvt 2 env) (substitute tv t 2 e) (substitute tv t 2 t 1))).Notice the premise requiring bound type variables to be distinct 1. This premiseturned out to be difficult to formally express, and I was stuck when proving the typesubstitution lemma. It is unlikely that this proof can be made easier by improve-ments to REDEX-PLUS, as the difficulty in this proof lies in mechanizing the notionof “distinctness” in a proof assistant.7.4 Automatic Solving with SMT SolversREDEX-PLUS supports generating language definitions in the SMT-LIB 2 languagefor automatic theorem proving using an SMT solver (see section 4.2.3). SinceREDEX-PLUS does not support translating variable bindings into SMT-LIB, I willuse an alternative language model of simple arithmetic expressions, shown in figure7.6 for demonstration.I can then use the SMT solver to automatically prove that certain expressionsreduce to other expressions. Here, in order to prove that a relation holds, I firstassert that the relation does not hold, and then ask the SMT solver to check thesatisfiability of the statement. If the statement is unsatisfiable, then it means thestatement must be true. Running the code in figure 7.7 returns (unsat) two times,which means in both cases, the reduction relation holds.7.4.1 Limitations of SMT SolversUnfortunately, there are some serious limitations around using SMT language mod-els generated by REDEX-PLUS, namely, the SMT solver making up non-existentderivation rules when finding solutions, and difficulty with inductive reasoning.Consider the code in figure 7.8, which attempts to find x, which is what theArith (see figure 7.6) expression “(add 1 1)” reduces to. Surprisingly, Z3 thinksx can be zero, despite the derivation rules for the reduction relation say otherwise.1See section 5.1.2 for discussion on a related requirement.77(define-language Arith[e ::= (add e e) (min e e) (mul e e) integer])(define eval-single-step(reduction-relationArith#:domain e#:codomain e[--> (add integer_1 integer_2)(, (+ (term integer_1) (term integer_2))) "add"][--> (min integer_1 integer_2)(, (- (term integer_1) (term integer_2))) "min"][--> (mul integer_a integer_b)(, (* (term integer_a) (term integer_b))) "mul"]))(define eval (compatible-closure eval-single-step Arith e))Figure 7.6: The Redex definition of the a simple arithmetic expression lan-guage and its reduction relation.This happens because Arith-eval, the reduction relation, is represented as anuninterpreted function in SMT-LIB. The SMT solver is free to come up with adefinition for the function however it wants, as long as it satisfies the assertionsabout the function. This problem makes it impossible to use SMT solvers to findterms that satisfy a certain property, limiting their use to checking the correctnessof statements only.Also consider the language model of natural numbers, the “greater or equalto” relation, and the “twice as large as” relation, as defined in figure 7.9. Figure7.10 shows the SMT code for checking the correctness of two simple theoremsregarding this language model: that all natural numbers are greater or equal to zero;and that if two numbers are both twice as large as another number, then the twonumbers are the same. Proving either theorem requires induction over the naturalnumber datatype. When given this code as input, Z3 runs indefinitely withoutgiving any results, and CVC5, with the --quant-ind flag turned on, can prove the78; (mul (add 10 20) (min 20 10)) --> (mul 30 (min 20 10))(push)(assert (not (Arith-eval(Arith-mul (Arith-add (Arith-e-integer 10) (Arith-e-integer 20))(Arith-min (Arith-e-integer 20) (Arith-e-integer 10)))(Arith-mul (Arith-e-integer 30)(Arith-min (Arith-e-integer 20) (Arith-e-integer 10))))))(check-sat)(pop); (mul (add 10 20) (min 20 10)) --> (mul (add 10 20) 10)(push)(assert (not (Arith-eval(Arith-mul (Arith-add (Arith-e-integer 10) (Arith-e-integer 20))(Arith-min (Arith-e-integer 20) (Arith-e-integer 10)))(Arith-mul (Arith-add (Arith-e-integer 10) (Arith-e-integer 20))(Arith-e-integer 10)))))(check-sat)(pop)Figure 7.7: SMT-LIB code for proving two reduction relations. The “push”and “pop” commands are for delimiting each of the two proofs.first theorem but not the second. SMT solvers’ difficulty with inductions is well-known [28, 35]. Given language models often involve inductively defined syntaxstructures, this problem with inductive proofs will likely become an obstacle whenusing SMT solvers with such language models.79(declare-fun x () Arith-e)(assert(Arith-eval (Arith-add (Arith-e-integer 1) (Arith-e-integer 1)) x))(check-sat)(get-model)sat(model(define-fun x () Arith-e(Arith-e-integer 0))(define-fun Arith-eval-single-step((x!0 Arith-e) (x!1 Arith-e)) Booltrue)(define-fun Arith-eval ((x!0 Arith-e) (x!1 Arith-e)) Bool(let ((a!1 (= (ite (= x!1 (Arith-e-integer 0))(Arith-e-integer 0)(Arith-e-integer 2))(Arith-e-integer 0)))(a!2 (= (ite (= x!1 (Arith-e-integer 0))(Arith-e-integer 0)(Arith-e-integer 2))(Arith-e-integer 2))))(or a!1 a!2))))Figure 7.8: SMT-LIB code for finding what the expression (add 1 1) re-duces to, and the Z3 output from running the code. Notice that themodel Z3 came up with states that Arith-eval-single-step is alwaystrue (i.e. every term reduces to every other term), and Arith-eval istrue as long as the reduction result is zero or two, which are both clearlynonsensical.80(define-language Nat[n ::= (S n) Z])(define-judgement-form Nat#:contract (geq n n)[(geq Z Z) "zero"][(geq (S n_1) n_2) (geq n_1 n_2) "succ"][(geq (S n_1) (S n_2)) (geq n_1 n_2) "succ2"])(define-judgement-form Nat#:contract (twice n n)[(twice Z Z) "identity"][(twice (S (S n_1)) n_2) (twice n_1 n_2) "twice"])Figure 7.9: The Redex definition of natural numbers and two relations.(push)(assert (not (forall ((n Nat-n)) (Nat-geq n Nat-Z))))(check-sat)(pop)(push)(assert (not (forall ((n Nat-n) (n21 Nat-n) (n22 Nat-n))(=> (Nat-twice n21 n) (Nat-twice n22 n) (= n21 n22)))))(check-sat)(pop)Figure 7.10: SMT-LIB code for checking the correctness of two simple the-orems about natural numbers.81Chapter 8Conclusion8.1 ContributionsIn this thesis I presented REDEX-PLUS, an implementation of a computer sciencemetanotation to bridge the gap between intuitive, informal notations used in rea-soning about programming languages, and proof assistants in which facts about thelanguages can be formally proven.During the course of the work, I identified a small, well-defined subset of Re-dex as the input of REDEX-PLUS, and implemented a modular, extensible trans-lation procedure from this Redex subset to a number of proof assistant targets. Ihave also shown that the generated models can be used to prove theorems aboutthe language models. To my knowledge, REDEX-PLUS is the only tool capable offaithfully translating language models with multiple types of bound variables 1 intomultiple proof assistant languages.1For example, term variables and type variables828.2 Future WorkGenerating Binding LemmasMany properties of binding operations are useful in proofs. For example, the proofof type preservation of STLC uses a lemma about binding operations (see section7.2.3). It is may be possible to generate a selection of binding lemmas and theirproofs as a part of the translation process. LNgen (see section 2.1.1) which gener-ates such lemmas and proofs, may serve as a useful point of reference.Ellipsis PatternsEllipsis patterns, which denote repetitions of sub-patterns, are not supported, notbecause of any theoretical incompatibilities (which is the reason why, for instance,arbitrary Racket expressions in side-conditions are not allowed), but simply dueto complexities and difficulties in implementation. Ellipsis in judgement forms isa similar feature currently unsupported for the same reasons.Repetition of sub-patterns can be represented as a list containing terms rep-resenting these sub-patterns. This would likely require generating data structuredefinitions to represent the sub-patterns. While lists can be easily defined if not di-rectly importable from the standard libraries, ad hoc list operations and additionalconstraints on list lengths will be required for more complicated operations (see3.1.2). However, it is worth noting that even supporting just a small subset of ellip-sis patterns (allowing only non-terminals as sub-patterns, for example) will alreadymassively improve the expressiveness of REDEX-PLUS.Non-terminal SubsetsOverlapping non-terminals are useful for denoting that certain terms (e.g. “values”that cannot be further reduced) are a subset of some other terms (e.g. all expres-sions). They are problematic to express because REDEX-PLUS’s targets generallydo not allow one type (non-terminal) to be the subset of another.However, it might be possible to side-step this restriction by turning non-terminals denoting a subset of another non-terminal into relations on terms of theother non-terminal. For example, in the case of expressions and values, it might be83possible to represent expressions normally as non-terminals, and represent valuesas expressions that satisfy a certain condition. Then, all occurrences of values in thelanguage model will be represented by expressions, accompanied by the require-ment that it satisfies the “value” condition. This approach will allow REDEX-PLUSto adequately support many common use cases of overlapping non-terminals, butcomes with two major difficulties: first, there needs to be some way of knowingwhich non-terminals should be represented as a subset of other non-terminals, ei-ther manually, or automatically but at the risk of unexpected outcomes; second,inserting the condition might be difficult in places such as function signatures.Context Closures for Reduction RelationsContext closures are useful for specifying the order of reduction, but are currentlyunsupported because they require a non-terminal to be used as the reduction con-text, but defining this non-terminal definition is problematic: it will overlap withother non-terminals, and it will contain holes which are difficult to properly trans-late. In addition, context closure definitions often use non-terminals that are subsetsof other non-terminals (for example, the aforementioned “values” non-terminal),which are not supported either.To meaningfully support context closures, there needs to be a way to reasonablyhandle non-terminals intended to be used as reduction contexts. One possible wayis to use them only when generating the definition of the context closure, and do notgenerate code for them at all; alternatively, they can be translated into a predicatethat is true only for terms within the reduction context. The generation of thecontext closure themselves would require first generating the compatible closure,and filtering out cases where the term to be reduced is not in the reduction context.84Bibliography[1] A. Armando, J. Mantovani, and L. Platania. Bounded model checking ofsoftware using smt solvers instead of sat solvers. In A. Valmari, editor,Model Checking Software, 2006. doi:10.1007/s10009-008-0091-0. → page41[2] B. Aydemir and S. Weirich. Lngen: Tool support for locally namelessrepresentations. 2010. doi:20.500.14332/7902. → pages 7, 76[3] B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce,P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic.Mechanized metatheory for the masses: The poplmark challenge. InTheorem Proving in Higher Order Logics, 2005. doi:10.1007/11541868 4.→ page 49[4] J. W. Backus, F. L. Bauer, J. Green, C. Katz, J. McCarthy, A. J. Perlis,H. Rutishauser, K. Samelson, B. Vauquois, J. H. Wegstein, A. vanWijngaarden, M. Woodger, and P. Naur. Revised report on the algorithmlanguage algol 60. Commun. ACM, 6(1):1–17, Jan. 1963.doi:10.1145/366193.366201. → page 1[5] H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann,A. Mohamed, M. Mohamed, A. Niemetz, A. No¨tzli, A. Ozdemir, M. Preiner,A. Reynolds, Y. Sheng, C. Tinelli, and Y. Zohar. cvc5: A versatile andindustrial-strength smt solver. In Tools and Algorithms for the Constructionand Analysis of Systems, 2022. doi:10.1007/978-3-030-99524-9 24. →page 42[6] C. Barrett and C. Tinelli. Satisfiability Modulo Theories. 2018.doi:10.1007/978-3-319-10575-8 11. → page 41[7] C. Barrett, P. Fontaine, and C. Tinelli. The SMT-LIB Standard: Version 2.6.Technical report, Department of Computer Science, The University of Iowa,2017. URL https://smtlib.cs.uiowa.edu/language.shtml. → page 4285[8] S. Berghofer and C. Urban. A head-to-head comparison of de bruijn indicesand names. Electronic Notes in Theoretical Computer Science, 174(5),2007. doi:10.1016/j.entcs.2007.01.018. Proceedings of the FirstInternational Workshop on Logical Frameworks and Meta-Languages:Theory and Practice (LFMTP 2006). → page 49[9] P. Boutillier, S. Glondu, B. Gre´goire, H. Herbelin, P. Letouzey, P.-M. Pe´drot,Y. Re´gis-Gianas, M. Sozeau, A. Spiwack, and E. Tassi. Coq 8.4 ReferenceManual. Research report, Inria, July 2014. URLhttps://hal.inria.fr/hal-01114602. The Coq Development Team. → page 37[10] A. Bove, P. Dybjer, and U. Norell. A brief overview of agda – a functionallanguage with dependent types. In Theorem Proving in Higher OrderLogics, 2009. doi:10.1007/978-3-642-03359-9 6. → page 38[11] M. Bravenboer, K. T. Kalleberg, R. Vermaas, and E. Visser. Stratego/xt 0.17.a language and toolset for program transformation. Science of ComputerProgramming, 72(1), 2008. doi:10.1016/j.scico.2007.11.003. Special Issueon Second issue of experimental software and toolkits (EST). → page 9[12] A. Chargue´raud. The locally nameless representation. Journal of AutomatedReasoning, 49(3), 2011;2012;. doi:10.1007/s10817-011-9225-2. → pages49, 51[13] L. Cordeiro, B. Fischer, and J. Marques-Silva. Smt-based bounded modelchecking for embedded ansi-c software. IEEE Transactions on SoftwareEngineering, 38(4), 2012. doi:10.1109/TSE.2011.59. → page 41[14] N. de Bruijn. Lambda calculus notation with nameless dummies, a tool forautomatic formula manipulation, with application to the church-rossertheorem. Indagationes Mathematicae (Proceedings), 75(5), 1972.doi:10.1016/1385-7258(72)90034-0. → pages 3, 43[15] L. de Moura and N. Bjørner. Z3: An efficient smt solver. In C. R.Ramakrishnan and J. Rehof, editors, Tools and Algorithms for theConstruction and Analysis of Systems, 2008.doi:10.1007/978-3-540-78800-3 24. → pages 41, 42[16] L. De Moura and N. Bjørner. Satisfiability modulo theories: Introductionand applications. Commun. ACM, 54(9), Sept. 2011.doi:10.1145/1995376.1995394. → page 4186[17] D. Delahaye. A tactic language for the system coq. In M. Parigot andA. Voronkov, editors, Logic for Programming and Automated Reasoning,2000. doi:10.1007/3-540-44404-1 7. → page 37[18] S. Dolan and L. White. Syntax with shifted names. 2019. → page 52[19] S. Dolan and L. White. shifted-names, 2019. URLhttps://github.com/lpw25/shifted-names. → page 52[20] R. B. Findler, C. Klein, B. Fetscher, and M. Felleisen. Redex: Practicalsemantics engineering. URL https://docs.racket-lang.org/redex/. → pages3, 10[21] M. Gabbay and A. Pitts. A new approach to abstract syntax involvingbinders. In Proceedings. 14th Symposium on Logic in Computer Science(Cat. No. PR00158), 1999. doi:10.1109/LICS.1999.782617. → page 54[22] G. Gentzen. Untersuchungen u¨ber das logische schließen. i. MathematischeZeitschrift, 39, 1935. doi:0.1007/BF01201353. → page 1[23] R. Harper. Practical foundations for programming languages, 2011. → page3[24] L. C. Kats and E. Visser. The spoofax language workbench: Rules fordeclarative specification of languages and ides. In Proceedings of the ACMInternational Conference on Object Oriented Programming SystemsLanguages and Applications, 2010. doi:10.1145/1869459.1869497. →pages 3, 9[25] A. W. Keep and R. K. Dybvig. A nanopass framework for commercialcompiler development. In Proceedings of the 18th ACM SIGPLANInternational Conference on Functional Programming, ICFP ’13, 2013.doi:10.1145/2500365.2500618. → page 59[26] C. Klein, J. Clements, C. Dimoulas, C. Eastlund, M. Felleisen, M. Flatt,J. A. McCarthy, J. Rafkind, S. Tobin-Hochstadt, and R. B. Findler. Run yourresearch: On the effectiveness of lightweight mechanization. 2012.doi:10.1145/2103656.2103691. → pages 3, 10[27] U. K. Le Guin. A Wizard of Earthsea. Parnassus Press, 1968. → page 43[28] K. R. M. Leino. Automating induction with an smt solver. In V. Kuncak andA. Rybalchenko, editors, Verification, Model Checking, and AbstractInterpretation, 2012. doi:10.1007/978-3-642-27940-9 21. → page 7987[29] Y. Li, A. Albarghouthi, Z. Kincaid, A. Gurfinkel, and M. Chechik. Symbolicoptimization with smt solvers. In Proceedings of the 41st ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages,2014. doi:10.1145/2535838.2535857. → page 41[30] S. Owens, P. Bo¨hm, F. Zappa Nardelli, and P. Sewell. Lem: A lightweighttool for heavyweight semantics. In Interactive Theorem Proving, 2011.doi:10.1007/978-3-642-22863-6 27. → pages 3, 8[31] F. Pfenning and C. Elliott. Higher-order abstract syntax. In Proceedings ofthe ACM SIGPLAN 1988 Conference on Programming Language Designand Implementation, 1988. doi:10.1145/53990. → page 3[32] B. Pientka. Beluga: Programming with dependent types, contextual data,and contexts. In M. Blume, N. Kobayashi, and G. Vidal, editors, Functionaland Logic Programming, 2010. doi:10.1007/978-3-642-12251-4 1. → page40[33] B. C. Pierce. Types and Programming Languages. MIT Press, 2002. →pages 12, 43, 48, 49, 69[34] B. C. Pierce, A. A. de Amorim, C. Casinghino, M. Gaboardi, M. Greenberg,C. Hrit¸cu, V. Sjo¨berg, A. Tolmach, and B. Yorgey. Programming LanguageFoundations, volume 2 of Software Foundations. Electronic textbook, 2023.Version 6.4, http://softwarefoundations.cis.upenn.edu. → page 69[35] A. Reynolds and V. Kuncak. Induction for smt solvers. In D. D’Souza,A. Lal, and K. G. Larsen, editors, Verification, Model Checking, and AbstractInterpretation, 2015. doi:10.1007/978-3-662-46081-8 5. → page 79[36] D. Sarkar, O. Waddell, and R. K. Dybvig. Educational pearl: A nanopassframework for compiler education. Journal of Functional Programming, 15(5), 2005. doi:10.1017/S0956796805005605. → page 59[37] P. Sewell, F. Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, andR. Strnisˇa. Ott: Tool Support for Semantics. URLhttps://www.cl.cam.ac.uk/∼pes20/ott/top2.html. → pages 7, 8[38] P. Sewell, F. Z. Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, andR. Strnisˇa. Ott: Effective tool support for the working semanticist. Journalof Functional Programming, 20(1), 2010.doi:10.1017/S0956796809990293. → pages 3, 788[39] G. L. Steele. It’s time for a new old language, 2017. URLhttps://labs.oracle.com/pls/apex/f?p=94065:10:175964141145:4986. →pages 2, 3[40] P. Wadler, W. Kokke, and J. G. Siek. Programming Language Foundationsin Agda. Aug. 2022. URL https://plfa.inf.ed.ac.uk/22.08/. → page 68[41] J. Xu. The redex-plus language. Aug. 2023. doi:10.5281/zenodo.8251566.→ pages iii, 489Appendix AEvaluation ProofsThis chapter contains Coq and Agda proofs done for evaluating REDEX-PLUS. Seesection 7.2 for more details on the proofs.90A.1 Coq ProofsA.1.1 ProgressTheorem Prog : forall e t, STLC_nil |- e : t -> STLC_Value e \/exists e', e >-> e'.↪→Proof with eauto.intros e t HT.remember STLC_nil as env0.generalize dependent Heqenv0.induction HT; intros Heqenv0.- inversion H; subst.+ inversion H0.+ inversion H2.- left. autoderive.- left. autoderive.- right.destruct IHHT1; subst...+ destruct H; inversion HT1; subst.exists (sub variable e__a e).autoderive.+ inversion H.exists (STLC_app x e__a).autoderive.Qed.A.1.2 Auxiliary Lemmas for Substitution LemmaLemmas about STLC-diffLemma same_not_diff : forall v, ˜ Is_true (STLC_diff v v).Proof with eauto.91intros v.unfold STLC_diff.rewrite String.eqb_refl...Qed.Lemma neq_diff : forall v v', v <> v' <-> Is_true (STLC_diff v v').Proof with eauto.intros v v'.unfold STLC_diff.split.- intros Hneq.apply String.eqb_neq in Hneq.rewrite Hneq.unfold Is_true...- intros Hd.destruct (String.string_dec v v')...contradict Hd.rewrite e.rewrite String.eqb_refl...Qed.Main lemmas about changing the environmentLemma Extend : forall env env',(forall x t, x : t <- env -> x : t <- env') ->(forall x y tx ty, x : tx <- (y : ty :: env) -> x : tx <- (y : ty:: env')).↪→Proof using Type with eauto.intros env env' HIn x y tx ty HxIn.inversion HxIn; autoderive.Qed.Lemma Rename : forall env env',92(forall v t, v : t <- env -> v : t <- env') ->(forall e t, env |- e : t -> env' |- e : t).Proof using Type with eauto.intros env env' HIn e t HT.generalize dependent env'.induction HT; intros env' HIn.- apply STLCProp_context.apply HIn...- autoderive.- apply STLCProp_abstract.apply IHHT.intros v t.apply Extend...- eapply STLCProp_apply...Qed.Corollaries about changing the environmentCorollary Weaken : forall env e t, STLC_nil |- e : t -> env |- e :t.↪→Proof with eauto.intros env e t HT0.apply (Rename STLC_nil env)...intros v t0 Hnil.inversion Hnil.Qed.Corollary Drop : forall env x e t1 t2 t,(x : t1 :: (x : t2 :: env) |- e : t) -> (x : t1 :: env |- e :t).↪→Proof with eauto.intros env x e t1 t2 t HT.93apply (Rename (x : t1 :: (x : t2 :: env)))...intros v t0 HIn.destruct (string_dec x v); subst.- inversion HIn; subst.+ autoderive.+ apply same_not_diff in H5.contradiction.- apply STLCProp_cons.+ inversion HIn; subst.* contradiction.* inversion H4; subst...contradiction.+ apply neq_diff...Qed.Corollary Swap : forall env x y e t1 t2 t,x <> y ->(x : t1 :: (y : t2 :: env)) |- e : t ->(y : t2 :: (x : t1 :: env)) |- e : t.Proof with eauto.intros env x y e t1 t2 t Hdiff HT.apply (Rename (x : t1 :: (y : t2 :: env)))...intros v t0 HIn.inversion HIn; subst.- eapply STLCProp_cons.+ autoderive.+ apply neq_diff...- inversion H4; subst; autoderive...Qed.94A.1.3 Substitution LemmaLemma Subst :forall env x xt v e t,STLC_nil |- v : xt-> x : xt :: env |- e : t-> env |- sub x v e : t.Proof with eauto.intros env x xt v e t HTv HTe.generalize dependent x.generalize dependent xt.generalize dependent env.generalize dependent t.induction e; intros t env xt HTv x HTe.- inversion HTe. subst.simpl sub.destruct (String.string_dec x s).+ rewrite <- String.eqb_eq in e.rewrite e.apply Weaken.inversion H1; subst...rewrite String.eqb_eq in e.subst.contradict H6.apply same_not_diff.+ rewrite <- String.eqb_neq in n.rewrite n.apply STLCProp_context.inversion H1; subst...rewrite String.eqb_refl in n.inversion n.95- inversion HTe.simpl sub.eapply STLCProp_apply...- inversion HTe.autoderive.- inversion HTe. subst.destruct (String.string_dec x s); simpl.+ rewrite <- String.eqb_eq in e0.rewrite e0.apply STLCProp_abstract.eapply Drop.rewrite String.eqb_eq in e0.subst...+ apply STLCProp_abstract.apply Swap in H4...rewrite <- String.eqb_neq in n.rewrite n...Qed.A.1.4 PreservationTheorem Pres : forall e t e', STLC_nil |- e : t -> e --> e' ->STLC_nil |- e' : t.↪→Proof with eauto.intros e t e' HT HR.remember STLC_nil as env0.generalize dependent e'.induction HT; intros e' HR;inversion HR; subst; try eapply STLCProp_apply...eapply Subst...inversion HT1...Qed.96A.2 Agda ProofsA.2.1 Progressprog : ∀ e {t} → ∅ ` e ∈ t → STLC-Value e unionmulti ∃[ e' ] (e e')prog (STLC-v x) (STLCProp-context ())prog (STLC-app e1 e2) (STLCProp-apply T1 T2) with prog e1 T1... | inj2 (e3 , e1R) = inj2 (STLC-app e3 e2 , STLCProp-beta-cc-appe1R)↪→... | inj1 x with e1... | STLC-lam x1 x2 x3 = inj2 ([ x1 ⇒ e2 ] x3 ,STLCProp-beta-single-step-subst-cc)↪→prog (STLC-e-natural x) V = inj1 STLCProp-natural-is-valueprog (STLC-lam x x1 e) V = inj1 STLCProp-lam-is-valueA.2.2 Auxiliary Lemmas for Substitution LemmaLemmas about STLC-diffsame-not-diff : ∀ {x} → STLC-diff x x Z≡ truesame-not-diff {x} with x ?= x... | no Hneq' = ⊥-elim (Hneq' refl)... | yes refl with false Data.Bool.Properties.?= true... | no Hneq = Hneqdiff-neq : ∀ {x x'} → STLC-diff x x' ≡ true → x Z≡ x'diff-neq {x} {x'} Hdiff with x ?= x'diff-neq {x} {x'} () | yes refl... | no Hneq = Hneqneq-diff : ∀ {x y} → x Z≡ y → STLC-diff x y ≡ trueneq-diff {x} {y} Hneq with x ?= y... | yes refl = ⊥-elim (Hneq refl)... | no Hneq' = refl97Main lemmas about changing the environmentextend : ∀ {env env'}→ (∀ {x t} → env 3 x ∈ t → env' 3 x ∈ t)→ (∀ {x y tx ty} → (y ∈ ty :: env) 3 x ∈ tx → (y ∈ ty :: env')3 x ∈ tx)↪→extend HIn STLCProp-axiom = STLCProp-axiomextend HIn (STLCProp-cons x x1) = STLCProp-cons (HIn x) x1rename : ∀ {env env'}→ (∀ {v t} → env 3 v ∈ t → env' 3 v ∈ t)→ (∀ {e t} → env ` e ∈ t → env' ` e ∈ t)rename HIn (STLCProp-context x) = STLCProp-context (HIn x)rename HIn STLCProp-natural = STLCProp-naturalrename HIn (STLCProp-abstract HT) = STLCProp-abstract (rename(extend HIn) HT)↪→rename HIn (STLCProp-apply HT HT1) = STLCProp-apply (rename HInHT) (rename HIn HT1)↪→Corollaries about changing the environmentweaken : ∀ {env e t} → ∅ ` e ∈ t → env ` e ∈ tweaken {env} HT = rename HIn HTwhereHIn : ∀ {v t} → ∅ 3 v ∈ t → env 3 v ∈ tHIn ()drop : ∀ {env x e t1 t2 t}→ (x ∈ t1 :: (x ∈ t2 :: env)) ` e ∈ t→ (x ∈ t1 :: env) ` e ∈ tdrop {env} {x} {e} {t1} {t2} HT = rename HIn HTwhereHIn : ∀ {x' x't} → (x ∈ t1 :: (x ∈ t2 :: env)) 3 x' ∈ x't→ (x ∈ t1 :: env) 3 x' ∈ x't98HIn STLCProp-axiom = STLCProp-axiomHIn (STLCProp-cons STLCProp-axiom x1) = ⊥-elim (same-not-diffx1)↪→HIn (STLCProp-cons (STLCProp-cons HIn' x) x1) = STLCProp-consHIn' x↪→swap : ∀ {env x y tx ty e t}→ x Z≡ y→ (x ∈ tx :: (y ∈ ty :: env)) ` e ∈ t→ (y ∈ ty :: (x ∈ tx :: env)) ` e ∈ tswap {env} {x} {y} {tx} {ty} {e} {t} Hneq HT = rename HIn HTwhereHIn : ∀ {x' x't} → (x ∈ tx :: (y ∈ ty :: env)) 3 x' ∈ x't→ (y ∈ ty :: (x ∈ tx :: env)) 3 x' ∈ x'tHIn STLCProp-axiom = STLCProp-cons STLCProp-axiom (neq-diffHneq)↪→HIn (STLCProp-cons STLCProp-axiom x1) = STLCProp-axiomHIn (STLCProp-cons (STLCProp-cons x x2) x1) = STLCProp-cons(STLCProp-cons x x1) x2↪→A.2.3 Substitution Lemmasubst : ∀ {env v e to vt t}→ ∅ ` to ∈ vt→ (v ∈ vt :: env) ` e ∈ t→ env ` [ v ⇒ to ] e ∈ tsubst {v = v} HTv (STLCProp-context {`variable = x}STLCProp-axiom) with v ?= x↪→... | yes refl = weaken HTv... | no Hneq = ⊥-elim (Hneq refl)subst {v = v} HTv (STLCProp-context {`variable = x} (STLCProp-consHIn' Hdiff)) with v ?= x↪→... | yes refl = ⊥-elim (diff-neq Hdiff refl)99... | no Hneq = STLCProp-context HIn'subst HTv STLCProp-natural = STLCProp-naturalsubst {v = v} HTv (STLCProp-abstract {variable:a = x} HTe') with v?= x↪→... | yes refl = STLCProp-abstract (drop HTe')... | no Hneq = STLCProp-abstract (subst HTv (swap (Z≡-sym Hneq)HTe'))↪→subst HTv (STLCProp-apply HTe1 HTe2) = STLCProp-apply (subst HTvHTe1) (subst HTv HTe2)↪→A.2.4 Preservationpres : ∀ {e t e'}→ ∅ ` e ∈ t→ e −→ e'→ ∅ ` e' ∈ tpres (STLCProp-context x) ()pres STLCProp-natural ()pres (STLCProp-abstract x) ()pres (STLCProp-apply (STLCProp-abstract x) x1) (β−→ x2) = substx1 x↪→pres (STLCProp-apply x x1) (app−→*l y) = STLCProp-apply (pres xy) x1↪→pres (STLCProp-apply x x1) (app−→*r x2 y) = STLCProp-apply x(pres x1 y)↪→100
Thesis/Dissertation
eng
Computer Science
Vancouver : University of British Columbia Library
Attribution-NonCommercial-NoDerivatives 4.0 International
Graduate
Bowman, William J. (Professor of computer science)
Redex-plus : a metanotation for programming languages
Text