# A semantics of K into dedukti

Amélie Ledein, Valentin Blot, Catherine Dubois

► To cite this version:

Amélie Ledein, Valentin Blot, Catherine Dubois. A semantics of K into dedukti. TYPES 2022 - 28th International Conference on Types for Proofs and Programs (TYPES), Jul 2023, Nantes, France. 10.4230/LIPIcs.TYPES.2022.23 . hal-03895834v2

HAL Id: hal-03895834

https://inria.hal.science/hal-03895834v2

Submitted on 8 Dec 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Semantics of K into Dedukti

Amélie Ledein

<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /></figure>

ID

Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, France

Valentin Blot

<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /></figure>

Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, France

Catherine Dubois

<figure><img src="image_6.png" /></figure>

<figure><img src="image_7.png" /></figure>

ID

ENSIIE, Samovar, Évry-Courcironnes, France

## Abstract

K is a semantical framework for formally describing the semantics of programming languages thanks to a BNF grammar and rewriting rules on configurations. It is also an environment that offers various tools to help programming with the languages specified in the formalism. For example, it is possible to execute programs thanks to the generated interpreter, or to check their properties thanks to the provided automatic theorem prover called the KPROVER. K is based on MATCHING LOGIC, a first-order logic with an application and fixed-point operators, extended with symbols to encode equality, typing and rewriting. This specific MATCHING LOGIC theory is called KORE.

DEDUKTI is a logical framework having for main goal the interoperability of proofs between different formal proof tools. Several translators to DEDUKTI exist or are under development, in order to automatically translate formalizations written, for instance, in COQ or PVS. DEDUKTI is based on the λΠ-calculus modulo theory, a λ-calculus with dependent types and extended with a primitive notion of computation defined by rewriting rules. The flexibility of this logical framework allows to encode many theories ranging from first-order logic to the Calculus of Constructions.

In this article, we present a paper formalization of the translation from K into KORE, and a paper formalization and an automatic translation tool, called KAMELO, from KORE to DEDUKTI in order to execute programs in DEDUKTI.

**2012 ACM Subject Classification** Theory of computation → Operational semantics

**Keywords and phrases** Programming language, Semantics, Rewriting, Logical framework, Type theory

**Digital Object Identifier** 10.4230/LIPIcs.TYPES.2022.12

**Supplementary Material** Software: https://gitlab.com/semantiko/kamelo
archived at swh:1:dir:9353026d393b52e5bc149a469a3d2386fb923dff

**Funding** Amélie Ledein: Digicosme and EuroProofNet

**Acknowledgements** We want to thank the K team, especially Andrei Arusoaie, Xiaohong Chen, Denisa Diaconescu, Everett Hildenbrandt, Zhengyao Lin, Dorel Lucanu, Ana Pantilie and Traian-Florin Serbanuta for their prompt responses to our many questions.

## 1 Introduction

The main objective of formal methods is to obtain greater confidence in programs. Before verifying a program, it must be written in a programming language whose syntax and semantics are precisely known. Therefore, we must first have a formalization of the semantics of the programming language used to write the program we wish to verify. Several tools make it possible to write formal semantics for example CENTAUR [7], ASF+SDF [23], OTT [20], SAIL [3], LEM [17] or K [19, 2]. In this article, we are only interested in the latter, since there are currently a large number of programming language semantics written in K such as JAVA [6], C [13] or JAVASCRIPT [18].

<figure><img src="image_8.png" /></figure>

© Amélie Ledein, Valentin Blot, and Catherine Dubois;

licensed under Creative Commons License CC-BY 4.0

28th International Conference on Types for Proofs and Programs (TYPES 2022).

Editors: Delia Kesner and Pierre-Marie Pédrot; Article No. 12; pp. 12:1–12:22

Leibniz International Proceedings in Informatics

<figure><img src="image_9.png" /></figure>

LIPICS Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
12:2 A Semantics of K into Dedukti

K is a semantical framework that offers many features for writing a semantics such as attributes to specify evaluation strategies. Once the semantics of a language $\mathcal{L}$ has been specified, K allows to execute a program $\mathcal{P}$ written in $\mathcal{L}$ but also offers the possibility of verifying some properties – expressed in the form of reachability properties – on the program $\mathcal{P}$ using the automatic theorem prover KPROVER [21]. As it is possible to automatically translate K semantics into a MATCHING LOGIC theory named KORE, the particularity of the K framework is to see any semantics $\mathcal{S}$ of a programming language $\mathcal{L}$ as a logical theory $\Gamma^\mathcal{L}$. That is the reason we look at the translation of K into DEDUKTI, which is a logical framework based on the $\lambda\Pi$-CALCULUS MODULO THEORY having for main goal the interoperability of proofs between different formal proof tools.

In this article, we are more particularly interested in the translation into DEDUKTI of any semantics written in K in order to execute programs in DEDUKTI. Our first contribution is a paper formalization of the translation from K into KORE. As no article has been yet published on this translation, this contribution was elaborated by reverse engineering on KORE files as well as thanks to discussions with the K team. Independently, we formalize transformations similar to what was done in IsaK [15, 16], which is a formalization in ISABELLE – but not based on KORE – of the static and dynamic semantics of K. In addition, the second contribution is a paper formalization and an automatic tool, called KAMELO [1], from KORE to DEDUKTI in order to execute programs in DEDUKTI. The general overview of the translation pipeline presented in this article is available in Figure 1. This is the first translation into DEDUKTI involving a semantical framework.

<figure><img src="image_10.png" /><figcaption>Figure 1 Overview of the translation pipeline presented in this article.</figcaption></figure>

A long-term goal is not only to execute a program $\mathcal{P}$ written with the formalized language $\mathcal{L}$ within DEDUKTI, but also to verify the proofs established by the KPROVER, or even make this proof with DEDUKTI if the KPROVER has failed, and also formally check meta-properties about the language $\mathcal{L}$. This long-term goal can be seen as a new pipeline for program verification, which is parametrized by a programming language and leaves the user free to choose the proof assistant they wish.

This article is structured as follows: first, we explain how to write a K semantics (Section 2). Then, we present a mathematical structure $\mathcal{M}$ to abstract K in order to formalize some internal transformations that K does on semantics (Section 3). Thanks to the mathematical structure $\mathcal{M}$, we formalize a computational translation $\mathcal{T}$ into the $\lambda\Pi$-CALCULUS MODULO THEORY (Section 4). Finally, we present our implementation of $\mathcal{T}$ (Section 5).
In the following, the keywords of a language or what is native in a language will be distinguished by color. The language of DEDUKTI will be distinguished by a **blue color**, the language of K by **an orange color** and the language of KORE by **a red color**. These facilitate reading but are not necessary for understanding.

## 2 What is the K framework?

This section introduces the K framework by explaining how to write a semantics using a small example, and then by presenting the diversity of K features. This section ends with the K grammar that we consider in the rest of this article.

### 2.1 A first K semantics

In this subsection, we show an example based on booleans and two binary symbols, which are lazily evaluated, to illustrate how to write a semantics in K. As usual, the first step to formalize a semantics is to define the syntax and then the semantics associated to the syntax.

#### 2.1.1 Define the syntax of a language

Defining the syntax of a language in K is similar to writing a BNF grammar. This is done in the module LAZY-SYNTAX (Figure 2 - lines 1 to 9) with the definition of booleans, which are typed by sort `MyBool`, a lazy disjunction, noted `||`, and a lazy conjunction, noted `&&`. A terminal symbol will be written between quotes, as for example `"||"`, and anything else in **bold** will therefore be a non-terminal symbol. In order to make the syntax parseable, it is possible to use *attributes*, i.e. keywords between square brackets, allowing to specify the associativity (`left`, `right`, `non-assoc`) or to add parentheses to the language (`bracket`). We explain the other possible attributes as we go along. Moreover, K supports the Kleene operators `*` and `+`, written `List` and `NeList` respectively.

<figure><img src="image_11.png" /><figcaption>Figure 2 Syntax and semantics of booleans, a lazy disjunction and a lazy conjunction.</figcaption></figure>

The subtyping relation between the sorts `MyBool` and `BExp` (Figure 2 - line 5) means that the boolean values `true` and `false` are also boolean expressions. In addition, any symbol has either the attribute `constructor`, when the symbol is an element of the syntax, or the attribute `function`, when the symbol is a *helper function* used to define the semantics, e.g. functions to manipulate the environment.
## 2.1.2 Define the semantics associated to the syntax

The main ingredients for defining the semantics of each element of the syntax are *configurations* and *rewriting rules*. Some attributes are also useful to define evaluation strategies. The semantics of a lazy disjunction and a lazy conjunction is defined in the module LAZY (Figure 2 - lines 10 to 17) which imports the syntax module (line 11 thanks to *imports*).

### 2.1.2.1 Configurations

A *configuration* models the state of the program and is composed of *cells*. For example, the configuration $\langle\langle x = 10; \rangle_k \langle x \mapsto 0 \rangle_{env}\rangle$ is composed of two cells, one labelled by *k* containing the program to be executed and the other labelled by *env* containing the current values of the variables. In the example in Figure 2, the configuration contains only the cell *k* (line 12). The configuration variable `$PGM$` will contain the parsed program given by the user.

### 2.1.2.2 Rewriting rules

A $K$ rewriting rule is a 1st order rule which can be either conditional, noted `rule LHS => RHS requires Cond`, or unconditional, noted `rule LHS => RHS`. Moreover, a $K$ rewriting rule can be non-linear, i.e. variables in the left-hand side can appear several times. The variables in the left-hand side (`LHS`) can be omitted using a wildcard (`_`) when they are not used in the right-hand side (`RHS`), as in the rule on line 14 or 16 (Figure 2). Finally, $K$ supports partial rewriting modulo ACUI, i.e. associativity (`assoc`), commutativity (`comm`), identity (`unit`) and idempotence (`idem`).

Any $K$ rewriting rule can be applied to a whole configuration, if the rewriting rule defines the semantics associated to the syntax, or does not mention the configuration, if the rewriting rule defines a helper function. This distinction is illustrated more precisely in the next paragraph.

### 2.1.2.3 Evaluation strategies

To define an evaluation strategy, i.e. specifying the order in which the sub-expressions are evaluated, it is possible to use *contexts* (*context*) as is conventionally done, but also *context aliases* (*context alias*) which allow contexts to be generated automatically rather than systematically writing similar contexts.

There are also two attributes for defining an evaluation strategy: `strict` defines non-deterministic strategies and `seqstrict` defines deterministic strategies from left to right by default. It is also possible to restrict the list of sub-expressions that must be evaluated by giving a list of numbers as done in Figure 2. Indeed, the attribute `strict(1)` forces the evaluation of the first argument of the symbol `&&`, and then it is possible to apply one of the rules on line 15 or 16. To use these attributes, the user needs to define the sort `KResult` which allows to distinguish final values from expressions thanks to subtyping. For instance, as `MyBool` is a sub-sort of `KResult` (Figure 2 - line 4), a final value is either `false` or `true`.

Whichever way an evaluation strategy is defined, it is translated using $K$ *computations* and *freezers*. A $K$ computation is a list of computations to be performed sequentially and built with the constructors `.` and `^`, whereas a freezer is a symbol that encapsulates the part of the computation that should not yet be modified, i.e. the tail of the $K$ computation, while waiting for the head of the $K$ computation to be evaluated. This mechanism is inspired by evaluation contexts [26] and continuations $v \frown C$.

The rewriting rules generated by `strict(1)` (Rules n°1 and n°2, with the attributes `heat` and `cool`) as well as an example of an execution are detailed in Figure 3. Freezers are noted
(\*<sub>sym</sub><sup>nb</sup> arg) where *sym* is a symbol, *nb* the number of the argument whose value we expect, and *arg* the list of other arguments. As the symbol **&&** has the attribute **constructor**, the rules on lines 15 and 16 (Figure 2) are respectively translated by K into the rules n°3 and n°4 (Figure 3). In contrast, as the symbol **||** has the attribute **function**, so K does not transform the rules on lines 13 and 14 (Figure 2). The translation of the attribute **strict(1)** into rewriting rules is similar in the case of attributes **strict** and **seqstrict**.

<figure><img src="image_12.png" /><figcaption>Figure 3 Translation of the attributes strict(1) and an example execution.</figcaption></figure>

In this article, a rewriting rule that has a **constructor** symbol as its head is called *semantical*, and a rewriting rule that has a **function** symbol as its head is called *evaluation*.

The attributes **assoc**, **comm**, **unit** and **idem** generate equations, named *equational rules*. A rewriting rule with the attribute **heat** or **cool** is called an *evaluation strategy rule*.

## 2.2 Additional features

The previous subsection illustrated the main K features. However, there are many other features, coming from attributes or the K standard library, in order to bring more precision to a semantics.

### 2.2.1 Definable features thanks to the attributes

K has about 70 attributes. Papers about K, e.g. [19], mention very few of them and the documentation [2] is not exhaustive and complete. However, many features require the use of attributes. This section presents the list of attributes in Figure 4 that we hope to be as exhaustive as possible.

<figure><img src="image_13.png" /><figcaption>Figure 4 List of K attributes as exhaustive as possible.</figcaption></figure>
12:6 A Semantics of K into Dedukti

**About importation.** What comes from the K standard library, briefly presented in Section 2.2.2, has the attribute hook. Furthermore, we can specify the visibility of a module or an import ($A_{visibility}$) or that a module is only useful for some backends ($A_{backend}$).

**About parsing.** The user can precise constraints about parsing such as the associativity of symbols (**left**, **right**, **non-assoc**) but also to reject cases of parsing ambiguity (**prefer**, **avoid**, **applyPriority**). Moreover, it is possible to type a part of the AST by declaring particular identifiers (**token**) that can be used later in the semantics. The precedence of a token is given by the attribute **prec**(*nb*). Sorts with the attribute **token** are only composed of symbols with the attribute **function** or **token**, and only these sorts can be composed of **token** symbols. Finally, K is able to insert file, line and column meta-data into the parse tree on a subtree of type *s* when parsing, when the sort *s* has the attribute **locations**.

**About printing.** There are also some attributes to change colors of printing in the console (**color**, **colors**), the names (**symbol**, **klabel**, **bracketLabel**) and the printing (**format**) of the symbols and to define a latex name (**latex**). Moreover, K will warn the user if a symbol is declared but not used in any of the rules. The user can disable this warning for a particular symbol or cell by adding the attribute **unused**.

**About symbol.** Compared to an evaluation strategy defined with the attributes **strict** and **seqstrict** (Section 2.1.2.3), it is possible to develop more complex ones thanks to the attributes **result** and **hybrid**. For example, these attributes can allow lists of values to be considered as values.

A symbol can be (1) a constructor, (2) a function, (3) a token, (4) a bracket or (5) a macro ($A_{family}$). Functions can be defined as injective (**injective**) or total (**total**), formerly called **functional**). Moreover, it is possible to request K to generate fresh values and use them with fresh variables !Var (**freshGenerator**) and also to define binder (**binder**).

**About cell.** The user can choose if a cell is optional (**multiplicity="?"**) or can appear several times (**multiplicity="*"**). These attributes allow the user to design a set of cells, which type can be defined by sorts **List**, **Set** or **Map** thanks to the attribute **type**. Moreover, each cell can have a console exit value (**exit**) or can print on the standard stream (**stream**).

**About rewriting.** Theoretically rewriting rules can be applied in any order, but K allows the user to associate a priority to each rule (**priority**(*nb*)**) or to indicate that a rule applies only if no other can apply (**owise**). Moreover, the attribute **anywhere** can be used to prevent K from automatically computing the configuration in a rewriting rule. Finally, it is also possible to allow variables to be unbound in the left-hand side of a rewriting rule thanks to the attribute **unboundVariables** or with unbound variables ?Var.

The semantics of most of these attributes are specified in the rest of this article.

2.2.2 Definable features thanks to the K standard library

The K standard library is composed of eight files. The file *prelude.md* is imported into any K definition and contains only two lines that import the following two files: *domains.md* which defines the types of several usual data structures, for instance, the sorts *Bytes*, *Array*, *Map*, *Set*, *List*, *Bool*, *Int*, *String* or *Float*, and *kast.md* which corresponds to the syntax of K. Moreover, the file *rat.md* is an implementation of the rational integers, the file
`substitution.md` is an implementation allowing substitution (required by the attribute `binder`), and the file `unification.md` is an implementation allowing unification. Finally, the two last files are `ffi.md` which allows C functions to be called and `json.md` which allows JSON files to be read. The three following symbols are also defined: `.: K [constructor]`, `∩: KItem × K → K [constructor]` and `inj: ∀ (From, To : K), From → To`.

## 2.3 A K grammar

To conclude this section, we present the overview of the translation from K semantics which is available in Figure 5 and formalized in the next section. The K grammar that we consider in this article is available in Figure 6. A K file can contain several modules (`module/endmodule`). It is possible to import files into another file (`requires` or `require`) or to import one or more modules into another module (`imports` or `import`). Additionally, an attribute is associated to a module (`A<sub>module</sub>`), a sort (`A<sub>sort</sub>`), a symbol (`A<sub>symbol</sub>`), a cell (`A<sub>cell</sub>`), a rewriting rule (`A<sub>rule</sub>`), a context (`A<sub>context</sub>`) or a context alias (`A<sub>context-alias</sub>`). Moreover, a configuration variable begins with `$` such as `$PGM`, a fresh variable begins with `!` and an unbound variable in a rewriting rule begins with `?`. Finally, there are three cast operators noted `:` (`::` and `:`).

The K grammar in Figure 6 is almost complete. In order not to make it too heavy, we have omitted a part of the syntax allowing to declare precedence and associativity of symbols since this is only useful for the generation of the K parser extended with the user-defined language $\mathcal{L}$ (Figure 5).

In addition, we consider that the declarations with at least one of the attributes related to symbolic execution ($A_{KPROVER}$) have been deleted as well as the syntactic sugar has been simplified. For example,

`syntax BExp ::= MyBool | BExp "&&" BExp` is syntactic sugar for

`syntax BExp ::= MyBool`

`syntax BExp ::= BExp "&&" BExp`. We do not take into account either the syntax ... or the fact that the rewriting arrow `=>` can be nested following Li and Gunter [15] who explain that this syntax is ambiguous syntactic sugar. We assume that the syntactic sugar is simplified by the black box “Desugar” (Figure 5).

In this article, we only consider a K semantics if K accepts it as well as the K grammar (Figure 6) – after deleting a part of the syntax and the syntactic sugar.

<figure><img src="image_14.png" /><figcaption>Figure 5 Overview of the translation from K semantics.</figcaption></figure>

We just explained the two first black boxes in Figure 5. Other boxes are explained (black one) or formalized (white one) in the next section.
12:8 A Semantics of K into Dedukti

<figure><img src="image_15.png" /><figcaption>Figure 6 The considered K grammar, where X is any element of X.</figcaption></figure>
# 3 Abstracting the K framework

This section presents a mathematical structure $\mathcal{M}$ which abstracts the syntax of $\mathbb{K}$. After the presentation of the structure $\mathcal{M}$ as well as the translation of the $\mathbb{K}$ syntax into the structure $\mathcal{M}$, we present various transformations of the structure $\mathcal{M}$ that correspond to the static semantics of $\mathbb{K}$. To present this work, we start with the output of the black box “Add the dependencies” (Figure 5) that recursively replaces each `require` command with the contents of these files, and then recursively replaces each `import` command with the contents of the module that must be imported. We consider that the output of the black box is a single module whose name corresponds to the name of the main initial semantics file. At this stage, the following attributes have finished influencing the transformation: `hook`, $\mathcal{A}_{visibility}$, $\mathcal{A}_{backend}$, `not-lr1`, $\mathcal{A}_{parsing}$, `token`, $\mathcal{A}_{token}$, `locations`, $\mathcal{A}_{printing}$ and $\mathcal{A}_{KPROVER}$.

## 3.1 An abstract view of K

To abstract a $\mathbb{K}$ file, we use the 7-uplet $\mathcal{M} \triangleq (\mathit{Sort}, \mathit{Rel}, \mathit{Sym}, \mathit{Config}, \mathcal{R}, \mathit{Context}, \mathit{Context}_{alias})$, where $\mathit{Sort}$ is the set of sorts, $\mathit{Rel}$ is the set of subtyping relations, $\mathit{Sym}$ is the set of symbols, $\mathit{Config}$ is the set of configurations, $\mathcal{R}$ is the set of rewriting rules, $\mathit{Context}$ is the set of contexts and $\mathit{Context}_{alias}$ is the set of context aliases. Figure 7 shows the translation $||$.|| of $\mathbb{K}$ syntax to the abstract structure $\mathcal{M}$. Syntactic declarations can create sorts, subtyping relations between two sorts, or symbols. As $\mathbb{K}$ allows mixfix notations, we translate them into prefix notations such as $|| \mathit{syntax} \ Exp ::= "if" \mathit{Bool} \ "then" \ Exp "else" \ Exp || = || \mathit{syntax} \ Exp ::= if-then-else(\mathit{Bool}, \ Exp, \ Exp) ||$. Moreover, a configuration declaration generates a list of trees $l$. Section 3.2 shows that $l$ is transformed into a single tree. Finally, any unconditional rewriting rule can be seen as a conditional rule with the condition “true”.

```
|| syntax s      ([ Attr ]) ? || = Sort ← { s }
|| syntax s₁ ::= s₂ ([ Attr ]) ? || = Sort ← { s₁ ; s₂ } ; Rel ← { s₂ < s₁ }
|| syntax { α₁, ..., αₙ } α ::= sym ( s₁, ..., sₓ ) [ Attr ] || with n ≥ 0 and x ≥ 0 =
  Sort ← { α ; s₁ ; ... ; sₓ } \ { α₁, ..., αₙ } ;
  Sym ← { sym : ∀α₁, ..., ∀αₙ, s₁ × ... × sₓ → α [ Attr ] }
|| syntax { α₁, ..., αₙ } α ::= i₁ ... iₓ [ Attr ] || with n ≥ 0 and x ≥ 1 =
  || syntax { α₁, ..., αₙ } α ::= t₁...-tₙ ( s₁, ..., sₓ ) [ Attr ] ||
    where tᵢ ∈ Iₜerminal   ≜ { iₖ | k ∈ ⌊1; x⌋ and iₖ ∈ ⟨ terminal ⟩ }
    sᵢ ∈ Iₙon-terminal ≜ { iₖ | k ∈ ⌊1; x⌋ and iₖ ∈ ⟨ non-terminal ⟩ }
|| syntax s ::= r ⟨ str-of-reg-expr ⟩ [ Attr ] || = Sort ← { s }
|| syntax s₁ ::= List { s₂, sep } || = Sort ← { s₁ ; s₂ }
|| syntax s₁ ::= NeList { s₂, sep } || = Sort ← { s₁ ; s₂ }

|| configuration cell₁ ... cellₙ || with n ≥ 1 = Config ← { (|| cell₁ ||_rec ; ... ; || cellₙ ||_rec ) }
|| < C > v : s < / C > ||_rec = [C]s(v) (If s is not given, we can infer it from v.)
|| < C > cell₁ ... cellₙ < / C > ||_rec = <C>(|| cell₁ ||_rec, ..., || cellₙ ||_rec )

|| rule LHS => RHS [ Attr ] || = R ← { (LHS true ↪ → RHS [Attr]) }
|| rule LHS => RHS requires Cond [ Attr ] || = R ← { (LHS Cond ↪ → RHS [Attr]) }

|| context C ([ Attr ]) ? || = Context ← { (C, true, Attr) }
|| context C requires Cond ([ Attr ]) ? || = Context ← { (C, Cond, Attr) }
|| context alias [ label ] : CA ([ Attr ]) ? || = Context alias ← { (label, CA, Attr) }
```

<caption>Figure 7 From $\mathbb{K}$ to an abstract 7-uplet, where $X \leftarrow data$ is the set $X$ extended with data.</caption>

The following subsection explains the internal transformations made by $\mathbb{K}$ from the obtained mathematical structure $\mathcal{M}$.
## 3.2 Compilation of a K semantics

This subsection formalizes the transformations on the previous mathematical structure $\mathcal{M}$ that correspond to the static semantics of $\mathcal{K}$. After these transformations, the 7-uplet $\mathcal{M}$ will become a quadruplet. As we abstract the content of the $\mathcal{K}$ standard library by the sets $\mathcal{S}ort_{lib}, \mathcal{R}el_{lib}, \mathcal{Sym}_{lib}$ and $\mathcal{R}_{lib}$, we initially assume that $\mathcal{S}ort = \mathcal{S}ort_{lib}, \mathcal{R}el = \mathcal{R}el_{lib}, \mathcal{Sym} = \mathcal{Sym}_{lib}$ and $\mathcal{R} = \mathcal{R}_{lib}$ whereas $\mathcal{Config}, \mathcal{Context}$ and $\mathcal{Context}_{alias}$ are empty. The goal of the first transformation (Figure 8) is to check the validity of a $\mathcal{K}$ semantics.

Each symbol should be a constructor, a function, a token, a bracket or a macro. If this is not the case, it means that the symbol is implicitly a constructor. We therefore explicitly add the attribute constructor, which defines the new set $Sym'$ (Figure 8). Regarding the attribute macro, the documentation is not precise enough. According to Li and Gunter [14], macros are subject to many errors when writing semantics, but in practice macros are always considered as syntactic sugar. The associated rewriting rules are used only once at the beginning of an evaluation of the input programs, to rewrite the syntactic sugar into another term. Macros can therefore be replaced by functions as they are not more expressive.

Moreover, a semantics must have only one configuration, and some attributes have precise restrictions such as the attributes strict and seqstrict are incompatible with function, while a bracket symbol of a given sort has only one argument of that sort.

<figure><img src="image_16.png" /><figcaption>Figure 8 Formalization of the function $||.||_{check-input}$.</figcaption></figure>

**Generate evaluation strategy rules thanks to contexts and context aliases.** We have seen that to define evaluation strategies in $\mathcal{K}$, we can define context aliases, contexts or use the attributes strict and seqstrict. We assume the existence of a function $||.||_{delete-context-alias}$ that transforms a context alias into contexts as well as a function $||.||_{delete-context}$ that transforms a context into rewriting rules. The lack of information in the documentation prevents us from formalizing these two functions.

**Generate evaluation strategy rules thanks to attributes.** We formalize the rule generation from the attributes strict and seqstrict (when the attributes result and hybrid are not also used) in Figure 9, where $nbArg(sym)$ is the number of argument(s) of the symbol sym and n is implicitly used to denote the arity of a symbol. For example, rules 1. and 2. (Figure 3) illustrate the translation formalized in Figure 9.
$\| (\mathit{Sort}, \mathit{Rel}, \mathit{Sym}, \mathit{Config}, \mathcal{R}) \|_{\mathit{generate-strategy}} = (\mathit{Sort}, \mathit{Rel}, \mathit{Sym}'), \mathit{Config}, \mathcal{R}')$

where

$$
\begin{align*}
S_{\mathit{strict}} &\triangleq \{ s \in \mathit{Sym} \mid \mathit{strict} \in \mathit{Attr}(s) \} \\
S_{\mathit{seqstrict}} &\triangleq \{ s \in \mathit{Sym} \mid \mathit{seqstrict} \in \mathit{Attr}(s) \} \\
\mathit{Freezer} &\triangleq \left\{
  \begin{array}{@{}l@{}}
    \ast_{\mathit{sym}}^{n_j} : \underbrace{\mathcal{K} \times \dots \times \mathcal{K}}_{\text{nbArg}(\mathit{sym})-1} \to \mathit{KItem} [\mathit{constructor}] \\
    \phantom{\ast_{\mathit{sym}}^{n_j} : \underbrace{\mathcal{K} \times \dots \times \mathcal{K}}_{\text{nbArg}(\mathit{sym})-1}} \text{ and } \mathit{strict} (n_1, \dots, n_k) \in \mathit{Attr}(\mathit{sym}) \\
    \phantom{\ast_{\mathit{sym}}^{n_j} : \underbrace{\mathcal{K} \times \dots \times \mathcal{K}}_{\text{nbArg}(\mathit{sym})-1}} \text{ or } \mathit{seqstrict} (n_1, \dots, n_k) \in \mathit{Attr}(\mathit{sym})
  \end{array}
\right\}
\end{align*}
$$

$$
S^{\prime} \triangleq \mathrm{Sym} \cup \mathrm{Freezer}
$$

$$
\mathcal{R}' \triangleq \mathcal{R} \cup \mathcal{R}_{\text{strict}} \cup \mathcal{R}_{\text{seqstrict}}
$$

Constraint:

Every argument of the attribute `strict` or `seqstrict` should be in `[1;arity(sym)]`.

$\mathcal{R}_{\mathit{strict}}$ is composed of the following rewriting rules:

For all $sym \in S_{\mathit{strict}}$ such that $\mathit{strict} (n_1, \dots, n_j) \in \mathit{Attr}(sym)$, for all $k \in \{ n_1, \dots, n_j \}$:

$sym E_1 \dots E_n \stackrel{c}{\rightleftharpoons} E_k \stackrel{c}{\rightleftharpoons} (\ast_{sym}^k E_1 \dots E_{k-1} E_{k+1} \dots E_n) [\mathit{heat}]$, where $c \triangleq \neg (\mathit{isKResult} E_k)$

$E_k \stackrel{c}{\rightleftharpoons} (\ast_{sym}^k E_1 \dots E_{k-1} E_{k+1} \dots E_n) \stackrel{c}{\rightleftharpoons} sym E_1 \dots E_n [\mathit{cool}]$, where $c \triangleq \mathit{isKResult} E_k$

$\mathcal{R}_{\mathit{seqstrict}}$ is composed of the following rewriting rules:

For all $sym \in S_{\mathit{seqstrict}}$ such that $\mathit{seqstrict} (n_1, \dots, n_j) \in \mathit{Attr}(sym)$, for all $k \in \{ n_1, \dots, n_j \}$:

$sym E_1 \dots E_n \stackrel{c}{\rightleftharpoons} E_k \stackrel{c}{\rightleftharpoons} (\ast_{sym}^k E_1 \dots E_{k-1} E_{k+1} \dots E_n) [\mathit{heat}]$

where $c \triangleq \mathit{isKResult} E_1 \land \dots \land \mathit{isKResult} E_{k-1} \land \neg (\mathit{isKResult} E_k)$

$E_k \stackrel{c}{\rightleftharpoons} (\ast_{sym}^k E_1 \dots E_{k-1} E_{k+1} \dots E_n) \stackrel{c}{\rightleftharpoons} sym E_1 \dots E_n [\mathit{cool}]$, where $c \triangleq \mathit{isKResult} E_k$

■ Figure 9 Formalization of the function $\| \cdot \|_{\mathit{generate-strategy}}$.

**Encapsulate the configuration.** According to the grammar in Figure 6, a configuration is a list of finite branching trees. However $\mathcal{K}$ encapsulates any configuration $[cell_1;\dots; cell_n]$ as follows: $<\mathit{GT}>(<\mathit{T}>}(cell_1,\dots, cell_n), [\mathcal{GC}]_{\mathit{Int}}(0))$, where $\mathit{GT} \triangleq \mathit{GeneratedTop}$ and $\mathcal{GC} \triangleq \mathit{GeneratedCounter}$. For instance, the initial configuration from Figure 2 becomes
$$ \langle \langle \langle \mathit{PGM} : \mathbf{BExp} \rangle_k \rangle_T \langle 0 \rangle_{\mathit{GC}} \rangle_{\mathit{GT}}. $$

Thus, after this transformation, any configuration becomes a single finite branching tree.

**Generate implicit cells.** Now that we have generated the full configuration, we formalize the completion of the rewriting rules in Figure 10. For instance, the result of mgconf *Config* is $\langle \langle \langle pgm \rangle_k \rangle_T \langle c \rangle_{GC} \rangle_{GT}$, where *Config* is the initial configuration of Figure 2, *pgm* and *c* are fresh variables. Moreover, rule 4. from Figure 3 becomes:

rule $\langle \langle \text{false } \& \& \_ \wedge S \rangle_k \rangle_T \langle c \rangle_{GC} \rangle_{GT} \Rightarrow \langle \langle \text{false } \wedge S \rangle_k \rangle_T \langle c \rangle_{GC} \rangle_{GT}$.

$\| (\mathit{Sort}, \mathit{Rel}, \mathit{Sym}, \mathit{Config}, \mathcal{R}) \|_{\mathit{add-cell}} = (\mathit{Sort}, \mathit{Rel}, \mathit{Sym}, \mathit{Config}, \mathcal{R}')$

where

$$
\mathcal{R}' \triangleq \{ \| l \stackrel{c}{\rightleftharpoons} r [\mathit{Attr}] \|_x \mid l \stackrel{c}{\rightleftharpoons} r [\mathit{Attr}] \in \mathcal{R} \text{ and } x \triangleq \mathit{mgconf} \ \mathit{Config} \}
$$

with mgconf (<C>(Cell<sub>1</sub>, ..., Cell<sub>n</sub>)) $\triangleq$ <C>(mgconf Cell<sub>1</sub>, ..., mgconf Cell<sub>n</sub>)

mgconf ([C]<sub>s</sub>(v)) $\triangleq$ [C]<sub>s</sub>(f), where f is a fresh variable

with $\| l \stackrel{c}{\rightleftharpoons} r [\mathit{Attr}] \|_x \triangleq l \stackrel{c}{\rightleftharpoons} r [\mathit{Attr}]$, if the head symbol of *l* is a function symbol

$l \stackrel{c}{\rightleftharpoons} r [\mathit{Attr}]$, if anywhere $\in \mathit{Attr}$

$\bar{l}^x \stackrel{c}{\rightleftharpoons} \bar{r}^{-x} [\mathit{Attr}]$, otherwise

with $\bar{p}^x \triangleq x [ \overrightarrow{[C]_s(y)} \setminus \overrightarrow{[C]_s(v)} ]$ where $\overrightarrow{[C]_s(v)}$ are the leaves appearing in *p*

■ Figure 10 Formalization of the function $\| \cdot \|_{\mathit{add-cell}}$.

**Split the configuration.** Now we are ready to decompose the configuration into sorts and symbols. The generated rewriting rules are useful to complete the initial configuration with the value given by the user thanks to the configuration variable. The formalization is available in Figure 11, where $\mathit{GT} \triangleq \mathit{GeneratedTop}$ and $\mathcal{GC} \triangleq \mathit{GeneratedCounter}$.
12:12 A Semantics of K into Dedukti

$$
\| (\mathcal{S}, \mathcal{R}, \mathcal{S}, \mathcal{C}, \mathcal{F}) \|_{\text{split-config}} = (\mathcal{S}', \mathcal{R}', \mathcal{S}', \mathcal{R}')
$$

where

$$
\mathcal{S}' \triangleq \mathcal{S} \cup \{ \mathcal{S} \mid \langle C \rangle(c_1, \dots, c_n) \in \mathcal{C} \}
$$

$$
\mathcal{S}_{\text{cell}} \triangleq \{ C : \text{Type} ( \langle C \rangle(c_1, \dots, c_n) ) [ \text{constructor} ] | \langle C \rangle(c_1, \dots, c_n) \in \mathcal{C} \}
$$

$$
\mathcal{S}_{\text{init}} \triangleq \{ \text{initC} : \text{SortC} [ \text{function, initializer} ] | \langle C \rangle(c_1, \dots, c_n) \in \mathcal{C} \}
$$

$$
\mathcal{S}_{\text{get}} \triangleq \{ \text{getGC} : \text{SortGT} \to \text{SortGC} [ \text{function} ] \}
$$

$$
\mathcal{S}' \triangleq \mathcal{S} \cup \mathcal{S}_{\text{cell}} \cup \mathcal{S}_{\text{init}} \cup \mathcal{S}_{\text{get}}
$$

$$
\mathcal{R}_{\text{init}} \triangleq \{ \text{initC} \hookrightarrow C((\text{GetInit } c_1), \dots, (\text{GetInit } c_n)) [ \text{ initializer} ] \mid \langle C \rangle(c_1, \dots, c_n) \in \mathcal{C} \}
$$

$$
\mathcal{R}' \triangleq \mathcal{R} \cup \mathcal{R}_{\text{init}} \cup \{ \text{getGC}(\text{GT}(X,V)) \hookrightarrow V \}
$$

$$
\text{with} \quad \text{Type} ( \langle X \rangle(c_1, \dots, c_n) ) \triangleq \text{RetType}(c_1) \times \dots \times \text{RetType}(c_n) \to \text{SortX}
$$

$$
\text{with} \quad \text{RetType} ( \langle X \rangle(c_1, \dots, c_n) ) \triangleq \text{SortX}
$$

$$
\text{RetType} ( [X]_s(v) ) \triangleq s
$$

$$
\text{with} \quad \text{GetInit} ( \langle X \rangle(c_1, \dots, c_n) ) \triangleq \text{initX}
$$

$$
\text{GetInit} ( [X]_s(v) ) \triangleq v
$$

■ Figure 11 Formalization of the function || . || split-config .

For example, the symbol `initK`: `SortK` and the rule `initK` `ñ` `K $PGM` are generated as well as the symbols `GT`: `SortT` `×` `SortGC` `→` `SortGT` and `T`: `SortK` `→` `SortT`.

**Add implicit attributes.** Implicitly, every symbol with the attribute `constructor` also has the attributes `total`, formerly called `functional`, and `injective`, as formalized in Figure 12.

$$
\| (\mathcal{S}, \mathcal{R}, \mathcal{S}, \mathcal{R}) \|_{\text{add-attributes}} = (\mathcal{S}, \mathcal{R}, \mathcal{S}', \mathcal{R}')
$$

where

$$
S_{\text{constructor}} \triangleq \{ s \in \mathcal{S} \mid \text{constructor} \in \text{Attr}(s) \}
$$

$$
S'_{\text{constructor}} \triangleq \left\{
\begin{array}{l}
\{ n : \forall \vec{v}, \vec{t} \to \alpha [ \text{Attr} \cup \{\text{total}, \text{injective}\} ] \\
\qquad \mid n : \forall \vec{v}, \vec{t} \to \alpha [ \text{Attr} ] \in S_{\text{constructor}} \}
\end{array}
\right\}
$$

$$
\mathcal{S}' \triangleq (\mathcal{S} \setminus S_{\text{constructor}}) \cup S'_{\text{constructor}}
$$

■ Figure 12 Formalization of the function || . || add-attributes .

**Manage the fresh values.** When using a K rewriting rule, any occurrence of a fresh variable !X is replaced by the current value presents in the cell GeneratedCounter and the current value of the cell GeneratedCounter is replaced by a new one. For instance, the rewriting rule rule `foo X S k T c GC GT` => `foo X S k T c GC GT` becomes `foo X S k T c GC GT` => `c S k T c + GC GT`.

**Add type-related symbols and extend the typing hierarchy.** Implicitly, every user-defined sort is a sub-sort of `KItem`. Moreover, K generates projection symbols and predicate symbols such as `isKResult`, as shown in Figure 13.

$$
\| (\mathcal{S}, \mathcal{R}, \mathcal{S}, \mathcal{R}) \|_{\text{typing}} = (\mathcal{S}, \mathcal{R}', \mathcal{S}', \mathcal{R}')
$$

where

$$
\mathcal{R}' \triangleq \mathcal{R} \cup \{ s < KItem \mid s \in \mathcal{S} \setminus \{ K ; KItem \} \}
$$

$$
\mathcal{F}_{\text{projection}} \triangleq \{ \text{projs} : K \to s [ \text{projection}, \text{function} ] | s \in \mathcal{S} \setminus \{ K \} \}
$$

$$
\mathcal{F}_{\text{predicate}} \triangleq \{ \text{iss} : K \to \text{Bool} [ \text{predicate}, \text{function}, \text{total} ] | s \in \mathcal{S} \}
$$

$$
\mathcal{S}' \triangleq \mathcal{S} \cup \mathcal{F}_{\text{projection}} \cup \mathcal{F}_{\text{predicate}}
$$

$$
\mathcal{R}_{\text{projection}} \triangleq \{ s ( \text{inj}^{\text{KItem}} X ) \hookrightarrow X [ \text{projection} ] \mid s \in \mathcal{F}_{\text{projection}} \text{ if } t \text{ is the output type of } s \}
$$

$$
\mathcal{R}_{\text{predicate}} \triangleq \{ p ( \text{inj}^{\text{KItem}} X ) \hookrightarrow \text{true} [ ] | p \in \mathcal{F}_{\text{predicate}} \text{ if } s \text{ is the output sort of } p \}
$$

$$
\mathcal{R}_{\text{pred-oweise}} \triangleq \{ p X \hookrightarrow \text{false} [ \text{oweise} ] | p \in \mathcal{F}_{\text{predicate}} \}
$$

$$
\mathcal{R}' \triangleq \mathcal{R} \cup \mathcal{R}_{\text{projection}} \cup \mathcal{R}_{\text{predicate}} \cup \mathcal{R}_{\text{pred-oweise}}
$$

■ Figure 13 Formalization of the function || . || typing .
12:14 A Semantics of K into Dedukti

<figure><img src="image_17.png" /><figcaption>Figure 15 The printer to KORE.</figcaption></figure>

THEORY. This translation has been implemented in a tool written in OCAML, named KAMELO, which is presented in the next section.

4.1 The λΠ-calculus modulo theory

The λΠ-CALCULUS MODULO THEORY, λΠ≡ₜ in short, is a logical framework, i.e. allowing to define theories, introduced by Cousineau and Dowek [10]. λΠ≡ₜ is an extension of the λ-calculus with dependent types and a primitive notion of computation defined thanks to rewriting rules [11]. The syntax as well as the typing rules that define the λΠ≡ₜ are available in Figure 16, where the typing judgment Γ ⊢ t : A means that the term t has type A with respect to the context Γ. The specific typing judgment Γ ⊢ A : Type indicates that A is a type under the context Γ. We also consider a signature Σ, and a set of higher-order rewriting rules R. In this framework, for any rewriting rule l ↪ → r ∈ R, FV(r) ⊆ FV(l) holds (where FV(p) is the set of free variables of p). The use of such a rewriting rule requires that for any substitution σ, the instantiation of its left-hand side lσ and the instantiation of its right-hand side rσ are well-typed with the same type (Γ ⊢ lσ : A and Γ ⊢ rσ : A for a certain type A).

<figure><img src="image_18.png" /><figcaption>Figure 16 Syntax and typing of λΠ≡ₜ with a signature Σ and a rewriting system R.</figcaption></figure>
Note that in the conversion rule (conv), the equivalence relation depends not only on $\beta$-reduction but also on the rewriting system $\mathcal{R}$. Moreover, in order to have the decidability of the type-checking, the condition $A \equiv_{\beta\mathcal{R}} B$ of the rule (conv) must be decidable, which is ensured when the considered rewriting systems are convergent. Finally, contexts can contain ill-formed elements and the order of the elements does not matter. Indeed, thanks to the rule (var), only well-formed elements in the context can be used when doing a proof. This presentation has been proved equivalent to the usual presentations by Dowek [12].

## 4.2 Dedukti

DEDUKTI [4, 5] is a logical framework based on the $\lambda\Pi \equiv_T$. Indeed, expressing the Calculus of Constructions in DEDUKTI is equivalent to defining it as a theory of the $\lambda\Pi \equiv_T$. Several logics have been encoded in DEDUKTI, facilitating the interoperability of proofs between various formal tools [9, 22]. In this section, we only present the features available in DEDUKTI needed in this article.

**Typing and symbols.** The syntax of the $\lambda\Pi \equiv_T$ is directly accessible in DEDUKTI: TYPE (Kind is not accessible to the user but only inferred by the system), $\lambda$ (abstraction), $\Pi$ (dependent product). We write $A \to B$ when the dependent product $\Pi$ ($x: A$), $B$ is not dependent, i.e. when $x \notin FV(B)$.

The signature is defined from symbols. If the declaration of a symbol is made with the keyword `symbol` alone, the symbol is said to be *defined*, without any particular property, whereas with the additional keyword `constant`, the symbol is said to be *constant* and can not be reduced by any rewriting rule.

**Rewriting rules.** A DEDUKTI rule is written `rule LHS $\leftrightarrow$ RHS` in which the free variables are noted `$x$`, `$\$y$`, etc. As in $\mathbb{K}$, it is possible to use a wildcard (`_`) on the left-hand side when a free variable is not used in the right-hand side. DEDUKTI rules allow higher-order, can be non-linear and do not necessarily apply to the head of the term, but are not conditional.

## 4.3 Translation from abstract $\mathbb{K}$ to the $\lambda\Pi$-calculus modulo theory

Section 3 presented an abstract version of $\mathbb{K}$: any $\mathbb{K}$ file can thus be reduced to a set of sorts, subtyping relations, symbols and rewriting rules. Figure 17 presents the translation of these sets into the $\lambda\Pi$-CALCULUS MODULO THEORY.

<figure><img src="image_19.png" /><figcaption>Figure 17 From abstract $\mathbb{K}$ to the $\lambda\Pi \equiv_T$.</figcaption></figure>

Any sort becomes a symbol of type $\mathbb{K}$, except the sort $\mathbb{K}$ itself, which has the type `Type`. Symbols and unconditional rules are unchanged and the set of rewriting rules obtained at the end of the translation $|| \cdot ||_{\lambda\Pi \equiv_T}$ is $\{ l \leftrightarrow r \mid \text{for all } l \leftrightarrow r \in \mathcal{R}_{\text{unconditional}} \} \cup || \mathcal{R}_{\text{conditional}} ||_{\text{CTRS}} \cup || (\text{Rel}, \text{Sym}, \mathcal{R}_{\text{strategy}}) ||_{\text{strategy}}$. The translation function $|| \cdot ||_{\text{CTRS}}$ is explained in Section 4.3.1 and the translation function $|| \cdot ||_{\text{strategy}}$ is explained in Section 4.3.2.
### 4.3.1 Translating conditional rewriting rules

In this section, we are interested in the translation of conditional rewriting rules. As conditional rewriting rules are not primitive in $\lambda\Pi \equiv_T$, it is necessary to find an encoding of a conditional rewriting system (CTRS) into a non-conditional rewriting system (TRS).

#### 4.3.1.1 From a CTRS to a TRS: Examples

We present two examples to illustrate the encoding of a CTRS into a TRS.

**An example without *owise*.** Consider the following system:

(1) $max X Y \stackrel{c}{\rightleftharpoons} Y$, where $c \triangleq X < Y$

(2) $max X Y \stackrel{c}{\rightleftharpoons} X$, where $c \triangleq X \geq Y$.

The resulting encoding is available in Figure 18 as well as an execution.

<table><caption>Figure 18 Rules generated with the variant of Viry's encoding (left) and a computation (right).</caption><tr><td>(0)</td><td>$max X Y \rightleftharpoons bmax X Y b b$</td><td>$max 5 3 \rightleftharpoons_0 bmax 5 3 b b$</td></tr><tr><td>(1')</td><td>$bmax X Y b C \rightleftharpoons bmax X Y (X < Y) C$</td><td>$\rightleftharpoons_1 bmax 5 3 (5 < 3) b$</td></tr><tr><td>(1'')</td><td>$bmax X Y true C \rightleftharpoons Y$</td><td>$\rightleftharpoons^* bmax 5 3 false b$</td></tr><tr><td>(2')</td><td>$bmax X Y C b \rightleftharpoons bmax X Y C (X \geq Y)$</td><td>$\rightleftharpoons_2 bmax 5 3 false (5 \geq 3)$</td></tr><tr><td>(2'')</td><td>$bmax X Y C true \rightleftharpoons X$</td><td>$\rightleftharpoons^* bmax 5 3 false true \rightleftharpoons_{2''} 5$</td></tr></table>

The general idea of the encoding, proposed in this section and initially proposed by Viry [24], is to add as many arguments as there are conditions for a symbol defined with conditional rules. In Figure 18, rule (0) rewrites a term whose head symbol is $max$ into a term using the corresponding extended version of arity 4, $bmax$ here, where all boolean arguments are $b$, indicating that the boolean arguments have not yet been initialised by a condition. Rules (1') and (2') initialize the conditions to be computed whereas rules (1'') and (2'') reduce the size of the term since one of the conditions has been evaluated to true. This encoding has the advantage of not fixing the order of evaluation of the conditions but increases the computation time by doubling the initial number of rules.

Contrary to Viry, we choose to extend the signature, as here with the symbol $bmax$, rather than replacing each symbol of the signature by an equivalent symbol with a greater arity. This choice makes it possible to follow the computations of the conditions and does not force us to translate the obtained normal forms.

**An example with *owise*.** The previous example can also be written more succinctly:

$max X Y \stackrel{c}{\rightleftharpoons} Y$, where $c \triangleq X < Y$

$max X Y \rightleftharpoons X$ [owise]

To encode the attribute *owise*, we have two possibilities: implement an algorithm that determines the complementary condition or consider that all conditions necessarily reduce to either true or false. According to the expressiveness of the conditions that can be written in K (Figure 14), we add the following hypothesis: any boolean function is a total function. Under this assumption, it is not required to compute the complementary condition as we can generate a rule where every boolean argument is false, as shown in Figure 19. This case is formalized in 5.(c) (Figure 20).

Furthermore, K accepts a set of unconditional rules with at least one rule having the attribute *owise*. We exclude this case because we cannot model "If no other rule applies", with a boolean condition. This is equivalent to the use of the attribute *priority*($nb$), with which we do not yet take into account.
<figure><img src="image_20.png" /><figcaption>Figure 19 Rules generated with the variant of Viry's encoding, when the attribute *owise* is used.</figcaption></figure>

### 4.3.1.2 From a CTRS to a TRS: Formalization

We present the translation, noted $||.||_{CTRS}$ previously, as an algorithm in Figure 20. This translation takes as argument a set $\mathfrak{R}$ of conditional rewriting rules $l \stackrel{c}{\hookrightarrow} r$ [Attr]. To avoid naming conflicts, we also assume that $b$ is an unused symbol name and that it does not appear in the head of any symbol name.

According to Figure 10, we need to change the definition of the head symbol of a rule. We note head<sub>k</sub> the function computing the head symbol of the cell <k>, for a given rule, without considering the symbols ., ↙ and inj. Now, we are able to define the function returning the head symbol of a rule:

$$ \text{head}(l \stackrel{c}{\hookrightarrow} r [\text{Attr}]) = \begin{cases} \text{head}_{<k>} (l \stackrel{c}{\hookrightarrow} r) & \text{if the rule is a semantical rule and anywhere} \notin \text{Attr} \\ f & \text{otherwise, where } l \triangleq f a \dots a \text{ (Figure 14)} \end{cases} $$

We also define the set of rules noted $C_\sigma$, in which the rules share the same head symbol $\sigma$, that is $C_\sigma \triangleq \{ l \stackrel{c}{\hookrightarrow} r [\text{Attr}] | \text{head}(l \stackrel{c}{\hookrightarrow} r [\text{Attr}]) = \sigma \}$. We assume that, if there is a rule with the attribute *owise* in $C_\sigma$ for a given $\sigma$, all the other rules in $C_\sigma$ must have a condition.

After calculating each set $C_\sigma$ from $\mathfrak{R}$, we run the algorithm presented in Figure 20, for each $C_\sigma$, where $X$ is the number of conditional rules in $C_\sigma$.

1. If $X = 0$, $C_\sigma$ is unchanged and the algorithm stops. Otherwise, initialize $i$ to 0 and go to 2.

2. Generate the most general left-hand side for a given symbol $\sigma$, noted mglhs$_\sigma$.

3. Generate the extended symbol $b\sigma$ of type $T_1 \rightarrow \dots \rightarrow T_{n-1} \rightarrow b\text{Bool} \rightarrow \dots \rightarrow b\text{Bool} \rightarrow T_n$, with $X$ argument(s) of type $b\text{Bool}$, where $b\text{Bool} = \text{Bool} \cup \{b\}$, and $\sigma$ of type $T_1 \times \dots \times T_{n-1} \rightarrow T_n$.

4. Generate the substitution rule: $mglhs_\sigma \hookrightarrow mglhs_\sigma[\text{update}_{same}(\sigma, b\sigma, b)]_\sigma$

5. For each rule $l \stackrel{c}{\hookrightarrow} r [\text{Attr}] \in C_\sigma$:

a. If $c \neq \text{true}$ and *owise* $\notin$ *Attr*:

- Increment $i$ by 1

- Generate the initialization rule:

$l[\text{update}_{diff}(\sigma, b\sigma, b, i, \_) ]_\sigma \hookrightarrow l[\text{update}_{diff}(\sigma, b\sigma, c, i, \_) ]_\sigma$

- Generate the reduction rule: $l[\text{update}_{diff}(\sigma, b\sigma, \text{true}, i, \_) ]_\sigma \hookrightarrow r$

b. If $c = \text{true}$ and *owise* $\notin$ *Attr*:

- Generate the reduction rule: $l[\text{update}_{same}(\sigma, b\sigma, \_) ]_\sigma \hookrightarrow r$

c. If $c = \text{true}$ and *owise* $\in$ *Attr*:

- Generate the reduction rule: $l[\text{update}_{same}(\sigma, b\sigma, \text{false}) ]_\sigma \hookrightarrow r$

where:

* $t_1[t_2]_\sigma$ means that we substitute $t_2$ for the subterm with the head symbol $\sigma$ in $t_1$.

* $arg_i(t)$ corresponds to the $i$-th argument of $t$ and $arity(t)$ to the number of arguments of $t$.

* $mglhs_\sigma \triangleq (\text{mgconf init-config}) [ [\text{K}]_\kappa(x) \setminus [\text{K}]_\kappa((\text{inj}^{\text{Item}}_{\text{RetType}(\sigma)} \sigma f_1 \dots f_{arity(\sigma)}) \cap L) ]$, where *init-config* is the initial configuration, and $f_i$ and $L$ are fresh variables.

* $\text{update}_{diff}(\sigma, b\sigma, s_1, i, s_2) = b\sigma x_1 \dots x_{arity(\sigma)+X}$ with $x_j = \begin{cases} arg_j(\sigma) & \text{if } 1 \le j \le \text{arity}(\sigma) \\ s_1 & \text{if } j = \text{arity}(\sigma) + i \\ s_2 & \text{otherwise} \end{cases}$

* $\text{update}_{same}(\sigma, b\sigma, s) = b\sigma x_1 \dots x_{arity(\sigma)+X}$ with $x_j = \begin{cases} arg_j(\sigma) & \text{if } 1 \le j \le \text{arity}(\sigma) \\ s & \text{otherwise} \end{cases}$

<caption>Figure 20 Variant of Viry's encoding.</caption>
4.3.2 Translating evaluation strategies

As we saw in Section 3.2, some conditional rewriting rules can be generated during the translation of K to KORE, as is the case for the evaluation strategies defined by the attributes strict and seqstrict. The rewriting rules generated by these attributes require the translation of the K computations, i.e. the symbols . and ∧, the freezers but also the predicate isKResult. However, these conditional rewriting rules are part of a known case where Viry's encoding is not confluent, notably because the order of application of some rewriting rules modifies the result of the condition, which can stop the computation. Figure 21 shows the translation of the rules of Figure 3 with Viry's encoding (on the right) and an example of a valid but stuck execution<fnref n="1" /> (on the left).

<figure><img src="image_21.png" /><figcaption>Figure 21 Rules generated with previous encoding (left) and a stuck execution (right).</figcaption></figure>

Intuitively, these rules are used to ensure that $E_1$ is of a specific sort in order to allow or not its evaluation. The idea of our new encoding is to specialize some terms of the rules, i.e. to refine the pattern-matching in order to ensure the desired type. For example, rule 2. in Figure 3 becomes $\langle (\text{inj}_{\text{Bool}}^{\text{KItem}} E_1) \cap (*_{\&\&}^1 E_2) \cap S \rangle_k \leftrightarrow \langle (\text{inj}_{\text{Bool}}^{\text{BExp}} E_1) \&\& E_2 \cap S \rangle_k$, where we force $E_1$ to have the sort `Bool`. Thus this rule can be used only if the term $E_1$ is a fully computed Boolean expression. Moreover, rule 1. in Figure 3 becomes the single rule $\langle (X_1 \&\& X_2) \&\& E_2 \cap S \rangle_k \leftrightarrow \langle (X_1 \&\& X_2) \cap (*_{\&\&}^1 E_2) \cap S \rangle_k$ because there is only one constructor associated to `BExp` and no `token` symbol. Symbols with the attribute `function` or `macro` are not considered, because they are not allowed in the left-hand side of a rule, as well as symbols with the attribute `bracket`, because these ones disappear during the compilation process of K. The full formalization is available in Figure 22.

<figure><img src="image_22.png" /><figcaption>Figure 22 Specialization of the evaluation strategy rules.</figcaption></figure>

<footnote n="1">¹ It is also possible to obtain `false`.</footnote>
### 4.3.3 Semantics preservation

The soundness of the translation is not formally proved in this article. Informally, our translation seeks to ensure that the program executed in the $K$ framework and the program executed in DEDUKTI have the same behaviour. If the language described is deterministic, $K$ and DEDUKTI compute the same value or give the same final state. If the language is non-deterministic, $K$ allows to obtain all possible final configurations. In DEDUKTI, it is only possible to obtain one final configuration, because the algorithm is deterministic.

As previously, we assume that every condition is reducible into `false` or `true`. We also assume that the $K$ semantics does not use the following attributes: no cell of the configuration has one of the attributes `multiplicity`, `stream`, `type`, `exit`, no evaluation strategy based on `result` or `hybrid`, and no rewriting rule has the attribute `priority()`, `unboundVariables`, `assoc`, `comm`, `unit` or `idem`. Lastly, we assume that, for a given symbol, among the associated evaluation rules, only one rule has the attribute `owise` and in this case, other rules must have a condition.

The two following parts present the soundness and completeness statements, thanks to the function $|.$| which is translated a $K$ term into a DEDUKTI one by induction on Term($K$):

- $| sym x_1 ... x_n | \triangleq sym | x_1 | ... | x_n |$, if $sym \in \Sigma_{DEDUKTI}$,

- $| x | \triangleq x$, where $x$ is a variable

#### 4.3.3.1 Soundness

The next conjecture helps to assert that any derivation in $K$ is also a derivation in DEDUKTI.

- **Conjecture 1.** For any $K$ rewriting step $l \leftrightarrow r$, there is a DK derivation $|l| \leftrightarrow^* |r|$.

- **Corollary (From $K$ to DEDUKTI).** For every derivation $l \leftrightarrow^* r$ in $K$, there is a derivation $|l| \leftrightarrow^* |r|$ in DEDUKTI.

#### 4.3.3.2 Completeness

We note *Flat* the set of every term starting with `b`.

We note *Ghost* the set of every term having at least one symbol in *Flat*.

- **Lemma 1.** $| . | : Term(K) \to Term(DEDUKTI) \setminus Ghost$ is a bijection.

We define the translation function $|| . ||_{K2DK} : Term(K) \to Term(DEDUKTI)$ such that
$$ || t ||_{K2DK} = | t | \text{ and the detranslation function } || . ||_{DK2K} : Term(DEDUKTI) \to Term(K) \text{ such that } || t ||_{DK2K} = \begin{cases} | t |^{-1} & \text{if } t \notin \text{Ghost} \\ || t ||_{forget} & \text{if } t \in \text{Ghost} \end{cases} $$

The function `forget` is defined inductively on Term(DEDUKTI):

- $|| sym x_1 ... x_n ||_{forget} \triangleq sym || x_1 ||_{forget} ... || x_n ||_{forget}$, if $sym \notin Flat$

- $|| b sym x_1 ... x_n ||_{forget} \triangleq sym || x_1 ||_{forget} ... || x_i ||_{forget}$, if $b sym \in Flat$, where $x_{i+1} ... x_n$ are conditions

- $| x ||_{forget} \triangleq x$, where $x$ is a variable

The following conjecture states that any derivation in DEDUKTI is also a derivation in $K$, except if the derivation begins or ends with a term generated by the Viry encoding.

- **Conjecture 2 (From DEDUKTI to K).** For every derivation $l \leftrightarrow^* r$ in DEDUKTI, there is a derivation $|l| ||_{DK2K} \leftrightarrow^* || r ||_{DK2K}$ in $K$ if $l \notin \text{Ghost}$ or $r \notin \text{Ghost}$.

- **Corollary (Preservation of confluence).** If the rewriting system $\mathcal{R}$ written in $K$ is confluent, then the translation of the rewriting system $\mathcal{R}$ in DEDUKTI is confluent.
► **Corollary (Preservation of termination).** If the rewriting system $\mathcal{R}$ written in $\mathcal{K}$ is terminating, then the translation of the rewriting system $\mathcal{R}$ in DEDUKTI is terminating.

# 5 Implementation and examples

This section focuses on the implementation of the translations presented in the previous section, i.e. on the tool KAMELO [1] which allows to translate KORE into DEDUKTI.

## 5.1 KaMeLo in a nutshell

In practice, the formalizations presented in Section 3.2 as well as the printer to KORE (Figure 15) correspond to the command `kompile` implemented by the $\mathcal{K}$ team. Like the command `krun`, also implemented by the $\mathcal{K}$ team, KAMELO allows programs translated into KORE to be executed in DEDUKTI thanks to the $\mathcal{K}$ semantics translated into KORE. KAMELO implements the translation formalized in Figure 20 and Figure 22.

Moreover, it is the responsibility of each backend to implement the $\mathcal{K}$ standard library and to support the appropriate attributes. The backend KAMELO does not support the attributes `multiplicity`, `stream`, `type`, `exit`, `result`, `hybrid`, `priority()`, `unboundVariables`, `assoc`, `comm`, `unit` and `idem`. The implementation of the $\mathcal{K}$ standard library in DEDUKTI is available on https://gitlab.com/semantiko/DK-BiblioteKo.

## 5.2 KaMeLo in action

From a semantics of 84 lines of a simple while-language similar to IMP in [25], it is possible to obtain a KORE file of 4 130 lines (18 sorts, 5 hooked sorts, 102 symbols, 78 hooked symbols and 552 axioms). However, in order to execute a program, the axioms with the attributes `subsort`, `total`, `constructor`, `assoc`, `comm`, `unit` or `idem` do not need to be translated. The translation of this semantics in DEDUKTI has 723 lines (122 symbols and 122 rewriting rules). To execute the following program computing the GCD of $x$ and $y$

```pascal
decl x, y ; x = 20 ; y = 15 ;
while not( (y <= x) and (x <= y) ) do
  { if y < x then x = x - y ; else y = y - x ; }
```

the command `$ krun --depth 0 --output kore GCD.imp` allows to translate the program in KORE. After translating it into DEDUKTI, the result is: `<generatedTop> (<T> (<k> .) (<env> (inj y ↦ inj 5) ; (inj x ↦ inj 5))) (<generatedCounter> 0);`. The source code of KAMELO [1] is joined by some tests as the one presented here.

# 6 Conclusion

This article presents a paper formalization of the translation from $\mathcal{K}$ into KORE and, a paper formalization and an automatic tool, called KAMELO, from KORE to DEDUKTI, in order to execute programs in DEDUKTI. There has already been a translation of a programming language in DEDUKTI [8, 9], but this is the first time a semantical framework has been translated into DEDUKTI.

This work needs to be extended to take into account the attributes `priority()/owise`, `multiplicity/type` and `result/hybrid`. The attributes `assoc`, `comm`, `unit`, `idem` and `unboundVariables` can theoretically not be translated in the general case.
The verification of proof objects generated by the KPROVER as well as the encoding of the theoretical foundations of K into those of DEDUKTI, are not in the scope of this article and will be the subject of future work. The translation presented here is nevertheless necessary to run a program and will be reused for proof checking.

References

1 GitLab of KaMeLo. URL: https://gitlab.com/semantiko/kamelo.

2 Website of K. URL: https://kframework.org/.

3 Website of Sail. URL: https://www.cl.cam.ac.uk/~pes20/sail/.

4 Ali Assaf, Guillaume Burel, Raphal Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system. In *TYPES: Types for Proofs and Programs*, Novi SAd, Serbia, May 2016. URL: https://hal-mines-paristech.archives-ouvertes.fr/hal-01441751.

5 Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some axioms for mathematics. In Naoki Kobayashi, editor, *6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference)*, volume 195 of *LIPIcs*, pages 20:1–20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.FSCD.2021.20.

6 Denis Bogdănaş and Grigore Roşu. K-Java: A Complete Semantics of Java. In *Proceedings of the 42nd Symposium on Principles of Programming Languages (POPL'15)*, pages 445–456. ACM, January 2015. doi:10.1145/2676726.2676982.

7 Patrick Borras, Dominique Clément, Th. Despeyroux, Janet Incerpi, Gilles Kahn, Bernard Lang, and V. Pascual. CENTAUR: The System. In Peter B. Henderson, editor, *Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, Boston, Massachusetts, USA, November 28-30, 1988*, pages 14–24. ACM, 1988. doi:10.1145/64135.65005.

8 Raphaël Cauderlier and Catherine Dubois. ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti. In *ICTAC 2016 - 13th International Colloquium on Theoretical Aspects of Computing*, volume 9965 of LNCS, pages 459–468, Taipei, Taiwan, October 2016. doi:10.1007/978-3-319-46750-4_26.

9 Raphaël Cauderlier and Catherine Dubois. FoCaLiZe and Dedukti to the rescue for proof interoperability. In Mauricio Ayala-Rincón and César A. Muñoz, editors, *ITP 2017: International Conference on Interactive Theorem Proving*, page 532, Brasília, Brazil, September 2017. doi:10.1007/978-3-319-66107-0_9.

10 D. Cousineau and Gilles Dowek. Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. In *TLCA*, 2007.

11 Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In *Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics*, pages 243–320, 1990.

12 Gilles Dowek. Interacting Safely with an Unsafe Environment. CoRR, abs/2107.07662, 2021. arXiv:2107.07662, doi:10.4204/EPTCS.337.3.

13 Chris Hathhorn, Chucky Ellison, and Grigore Roşu. Defining the Undefinedness of C. In *Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15)*, pages 336–345. ACM, June 2015. doi:10.1145/2813885.2737979.

14 Liyi Li and Elsa L. Gunter. IsaK: A Complete Semantics of K. Technical report, University of Illinois at Urbana-Champaign, June 2018. URL: https://hdl.handle.net/2142/100116.

15 Liyi Li and Elsa L. Gunter. IsaK-static: A complete static semantics of K. In *Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings*, pages 196–215. Springer-Verlag Berlin Heidelberg, 2018. doi:10.1007/978-3-030-02146-7_10.
16 Liyi Li and Elsa L. Gunter. A Complete Semantics of K and Its Translation to Isabelle. In Antonio Cerone and Peter Csaba Ölveczky, editors, *Theoretical Aspects of Computing – ICTAC 2021*, pages 152–171, Cham, 2021. Springer International Publishing.

17 Dominic Mulligan, Scott Owens, Kathryn Gray, Tom Ridge, and Peter Sewell. Lem: Reusable Engineering of Real-world Semantics. *ACM SIGPLAN Notices*, 49, August 2014. doi: 10.1145/2628136.2628143.

18 Daejun Park, Andrei Ştefănescu, and Grigore Roşu. KJS: A Complete Formal Semantics of JavaScript. In *Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’15)*, pages 346–356. ACM, June 2015. doi: 10.1145/2737924.2737991.

19 Grigore Roşu and Traian Florin Şerbănută. An overview of the K semantic framework. *The Journal of Logic and Algebraic Programming*, 79(6):397–434, August 2010. doi:10.1016/j.jlap.2010.03.012.

20 Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. Ott: Effective tool support for the working semanticist. *Journal of Functional Programming*, 20(1):71–122, 2010. doi:10.1017/S0956796809990293.

21 Andrei Stefănescu, Daejun Park, Shijiao Yuwen, Yilong Li, and Grigore Roşu. Semantics-based program verifiers for all languages. In *Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications*, pages 74–91, Amsterdam Netherlands, October 2016. ACM. doi:10.1145/2983990.2984027.

22 François Thiré. Sharing a library between proof assistants: Reaching out to the HOL family. *Electronic Proceedings in Theoretical Computer Science*, 274:57–71, July 2018. doi: 10.4204/eptcs.274.5.

23 M. G. J. van den Brand, A. van Deursen, J. Heering, H. A. de Jong, M. de Jonge, T. Kuipers, P. Klint, L. Moonen, P. A. Olivier, J. Scheerder, J. J. Vinju, E. Visser, and J. Visser. The Asf+Sdf Meta-environment: A Component-Based Language Development Environment. In Reinhard Wilhelm, editor, *Compiler Construction*, pages 365–370, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. doi:10.1007/3-540-45306-7_26.

24 Patrick Viry. Elimination of Conditions. *Journal of Symbolic Computation*, 28(3):381–401, 1999. doi:10.1006/jsco.1999.0288.

25 Glynn Winskel. *The formal semantics of programming languages - an introduction*. Foundation of computing series. MIT Press, 1993.

26 A.K. Wright and M. Felleisen. A syntactic approach to type soundness. *Inf. Comput.*, 115(1):38–94, November 1994. doi:10.1006/inco.1994.1093.