# One Down, 699 to Go: or, synthesising compositional desugarings

Sándor Bartha  The University of EdinburghInformatics Forum, 10 Crichton
StreetEdinburghUK<EMAIL_ADDRESS>,  James Cheney  The University of
EdinburghInformatics Forum, 10 Crichton StreetEdinburghUK The Alan Turing
Institute96 Euston RdLondonUK<EMAIL_ADDRESS>and  Vaishak Belle  The
University of EdinburghInformatics Forum, 10 Crichton StreetEdinburghUK The
Alan Turing Institute96 Euston RdLondonUK<EMAIL_ADDRESS>
###### Abstract.

Programming or scripting languages used in real-world systems are seldom
designed with a formal semantics in mind from the outset. Therefore,
developing well-founded analysis tools for these systems requires reverse-
engineering a formal semantics as a first step. This can take months or years
of effort.

Can we (at least partially) automate this process? Though desirable,
automatically reverse-engineering semantics rules from an implementation is
very challenging, as found by Krishnamurthi et al. (2019). In this paper, we
highlight that scaling methods with the size of the language is very difficult
due to state space explosion, so we propose to learn semantics incrementally.
We give a formalisation of Krishnamurthi et al.’s desugaring learning
framework in order to clarify the assumptions necessary for an incremental
learning algorithm to be feasible.

We show that this reformulation allows us to extend the search space and
express rules that Krishnamurthi et al. described as challenging, while still
retaining feasibility. We evaluate enumerative synthesis as a baseline
algorithm, and demonstrate that, with our reformulation of the problem, it is
possible to learn correct desugaring rules for the example source and core
languages proposed by Krishnamurthi et al., in most cases identical to the
intended rules. In addition, with user guidance, our system was able to
synthesize rules for desugaring list comprehensions and try/catch/finally
constructs.

Programming language semantics, testing, enumerative synthesis

††copyright: rightsretained††journal: PACMPL††journalyear:
2021††journalvolume: 5††journalnumber: OOPSLA††publicationmonth: 10††doi:
10.1145/3485499††ccs: Software and its engineering Semantics

##  1\. Introduction

Formal semantics is useful for the maintenance and analysis of programming
languages, and similarly for libraries and frameworks, whose semantics might
best be defined via an abstract language. But few languages are designed with
formal semantics from the start, and writing formal semantics based on an
already existing implementation involves guessing possible semantics rules and
painstakingly writing and evaluating many different test cases.

There are many arguments in favour of reverse engineering a formal
specification. Ambiguities are inevitable if the specification is only written
in natural language. Various implementations may interpret the requirements
differently, making it difficult to port the programs between them. Future
enhancements may break properties that the creators are unaware of but that
the users rely on, thus making programs unnecessarily difficult to maintain.
Security risks may go unnoticed, impacting every system built with the
language (Amin and Tate, 2016). A formal semantics is prerequisite to applying
formal methods or static analysis. Moreover, the ability to reconstruct the
semantics of an opaque system would make it possible to compare properties of
the induced semantics with the intended design, aiding the rationalisation or
redesign of the language.

The usage of formal semantics is standard in the hardware industry (Kern and
Greenstreet, 1999), and there is a lot of research effort to formalise aspects
of mainstream languages (Jung et al., 2017; Nienhuis et al., 2016). But its
impact on the wider software industry is modest: the vast majority of systems
in usage today do not have formal semantics. These systems rely on many
idiosyncratic solutions to represent computations, in the form of domain
specific languages, configuration languages, or query languages, and an even
larger number of libraries and frameworks, that frequently change their
behaviour from version to version. To get a sense of the scale of the work
involved in writing the full formal semantics of one language, see some recent
examples for popular programming languages, such as JavaScript (Maffeis et
al., 2008; Guha et al., 2010), R (Morandat et al., 2012), Python (Politz et
al., 2013), and PHP (Filaretti and Maffeis, 2014). Each of these formal
semantics are the result of months of work by research groups.

Let us step into the shoes of the semantics engineer, whose task is to reverse
engineer an interpretable semantics of an actual programming language, by
observing the behaviour of its opaque or non-intelligible interpreter.
Languages are usually riddled with many varieties of similar constructs, and
the tedious parts of producing formal specifications involve writing a lot of
small example programs, then testing their behaviour with the opaque
implementation. Krishnamurthi et al., the authors of ”The Next 700 Semantics:
A Research Challenge” ((2019)) argue for the need of semi-automation. A full
solution to this challenge would facilitate defining the formal semantics for
700 languages, alluding to how Peter Landin’s landmark paper ”The Next 700
Programming Languages” ((1966)), written more than 50 years ago, had
facilitated their creation in the first place.

As a first step towards achieving partial automation, Krishnamurthi et al.
(from now on, abbreviated kle) suggest that semantics be divided into a
complex part provided by human semantic engineers, and a tedious but shallow
part hopefully synthesised automatically. They formulate this division in the
following way: first let human engineers specify a core version of the
language, capturing the essential features, reducing the potentially hundreds
of language constructs to a few. They also provide a definitional interpreter
(e.g. a direct implementation of an operational semantics) for this core
language, which is much smaller. Our task then is reduced to finding
translation rules from the original (source) language to this core language,
based on observation of the behaviour of source programs. Note that we only
work with term languages consisting of abstract syntax trees: while reverse-
engineering a formal grammar for a language from its examples is also an
interesting problem, we are focusing only on the semantics of the resulting
term language. Our task is to find a program that translates, or _desugars_ ,
source terms into core terms.

For a familiar example, let the source language be a simple functional
language with arithmetic. We give its semantics by first providing the
semantics of the $\lambda$-calculus extended with the primitive types
(numbers) and operations (arithmetic) of the language, then translating
additional language constructs into this core language. Figure 1 shows some
potential test cases run on the opaque interpreter of the source language, and
Figure 1 shows an example translation rule that we should generate based on
these test cases. The rule expresses a let expression (in the source language)
in terms of a $\lambda$ expression and application (which is part of the
reduced core language). This example shows the semantics of one language
construct for the sake of demonstration, but in the general case the source
language may contain hundreds of constructs that need to be reduced to the
core language: this reduction of the number of term constructors is the main
point of the translation.

let x=1 in x+x $\leadsto$ 2

let x=2 in 1 $\leadsto$ 1

(a) Partial input: test cases for let expression

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{let}\,i=e_{1}\,\texttt{in}\,e_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}=\Big{(}\mbox{\Large$\lambda$}i\,.\,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}e_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}\Big{)}\,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}e_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}$

(b) Partial output: translation rule for let expression

Figure 1. Learning translation example

kle also suggest a natural search space: compositional _desugaring_
translations. They aim to synthesise a rule (or rules) for each source
language term constructor. Their formulation is insightful and practical. But
the specified task is still hard. They presented four unsuccessful solution
attempts, describing their shortcomings and challenging the research community
to overcome them.

From their astute analysis we identify two inherent properties that make this
problem so challenging: the non-standard learning framework and the
intractability of the program space. The non-standard learning framework makes
many search strategies hard to apply. Three out of the four attempts changed
the requirements in ways the usefulness of which is questionable for an
envisaged solution. Due to the astronomical search space all attempts failed
to reproduce the intended semantics of their example source and core languages
(which are still far behind the size of real world languages). kle studied a
reduced search space, tree transducers. They demonstrated however with their
example source and core languages that many common intended translation rules
in this domain cannot be expressed by tree transducers at all.

We directly build on kle’s work, but we take a slightly different position. We
work on the principle that, before considering search strategies, the
essential first step is to clearly formulate the problem to understand when a
solution is even possible in principle, and then divide the task into feasible
pieces. The main idea behind our paper is that the compositional translations
can be learned by structuring the learning process itself compositionally (or,
more precisely, incrementally). We hypothesise that we can learn the
translation rules of a few term constructors at a time, in each step relying
on the semantics of already established term constructors — following human
practice. This reformulation follows our intuition based on experience with
semantics engineering and has the potential to help with both challenging
aspects. First, it significantly reduces the search space for each synthesis
sub-task, since we only synthesise a small portion of the language’s
translation at a time. Second, by assuming that some part of the translation
is already known, we ease testing potential translations, since we can rely on
the already established parts of the translation.

We argue that this partitioning into feasible sub-tasks is often possible.
This paper makes the following contributions, leading to the first practical
solution to kle’s challenge:

  * •

We recapitulate kle’s challenge, offer further analysis of the obstacles to
it, and outline our approach to overcoming them. (Section 2)

  * •

We propose a formal framework for synthesizing compositional desugarings,
define a sub-task - the _desugaring extension problem_ : learning the
desugaring only on a portion of the source language (a sublanguage), and
highlight underlying assumptions. (Section 3)

  * •

We propose a way to build search spaces for translation rules represented in a
functional language, aiming to find a sweet spot between the too-restrictive
tree transducers and the intractable search space provided by a general
programming language. We show how to express all example translation rules
identified as challenging by kle, while retaining the ability to (relatively)
efficiently enumerate programs. (Section 4)

  * •

We test our approach by analysing a simple enumerative synthesis algorithm as
a baseline, and evaluating it on case studies. In particular, we show that,
using our modified specification for the task, it is possible to obtain most
intended desugaring rules proposed as a test by kle. We also investigated
synthesizing rules for further extensions such as list comprehensions and
try/catch/finally. (Sections 5 and 6)

At a conceptual level, we analyze the desugaring synthesis problem,
highlighting the importance of choices of hypothesis space; and at a technical
level we provide a specific approach that can synthesize the desugarings
proposed by kle as well as some simple extensions.

##  2\. Overview

###  2.1. The challenge

$\small\begin{array}[]{rcl}b\in\textit{Bool}&::=&\\{\texttt{true},\texttt{false}\\}\qquad
i\in\textit{Id}\qquad n\in\textit{Number}\qquad s\in\textit{String}\\\
o\in\textit{Op}&::=&\\{0-,\texttt{not},+,-,\land,\lor,<,>\\}\\\
t,t_{1},t_{2},t_{3}\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textit{STerm}}&::=&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SFalse}}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SNum}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}n}})}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SVar}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}})}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SStr}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}s}})}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SBetween}(t_{1},t_{2},t_{3})}\\\
&\mid&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SPrim}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}o}},[t,\dots])}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SIf}(t_{1},t_{2},t_{3})}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SLam}([\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},\dots],t)}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SApp}(t_{1},[t_{2},\dots])}\mid\\\
&\mid&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SLet}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t_{1},t_{2})}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SLetRec}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t_{1},t_{2})}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SAssign}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t)}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SList}([t,\dots])}\mid\\\
&\mid&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SListCase}(t_{1},t_{2},t_{3})}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SFor}(t_{1},[f,\dots],t_{2})}\\\
f\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textit{SForBind}}&::=&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SFBind}(i,t)}\\\
e,e_{1},e_{2},e_{3}\in{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}&::=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CBool}(b)}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CNum}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}n}})}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CVar}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}})}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CStr}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}s}})}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CPrim1}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}o}},e)}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CPrim2}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}o}},e_{1},e_{2})}\\\
&\mid&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CIf}(e_{1},e_{2},e_{3})}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLam}([\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},\dots],e)}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CApp}(e_{1},[e_{2},\dots])}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},e_{1},e_{2})}\\\
&\mid&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLetRec}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},e_{1},e_{2})}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CAssign}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},e)}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CList}([e,\dots])}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CListCase}(e_{1},e_{2},e_{3})}\end{array}$
(a) Syntax of Pidgin source (red) and core (blue) languages

$\small\begin{array}[]{rcl}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{STrue}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CBool}(true)}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SFalse}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CBool}(false)}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SNum}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}n}})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CNum}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}n}})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SVar}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CVar}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SStr}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}s}})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CStr}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}s}})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SBetween}(t_{1},t_{2},t_{3})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}(\%i_{1},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},\texttt{CLet}(\%i_{2},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},\texttt{CLet}(\%i_{3},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{3}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},}\\\
&&\quad\quad\quad{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CPrim2}(\land,\texttt{CPrim2}(<,\%i_{1},\%i_{2}),\texttt{CPrim2}(<,\%i_{2},\%i_{3})))))}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SPrim}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}o}},[t_{1}])}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CPrim1}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}o}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SPrim}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}o}},[t_{1},t_{2}])}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CPrim2}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}o}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SIf}(t_{1},t_{2},t_{3})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CIf}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{3}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SLam}([\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},\dots],t)}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLam}([\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},\dots],{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SApp}(t_{1},[t_{2},\dots])}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CApp}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},\dots])}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SLet}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t_{1},t_{2})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SLetRec}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t_{1},t_{2})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLetRec}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SAssign}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t)}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CAssign}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SList}([t,\dots])}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CList}([{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},\dots])}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SListCase}(t_{1},t_{2},t_{3})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CListCase}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{3}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SFor}(t_{1},[\texttt{SFBind}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t_{3}),\dots],t_{2})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CApp}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},[\texttt{CLam}([\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},\dots],{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}),\texttt{CList}([{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{3}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},\dots])])}\end{array}$
(b) Intended translation of the Pidgin source language into the core language

Figure 2. Pidgin source language, core language, and desugaring

kle presented a case study highlighting the challenge of learning desugarings
from examples. For convenience, we give a name to the language they proposed:
Pidgin. Figure 2 recapitulates the syntax of Pidgin’s source and core
languages and quotes their intended translations of Pidgin (red) to Core
Pidgin (blue). We treat the syntax of the languages (as shown by Figure 2)
along with their respective interpreters as the input of the learning process.
The intended output is the set of translation rules that Figure 2 depicts.
Except for minor notational differences, we repeat their definitions verbatim;
some features, such as list ”cons”, are omitted but easy to add.

kle did not give an explicit definition of the semantics of the core language
or of the notation used for the desugaring rules. We assume the core language
to be a standard call-by-value lambda-calculus with arguments evaluated left-
to-right, in which all variables are assignable references. The desugaring
rules used intuitive, but not formally defined, notations for fresh names and
list parameters, which we paraphrase in Figure 2. In the rule for SBetween,
the notations $\%i_{1},\%i_{2},\%i_{3}$ stand for freshly generated
identifiers. In rules such as SLam, SApp, and SList, notations $[t,\ldots]$
and
$[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},\ldots]$
stand for the (possibly empty) lists of sub-terms $t$ and their translations.
Finally, in the rule for SFor, the notation
$[\texttt{SFBind}(i,t_{3}),\ldots]$ stands for a (possibly empty) list of
bindings of identifiers $i$ to expressions $t_{3}$, and on the right-hand side
the notations $[i,\ldots]$ and
$[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{3}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},\ldots]$
stand for the lists of the first and (translated) second components of the
bindings, respectively (that is, the results of unzipping the list considering
the bindings as pairs). We describe reference implementations of the core
language and the desugaring rules in Appendix A.

The Pidgin source and core languages illustrate several potential
complications in the modelling of translations: the presence of primitive
types and operations, unrestricted number of children, and the special role of
names. Handling argument lists may require expressive translation rules that
can re-arrange them (SFor) or can pattern match on the list (SPrim). Fresh
name generation may be needed to control the order of evaluation of arguments
(${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SBetween}})$.
We will use Pidgin both for illustrating and evaluating our method. In more
realistic examples the source language could be much larger than the core
language, since the point of the translation is to reduce the language to a
smaller one.

###  2.2. Problem analysis

kle gave the initial analysis of the problem and of their four solution
attempts. Their first two attempts, based on tree matching and Gibbs sampling,
were inspired by solutions of a similar task in natural language translation.
They highlight the differences between natural language translation and this
problem, then considered program synthesis techniques with their third and
fourth attempts, based on genetic programming and constraint based program
synthesis respectively. We pick up their thread and highlight two challenging
aspects of the problem, the unusual learning framework and the vast search
space, from the point of view of program synthesis.

source program core program source output core output desugarsource
interpretercore interpretercompare Figure 3. Desugaring learning framework
(cf. Krishnamurthi et al. (2019))

Figure 3, quoted from their paper, captures their learning framework at a high
level. The setting is similar to an active inductive synthesis problem (Jha et
al., 2010; Gulwani et al., 2017): we do not have a logical specification, but
we can produce input/output examples from evaluations of programs by the
interpreters. But there is a crucial difference: the function we are trying to
learn is not the one we can directly test. In our problem statement we assumed
the existence of two languages, the source and the core, and respective
interpreters of the languages. We can evaluate source programs with the source
interpreter and core programs with the core interpreter — but we can only
relate them to each other through the very translation we want to learn. This
rules out many general program synthesis methods.

kle’s first two attempts assumed the availability of examples of the
translation (i.e. pairs consisting of a source program and its corresponding
intended translation in the core language), that are unlikely to be much
easier to produce than the rules themselves. Their fourth analysed method used
a constraint based program synthesis framework named SyntRec (Inala et al.,
2017), but simplified the problem by assuming a shared output space for the
two interpreters, allowing the comparison of the outputs directly, without
relying on the translation that we are about to synthesise. This evades using
this translation twice in the problem specification. Moreover, SyntRec also
required a deep embedding of the core interpreter into the framework. This
highlights that there are two slightly different problems at hand, depending
on whether we treat the core interpreter as opaque (similarly to the source)
or instead require that it has an implementation accessible to the synthesis
algorithm. Since we assumed that the user produces formal semantics of the
core language, using it in the learning process sounds reasonable. But the
formal semantics of even a relatively small language is quite large for
program synthesis methods to handle, and expanding this semantics in the
framework results in huge constraints. This could have played a role in the
explosion of the search space of the constraint based method when the
languages have state. A further problem with this approach is that producing
such an embedding for a synthesis method is not trivial for arbitrary formal
semantics in the first place.

The second problem is shared with program synthesis in general: the
astronomical size of the search space. The first two methods kle analysed are
based on a reduced notion of compositional translations: tree transducers.
They highlight with their example source and core languages that many common
intended translation rules in this domain can not be expressed with tree
transducers, like rules that require re-arranging lists of children (SFor), or
fresh name generation in the Core Pidgin expression (SBetween). Their third
and fourth attempts, based on genetic programming and constraint based program
synthesis, evade this restriction. These general program synthesis techniques,
in principle, can express arbitrary computable translation rules. But applying
general program synthesis methods seems even harder: the search space for
arbitrary computable translations is much larger than tree transducers.

All methods failed to scale up to the full Pidgin language (which is still not
the size of a real world language). We argue that this task extends the
already notoriously hard program synthesis problem with a new dimension: the
number of source term constructors, since, for a compositional translation, we
need to synthesise a separate “program” for each such constructor. This
results in a high number of program synthesis problems, some of which are
interdependent while others can be solved independently.

The partial progress reported by kle highlights that the problem is very
difficult. The main point of the translation is to reduce the number of term
constructors, thus we need an approach that scales well along this dimension.
But this could still be very difficult: not only does the search space grow
exponentially by the number of term constructors, but the term constructors’
translation rules may depend on each other, which makes testing translations
hard. To make progress, we therefore make additional assumptions and
reformulate the problem.

###  2.3. Our approach

When we teach students how to program, we typically do not tell them about all
of the language features at once: this would most likely overwhelm or confuse
them. Instead, in the first lecture we start with “hello world” and gradually
introduce related features in small groups. Indeed, Felleisen et al. (2001)
explicitly adopted this approach by providing language “levels”, or self-
contained sublanguages that intentionally exclude complex features for
pedagogical purposes.

We follow kle in their rational reconstruction of the problem, but we
investigate a simplifying assumption. We hypothesise that the compositional
translation can be learned incrementally, only learning the translation rules
of a few term constructors at a time. For this strategy to work, we must
assume that starting from the rules of a few term constructors given initially
we can iteratively find small groups of term constructors (i.e. language
“levels”) whose translation rules can be found by only testing them on the
part of the language where the translation is already established. Our
approach currently requires the user to provide this sequential decomposition
of the language learning problem. This approach yields two immediate
questions. First, whether the sub-task of learning only a few term
constructors is feasible. Second, whether decomposing languages into small,
more easily learnable sublanguages is feasible in the first place.

We seek an answer for the first by investigating a brute force enumerative
synthesis algorithm. The brute-force method of program synthesis, enumerative
program synthesis, is straightforward to apply to quite general sub-tasks, so
the unusual learning framework does not pose a problem. Enumerative synthesis
is not necessarily slow compared to other synthesis methods: it has proven to
be a very efficient technique in domains where the hypothesis space is rich
and complex, but the size of programs is small (see Alur et al. (2013)). This
description fits well our sub-tasks. While our enumerative algorithm is a
simple brute force search, there are many candidate heuristics and pruning
techniques. Enumerative synthesis combined with other methods fared well in
competitions (see Alur et al. (2017) or Reynolds et al. (2019) for recent
competition-winning synthesis algorithms), and may be applied to speed up our
search in the future. A further consideration is that the success of
enumerative synthesis directly depends on the search space. Our task is to
define a search space which is expressive enough that it can express a wide
variety of translation rules, including those kle considered challenging, but
small enough for the resulting learning task to be feasible. Enumerative
synthesis can demonstrate this, and could be used as both a baseline for
comparison and the basis of future improvements.

To investigate the second point, we formalise our assumption, list some
potential problems, and carry out a full test case: we present a solution of
the Pidgin challenge problem, and two simple extensions to it, based on a
(user-given) partitioning of the language. We also assume that the core
interpreter is opaque, as discussed above. Our approach can perhaps best be
characterised as a semi-automatic _desugaring synthesis assistant_ and does
involve some additional user guidance or feedback, discussed in Section 6.5.

##  3\. Formal framework

In this section we formalise the desugaring learning problem of kle and define
the desugaring extension problem. We show how in principle, full desugarings
can be structured as a series of extension learning problems, and investigate
the conditions when such a partitioning strategy can be successful in
principle. While it is not clear how we could prove that partitioning into a
sequence of desugaring extension problems is always possible, in later
sections we present empirical results showing that it is possible for Pidgin.

###  3.1. Syntax

We employ multi-sorted term languages (Meinke and Tucker, 1993) as a standard
model of syntax. The sorts correspond to the syntactic classes in Figure 2,
plus auxiliary sorts for lists and pairs. This representation allows us to
limit translations to sort-preserving ones, which automatically excludes many
ill-formed translation rules from the search. Our definition of the problem
would work with single-sorted languages as well, but our definition of the
search space relies on the sorts, and enumerative synthesis benefits greatly
from restricting the search space. The usage of multi-sorted terms also
highlights that in practice we may not evaluate every term, just those that
belong to the sort of programs.

###### Definition 3.1 (Signature).

A signature $\Sigma$ consists of

  * •

A non-empty finite set of sorts $S_{\Sigma}$, with a designated sort
$\sigma_{p}\in\Sigma$ for programs.

  * •

A finite set of term constructors (function symbols) $\mathcal{F}_{\Sigma}$.

  * •

The signature function $\mathit{sig}:\mathcal{F}\to S^{*}\times S$, where
$S^{*}$ is a (possibly empty) finite sequence of sorts. We will write
$f:\sigma_{1},\dots,\sigma_{n}\to\sigma$ (where $f\in\mathcal{F}$ and
$\sigma_{1},\dots,\sigma_{n},\sigma\in S$) when
$\mathit{sig}(f)=(\sigma_{1},\dots,\sigma_{n};\sigma)$. The number $n$ can be
$0$, in which case we will write $f:\sigma$, and will call $f$ a constant
symbol.

$\Sigma$ and $\Omega$ will stand for signatures
$(S_{\Sigma},\mathcal{F}_{\Sigma},\mathit{sig}_{\Sigma})$ and
$(S_{\Omega},\mathcal{F}_{\Omega},\mathit{sig}_{\Omega})$, respectively.

###### Remark 1.

Note that we do not have term constructors with lists of children, therefore
we need to model lists of children with an additional sort for the list and
additional term constructors nil and cons. We do not have sort polymorphism,
so we need to add a separate sort for each type of list.

For simplicity in our model we did not include an infinite number of
constants. Literals like numbers and strings therefore have their own term
constructors that we left out in the simplified grammar presented in Figure 2.

In our source language the sorts are Id, Number, String, Op, STerm, SForBind,
$\texttt{List}_{\textit{Id}}$,
$\texttt{List}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textit{STerm}}}$
and
$\texttt{List}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textit{SForBind}}}$.
The sorts of the core language are Bool, Id, Number, String, Op, CTerm,
$\texttt{List}_{\textit{Id}}$, and
$\texttt{List}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}}$.
We also consider each list sort to be automatically equipped with suitable
term constructors $\texttt{nil}_{s}:\texttt{List}_{s}$ and
$\texttt{cons}_{s}:s\times\texttt{List}_{s}\to\texttt{List}_{s}$. We consider
that sort SForBind is essentially a pair of an identifier and STerm, which we
may also write as $\textit{Id}\times\textit{STerm}$.

###### Definition 3.2 (Abstract language).

An _abstract language_ (or language for short) over signature $\Sigma$ is the
set of terms defined inductively with the term constructors in the signature.
We write $T_{\Sigma}$ for this set. The _size_ of a term is the number of term
constructors in it. We extend the signature function $\mathit{sig}$ to terms,
we will use the same notation for the extended function, and we will use
$T_{\Sigma}^{\sigma}$ for terms that belong to the sort $\sigma$. We call
$T_{\Sigma}^{\sigma_{p}}$ the set of program terms.

In functional programming, terms of a language can be represented with an
algebraic datatype (defining a separate type for each sort in the signature).
In universal algebra terminology, an abstract language is the free multi-
sorted algebra over the signature $\Sigma$.

###  3.2. Semantics

As explained earlier, we model both the source and core language as black-box
interpreters, which might seem natural to model as mathematical functions from
terms to result values. However, this approach is too simplistic, since there
are several complications that may arise:

  * •

The interpreter may not be deterministic.

  * •

The output space may not be part of the (input) language: it may contain
opaque functions, locations, or other non-observable values.

  * •

The observable behaviour may not be reduced to an input-output pair: there
could be other side effects like I/O operations.

  * •

Similarly, we may get errors because the source language is not defined on all
terms. Some terms may be allowed by the sort system, but still result in some
kind of error. For example, in our source language the grammar permits
nonsensical expressions like
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{{SPrim}}}(<,[])$.

  * •

Some computations may not terminate. We may model the output of diverging
computations with $\bot$, but for Turing-complete languages, the evaluation
function is not computable.

A standard way in semantics and pure functional programming to model these
complications is using _monads_ (Moggi, 1991; Wadler, 1992a). To make sense of
the composition of operations in the learning setting (see Figure 3), we may
assume that the source interpreter, the core interpreter, and the translation
we want to learn all live in the same monad $\mathcal{M}$. We only consider
deterministic languages, and we assume that output values (of a successfully
terminating program) are part of the input language. In the model we assume
that the evaluation function is computable, and terms where evaluation
exhausts resources (which includes time or CPU cycles and memory) evaluate to
a specific error ($\bot$). We assume for simplicity that for a given
interpreter there is a fixed (and sufficiently large) resource bound such that
the interpreter can be modelled as a deterministic, computable function.
Moreover, we assume that side-effects on any state maintained by $\mathcal{M}$
(e.g. variable assignments) are not directly observable; we only observe the
final output value.

What we get through these simplifications is an interpreter that maps terms to
either values (i.e. fully-evaluated terms) or errors. We assume that the set
of errors $E$ is shared between the source and core languages to allow
comparing the outputs. In other words, our computations take place in the
error monad over the category of total computable functions. We give a
simplified definition that suffices for our purposes:

###### Definition 3.3 (Error monad).

Let $E$ be a fixed, finite set of errors that contains $\bot$ and any errors
the interpreter may return (that are not part of the input language), like
syntax_error. We assume that $E$ is disjoint from any set of terms in any
languages, and let $\uplus$ mean the disjoint union of two disjoint sets. Our
interpreters and translations (and translation rules) will be functions of the
form $f:A\to B\uplus E$. We abuse notation by defining a notion of composition
for such functions by propagating the error as follows. Let $f:A\to B\uplus E$
and $g:B\to C\uplus E$. Then

$\forall a\in A,g(f(a))=\begin{cases*}g(b)&if $f(a)=b\in B$\\\ e&if $f(a)=e\in
E$\end{cases*}$

In the terminology of category theory this amounts to saying that these
functions are morphisms of the Kleisli category of the error monad and are
composed as such.

We also silently propagate the error from the left when a function has
multiple arguments. Let $f_{1}:A_{1}\to B_{1}\uplus E$, $f_{2}:A_{2}\to
B_{2}\uplus E$ and $g:B_{1}\times B_{2}\to C\uplus E$. Then

$\forall a_{1}\in A_{1},a_{2}\in
A_{2},g(f_{1}(a_{1}),f_{2}(a_{2}))=\begin{cases*}e_{1}&if
$f_{1}(a_{1})=e_{1}\in E$\\\ e_{2}&if $f_{1}(a_{1})=b_{1}\in B_{1}$ but
$f_{2}(a_{2})=e_{2}\in E$\\\ g(b_{1},b_{2})&if $f_{1}(a_{1})=b_{1}\in B_{1}$
and $f_{2}(a_{2})=b_{2}\in B_{2}$\end{cases*}$

We extend this shorthand to handle an arbitrary number of arguments.

###### Definition 3.4 (Semantics).

An _evaluation function_ (or _interpreter_) of a language $T_{\Sigma}$ is a
function $\phi:T_{\Sigma}^{\sigma^{p}}\to T_{\Sigma}^{\sigma^{p}}\uplus E$
over the terms such that:

  * •

$\forall t\in T_{\Sigma}^{p},\phi(\phi(t))=\phi(t)$, that is, $\phi$ is
idempotent.

The members of the image of $\phi$ in $T_{\Sigma}^{p}$ (that is, the image of
$\phi$ apart from the errors $E$) are called the _values_ of the language,
denoted by $V(T_{\Sigma})$. A value evaluates to itself (cf. Remark 3).

###  3.3. Translations

In general, the sorts of the source and the core language are different, and
indeed, in our example the core language has Booleans but the source does not,
while the source language has a sort for SForBind and the added
$\texttt{List}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textit{SForBind}}}$,
and neither has a corresponding sort in the core language. Our methods to
build a search space require a partial mapping from the source sorts to the
core sorts, that preserves the sort of programs.

We assume for simplicity that the sorts of the source and core languages are
subsets of a common set $S$, and that the sort of programs is common to the
two languages. Another case that we may consider is when the core language has
an expressive type system, and all source language sorts are mapped to some
type in the core language, in other words the source language is embedded into
a typed core language. We also leave this variant of the problem for future
investigations.

Translations take place in the same error monad as interpreters: this lets us
compose them with the interpreters. Translations can naturally return errors.
If evaluating a source term results in a syntax error, then we may not want to
map it into the core language, we may simply want to translate it directly
into the syntax error. For example, our intended translation in Figure 2 does
not give a mapping for a term with constructor SPrim and zero arguments. We
may imagine the source interpreter raising a syntax error in this case, and it
is more natural for the translation to raise the same syntax error directly,
since in the core language there are no corresponding constructs that result
in a syntax error in the core interpreter.

###### Definition 3.5 (Translation).

Let us have a source language $T_{\Sigma}$ and a core language $T_{\Omega}$,
where the signatures share the set of sorts $S$. We will refer to sort-
preserving functions $\delta:T_{\Sigma}\to T_{\Omega}\uplus E$ as
_translations_.

###### Definition 3.6 (Interpretation).

Let $T_{\Sigma}$ be the source and $T_{\Omega}$ the core language, again with
a common set of sorts. Let $f\in\mathcal{F}_{\Sigma}$ be a term constructor
with signature $f:\sigma_{1}\times\dots\times\sigma_{n}\to\sigma$. Then we
will call members of the function space
$T_{\Omega}^{\sigma_{1}}\times\dots\times T_{\Omega}^{\sigma_{n}}\to
T_{\Omega}^{\sigma}\uplus E$ _interpretations_ of $f$ over the signature
$\Omega$. When $f:\sigma$ ($f$ is constant), then an interpretation is simply
an element of $T_{\Omega}^{\sigma}\uplus E$.

###### Definition 3.7 (Compositional translation).

Let $T_{\Sigma}$ be the source language and $T_{\Omega}$ be the core language.
An _interpretation_ of the source signature $\Sigma$ into the target language
$T_{\Omega}$ is a function $\pi$ that assigns an interpretation to every term
constructor $f\in\mathcal{F}_{\Sigma}$ over the signature $\Omega$. We refer
to $\pi(f)$ as a _translation rule_ for $f$ in $\pi$.

An interpretation of the source signature defines a sort-preserving function
$\delta:T_{\Sigma}\to T_{\Omega}\uplus E$ from source to core terms using
structural recursion. We will call such translations _compositional_. In
functional programming terms these are “folds” (or more precisely,
traversals), over the datatype defined by $\Sigma$.

###### Remark 2.

Note that in our intended translation of the example languages SPrim has two
rules. This poses no problem in kle’s original model: tree transducers, if the
tree transducer is not deterministic. But in our model we always assume one
translation rule per term constructor, and the rule for SPrim can only be
expressed by case analysis on lists.

###  3.4. Correctness

###### Definition 3.8 (Soundness).

Let $T_{\Sigma}$ and $T_{\Omega}$ be two languages, with two evaluation
functions $\Phi_{\Sigma}$ and $\Phi_{\Omega}$, respectively. A translation
$\delta:T_{\Sigma}\to T_{\Omega}\uplus E$ is _sound_ iff (cf. Figure 3)

$\forall t\in
T_{\Sigma}^{p},\Phi_{\Omega}(\delta(t))=\delta(\Phi_{\Sigma}(t))$

###### Remark 3.

A sound translation maps values to values or errors: if $v\in V(T_{\Sigma})$,
then $\Phi_{\Sigma}(v)=v$, and since $\delta$ is sound,
$\Phi_{\Omega}(\delta(v))=\delta(\Phi_{\Sigma}(v))=\delta(v)$, which means
that $\delta(v)$ is either a value or an error.

###### Definition 3.9 (Adequacy).

Let $T_{\Sigma}$ and $T_{\Omega}$ be two languages, with two evaluation
functions $\Phi_{\Sigma}$ and $\Phi_{\Omega}$, respectively. A translation
$\delta:T_{\Sigma}\to T_{\Omega}\uplus E$ is _adequate_ iff

$\forall v\in V(T_{\Sigma}),\delta(v)\in
V(T_{\Omega})\qquad\text{and}\qquad\forall v_{1},v_{2}\in
V(T_{\Sigma}),v_{1}\neq v_{2}\implies\delta(v_{1})\neq\delta(v_{2})$

that is, $\delta$ maps values to values and it is injective when restricted to
values.

###### Definition 3.10 (Correctness).

We will call a sound and adequate translation _correct_.

In practice we cannot test these conditions, provided the source language is
Turing-complete, by Rice’s theorem since correctness is a nontrivial program
property. We define notions approximating correctness with a set of source
programs: a _test set_. In a more general setting, we may assume that —
putting non-termination aside — we can choose to evaluate arbitrary source
language terms during the algorithm. Our approach abstracts away from the
choice of the test set.

###### Definition 3.11 (Correctness with respect to a test set).

Let $T_{\Sigma}$ and $T_{\Omega}$ be two languages with evaluation functions
$\Phi_{\Sigma}$ and $\Phi_{\Omega}$, respectively. Let $\mathcal{I}\subset
T_{\Sigma}^{p}$ be a subset of programs of the source language. A translation
$\delta:T_{\Sigma}\to T_{\Omega}$ is _sound with respect to the test set_
$\mathcal{I}$ iff

$\forall t\in\mathcal{I},\Phi_{\Omega}(\delta(t))=\delta(\Phi_{\Sigma}(t))$

A translation is _adequate with respect to the test set_ $\mathcal{I}$ iff

$\forall t\in\mathcal{I},\Phi_{\Sigma}(t)\notin
E\implies\delta(\Phi_{\Sigma}(t))\notin E\qquad\text{and}$ $\forall
t_{1},t_{2}\in\mathcal{I},\Phi_{\Sigma}(t_{1})\neq\Phi_{\Sigma}(t_{2})\implies\Phi_{\Omega}(\delta(t_{1}))\neq\Phi_{\Omega}(\delta(t_{2}))$

A translation is _correct with respect to the test set_ $\mathcal{I}$ iff it
is sound and adequate with respect to $\mathcal{I}$.

###### Remark 4.

Although we assumed above that all values are representable, languages with
non-representable values could be handled by requiring that the example
programs do return a representable value. A more difficult question is how to
deal with nondeterminism or observable side-effects (e.g. due to concurrency
or I/O); as far as we know all approaches to tested semantics rely on
repeatable (i.e. deterministic) tests.

###  3.5. Sublanguages

Our main idea is that compositional translations can naturally be partitioned
along with the language. First we define the notion of sublanguage and
language extensions, and then the extension of compositional translations.

###### Definition 3.12.

(Sublanguage) A signature
$\Sigma^{\prime}=(S,\mathcal{F}_{\Sigma^{\prime}},\mathit{sig}_{\Sigma^{\prime}})$
is a _subsignature_ of signature
$\Sigma=(S,\mathcal{F}_{\Sigma},\mathit{sig}_{\Sigma})$, denoted as
$\Sigma^{\prime}\subseteq\Sigma$, if

$\mathcal{F}_{\Sigma^{\prime}}\subseteq\mathcal{F}_{\Sigma}\qquad\text{and}\qquad\forall
f\in\mathcal{F}_{\Sigma^{\prime}},\mathit{sig}_{\Sigma^{\prime}}(f)=\mathit{sig}_{\Sigma}(f)\,.$

Let $\Phi_{\Sigma}$ be the evaluation function of the language $T_{\Sigma}$.
We will call $T_{\Sigma^{\prime}}$ the _sublanguage_ of $T_{\Sigma}$, if it is
closed with respect to the evaluation function, that is:

$\Sigma^{\prime}\subseteq\Sigma\qquad\text{and}\qquad\forall t\in
T_{\Sigma^{\prime}},\Phi_{\Sigma}(t)\in T_{\Sigma^{\prime}}\uplus E\,.$

We will also call $\Sigma$ an _extension_ of $\Sigma^{\prime}$ and similarly
$T_{\Sigma}$ an extension of $T_{\Sigma^{\prime}}$.

###### Definition 3.13 (Extension of a compositional translation).

Let $T_{\Sigma^{\prime}}$ be a sublanguage of $T_{\Sigma}$, and let
$T_{\Omega}$ be our target language. Let $\pi^{\prime}$ be an interpretation
of $\Sigma^{\prime}$ into $T_{\Omega}$. We will call an interpretation $\pi$
of $\Sigma$ into $T_{\Omega}$ an _extension_ of $\pi^{\prime}$ if it assigns
the same interpretation to every term constructor in the sub-signature:

$\forall f\in\mathcal{F}_{\Sigma^{\prime}},\pi^{\prime}(f)=\pi(f)$

We will also call the compositional translation $\delta$ defined by $\pi$ an
_extension_ of $\delta^{\prime}$ defined by $\pi^{\prime}$.

We intend to consider different _hypothesis spaces_ (i.e. sets of possible
desugaring rules to consider). We also might want to consider different
hypothesis spaces for different language extensions.

###### Definition 3.14 (Hypothesis space).

Let us fix $T_{\Sigma}$ as our source language and $T_{\Omega}$ as our target
language. Let $T_{\Sigma^{\prime}}$ be a sublanguage of $T_{\Sigma}$. The
hypothesis space corresponding to the signatures $\Sigma$, $\Sigma^{\prime}$
and $\Omega$ is an enumerable set of interpretations (into $T_{\Omega}$) for
each term constructor
$f\in\mathcal{F}_{\Sigma}\setminus\mathcal{F}_{\Sigma}^{\prime}$.

We will use $\mathcal{H}$ to stand for our chosen hypothesis space, and
$\mathcal{H}^{f}$ for the set of interpretations the hypothesis space assigns
to the term constructor $f$.

When the source language, its sublanguage, the target language, the
interpretation of the sublanguage into the target language and a hypothesis
space is understood, we will call a compositional translation that is an
extension of the interpretation of the sublanguage and generated by
interpretations belonging to the hypothesis space a _desugaring_.

###  3.6. The desugaring extension problem

We can finally define the sub-task: extending a desugaring from a sublanguage
to a larger portion of the language.

###### Definition 3.15 (Desugaring extension problem).

The learning task is defined as follows:

#### Inputs:

  * •

A signature $\Sigma$ of the source language, and a signature $\Omega$ of the
target language.

  * •

A finite test set of example input terms of the source language:
$\mathcal{I}\subset T_{\Sigma}^{\sigma_{p}}$, and their corresponding outputs
according to an evaluation function $\Phi_{\Sigma}$.

  * •

A black-box evaluation function $\Phi_{\Omega}$ for the language $T_{\Omega}$.

  * •

A subset signature $\Sigma^{\prime}\subset\Sigma$, that defines a sublanguage
$T_{\Sigma^{\prime}}$

  * •

A hypothesis space $\mathcal{H}$ for the sublanguage $T_{\Sigma}^{\prime}$.

  * •

A correct translation defined on the sublanguage:
$\delta^{\prime}:T_{\Sigma^{\prime}}\to T_{\Omega}$.

#### Output:

A desugaring $\delta:T_{\Sigma}\to T_{\Omega}$, such that:

  * •

$\delta$ is an extension of $\delta^{\prime}$

  * •

$\forall f\in\mathcal{F}_{\Sigma}\setminus\mathcal{F}_{\Sigma^{\prime}}$, the
translation rule of $f$ in $\delta$ belongs to the hypothesis space
$\mathcal{H}^{f}$

  * •

$\delta$ is correct with respect to the test set $\mathcal{I}$.

In the desugaring extension problem we have the interpretation of the
sublanguage’s term constructors as input, and we are searching for the rest of
the term constructors’ interpretations. The main differences between our task
and the task described (in an informal manner) by kle are:

  * •

We assume that the desugaring rules may be partially known.

  * •

We explicitly use multi-sorted terms and sort-preserving translations.

  * •

We assume that the test set of source programs $\mathcal{I}$ is given as
input, and the source language interpreter may not be called on inputs outside
of $\mathcal{I}$.

The first two points restrict the search space so that we can define feasible
tasks, and the last one simplifies the setting of our search problem.

Our example task as depicted in Figure 2 can also be seen as an instance of
the desugaring extension problem. The sublanguage $T_{\Sigma^{\prime}}$ is the
language only containing literals (numbers, strings), identifiers and
operation symbols, as their translation is fixed in advance (not included in
the intended translation); the extended language is the full Pidgin source
language. However, to the best of our knowledge it is not known how to solve
this problem as the search space is too large. Therefore we divide it into a
series of desugaring extension problems.

###  3.7. Sequential learning

Let us assume that we are looking for the full desugaring of a source language
$T_{\Sigma}$ into a target language $T_{\Omega}$. The user should divide the
language into an increasing series of sublanguages:

$\Sigma_{0}\subset\Sigma_{1}\subset\dots\subset\Sigma_{n}=\Sigma$

where, for every $n\in[1\dots n]$ , $T_{\Sigma_{n-1}}$ is a sublanguage of
$T_{\Sigma_{n}}$. Assume that we know the translation for $\Sigma_{0}$ (which
typically contains literals and operations for primitive types). The user also
needs to provide a hypothesis space $\mathcal{H}_{i}$ and a test set
$\mathcal{I}_{i}$ for each sub-task.

Right now we do not investigate how we can obtain suitable partitioning of the
language, or suitable test sets; we assume they are part of the user input.

###### Definition 3.16 (Sequential desugaring learning problem).

The definition of the full learning task:

#### Inputs:

  * •

A signature $\Sigma$ of the source language, and a signature $\Omega$ of the
target language.

  * •

A series of sub-signatures:
$\Sigma_{0}\subset\Sigma_{1}\subset\dots\subset\Sigma_{n}=\Sigma$ where, for
every $k\in[1\dots n]$ , $T_{\Sigma_{k-1}}$ is a sublanguage of
$T_{\Sigma_{k}}$.

  * •

A series of finite test sets $\mathcal{I}_{k}\subset T_{\Sigma_{k}}$ for every
$k\in[1\dots n]$, and their corresponding outputs according to an evaluation
function $\Phi_{\Sigma}$.

  * •

A black-box evaluation function $\Phi_{\Omega}$ for the core language
$T_{\Omega}$.

  * •

Hypothesis spaces $\mathcal{H}_{1},\ldots,\mathcal{H}_{n}$.

  * •

A desugaring defined on the minimal sublanguage: $\delta_{0}:T_{\Sigma_{0}}\to
T_{\Omega}$ that is correct on $T_{\Sigma_{0}}$.

#### Output:

A desugaring $\delta:T_{\Sigma}\to T_{\Omega}$, such that

  * •

$\delta$ is an extension of $\delta_{0}$

  * •

$\forall k\in[1\dots n],\forall
f\in\mathcal{F}_{\Sigma_{k}}\setminus\mathcal{F}_{\Sigma_{k-1}}$, the
translation rule of $f$ in $\delta$ belongs to the hypothesis space
$\mathcal{H}^{f}_{k}$

  * •

$\delta$ is correct with respect to the full test set $\bigcup_{k\in[1\dots
n]}\mathcal{I}_{k}$.

Note that the sequential desugaring learning problem is almost the same as the
desugaring extension problem, we merely added some additional inputs that
divide the search space, so we partition one desugaring extension problem into
a series.

###  3.8. Conditions of a solution

We conclude this section with a short discussion of research questions
entailed by our approach.

#### Do solutions exist? Can we solve sequential problems by composing
solutions one extension at a time?

Some desugaring extension problems may not have a solution, since the chosen
hypothesis space may not contain the intended desugaring. But even if a
correct desugaring exists, it is possible that the given partial desugaring
(while being correct on the sublanguage) can not be extended to a correct full
desugaring. The reason is that some state or value may not be accessible in
the sublanguage, which makes some globally bad translations correct when only
tested on the sublanguage. For example, desugaring a conditional if X then Y
else Z expression into Y could be correct in the sublanguage, if in the
sublanguage all Boolean expressions evaluate to true. Further examples are
desugaring a try-catch expression simply to the main body in a sublanguage
without exceptions, or desugaring a fst selector of a pair to an error value
in a sublanguage without pairs. This means that a naive, greedy strategy for
solving a sequential problem might not work: we might commit to the wrong
semantics for a sublanguage too early, making later extensions impossible.
These silly examples seem pathological, but in practice, it seems likely that
a work-in-progress semantics will be in such a “stuck” state most of the time,
so understanding and finding ways of mitigating this situation is a major
challenge.

#### Are solutions unique?

In program synthesis, especially in inductive (example-based) synthesis, it is
a common problem that there are multiple programs that satisfy the
specification (see (Gulwani et al., 2017), chapter 7.4). Our task is similar:
not only could semantically different translations be correct with respect to
the finite test set, but even correct translation rules often can be expressed
multiple, semantically equivalent ways. These equivalent programs can often be
transformed into each other by semantics-preserving transformations, like
swapping the two branches of a conditional expression and negating the
condition, etc. Our task has a special ambiguity of this kind, that not only
concerns the individual translation rules but the whole translation. The
reason is that languages often have (many) _symmetries_ : that is, correct,
invertible translations into themselves. A composition of two correct
translations is still correct, so such symmetries induce many equivalent but
syntactically different desugarings. Swapping two branches of the conditional
is just the special case of the well-known symmetry of the Boolean language
that exchanges true and false. It is possible to map Boolean constants to the
opposite values, switch the and and or logical operations, and switch the
order of the branches of the if conditional, extending the transformation form
an individual translation rule to the whole translation.

#### Can we devise test sets that ensure correctness?

It is also possible that there are multiple, semantically inequivalent
solutions that are correct with respect to the given test set, but not all of
them are correct with respect to the whole source language. A question that
arises is whether there a finite test set $\mathcal{I}$ such that if a
translation is correct with respect to $\mathcal{I}$ then it is correct with
respect to the whole source language? Assuming opaque evaluation functions
such a test set may not exist. What reasonable assumptions can we make about
the languages to ensure that such test sets exist? Moreover, when do small
test sets exist (where the size of a test set is the sum of the size of its
elements), so that we can find a correct desugaring not just in theory, but in
practice with extensive testing? In particular, since our approach currently
places the burden of designing a good test set on the user, it is an
interesting question whether (and how) we could also automate the process of
synthesising such test sets, perhaps in a counterexample-guided inductive
synthesis (CEGIS) loop (Solar-Lezama et al., 2005; Jha et al., 2010).

#### Can desugaring learning problems be decomposed into feasible sequential
extension problems?

A final, and perhaps most important, question is: what is the exact semantic
condition for the existence of a partitioning of the source language into a
series of sublanguages such that each desugaring extension problem is feasible
and collectively they lead to a solution of the full problem? For example,
such that each extension is small (contains less than $n$ term constructors
for some small $n$), extensions of partially correct translations exist in
each step, and the extension can be found with a small test set. This seems
like an inherently empirical and language-dependent question and in the rest
of this paper we present experimental results investigating this question for
the challenge problem.

##  4\. Searching for desugarings

###  4.1. The algorithm

We use a simple enumerative synthesis algorithm to solve our sub-tasks (the
desugaring extension problems). A sequential problem is solved greedily, using
the solution in each step as the input desugaring to the next step.

The algorithm sequentially tests each desugaring of the enumeration
$E_{\mathcal{H}}$ until a correct one is found or we reach a timeout. The test
condition directly corresponds to our definition of correctness with respect
to the test set $\mathcal{I}$: we test soundness for every test program, and
test adequacy by testing whether the number of distinct outputs (values or
errors) we get by either the source or the target interpreter is equal. If
they are, this, together with the already tested soundness, ensures the
injectivity of the translation on the values obtained from the test set.

The main complexity of this simple algorithm lies in the definition (and
efficient implementation) of the enumeration of desugarings $E_{\mathcal{H}}$.
Indeed, the main point of the algorithm is to reduce the problem to an
enumerative search: to the definition of a hypothesis space and an enumeration
of that hypothesis space. We might choose different hypothesis spaces for
different desugaring extension sub-problems, based on domain knowledge.

In the rest of the section we define various hypothesis spaces of increasing
expressiveness. The hypothesis spaces (sets of interpretations) are defined
inductively, parametrised by a given source signature
$\sigma_{1}\times\dots\times\sigma_{n}\to\sigma$. The full translation is
generated by a tuple of such interpretations for each term constructor in
$\Sigma\setminus\Sigma^{\prime}$. We will not investigate different
enumeration strategies: our enumerations are the same that we would get by
breadth-first search (but we use a more efficient implementation, to be
discussed in Section 5).

###  4.2. Relabelling

The simplest hypothesis space we will consider,
$\mathcal{H}_{\text{relabel}}$, is formed by the term constructors of the
target language. With $\mathcal{H}_{\text{relabel}}$ we can express
desugarings which map each constructor of the source language to a term
constructor of the target language of the same signature: a relabelling. Note
that any arguments of the source term constructor are translated recursively
and the order of arguments cannot be changed. We will call the desugaring
extension problem specialised to $\mathcal{H}_{\text{relabel}}$ the
_relabelling problem_.

In our intended translation many rules can be expressed as relabellings: in
fact all of them except but STrue, SFalse, SPrim, SBetween, and SFor can:

$\begin{array}[]{rcl}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SNum}(n)}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CNum}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}n}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SVar}(n)}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CVar}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}n}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\\\
\vdots&\vdots&\vdots\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SListCase}(t_{1},t_{2},t_{3})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CListCase}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{3}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}\end{array}$

Of course there are also translation rules in $\mathcal{H}_{\text{relabel}}$
that are not correct (and therefore not our intended translation):

$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SLetRec}(i,t_{1},t_{2})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}$
$\displaystyle={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}(i,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})}$

This example shows that even if we assume that the intended translation is a
relabelling we still may need appropriate test cases that rule out incorrect
translations, and they are not always completely trivial to find. To
distinguish between the recursive and non-recursive let construct we need an
example which actually behaves recursively when interpreted as letrec.

###  4.3. Substitution

The next hypothesis space, $\mathcal{H}_{\text{subst}}$, is defined by terms
with variables and substitution.

###### Definition 4.1 (Terms with variables).

Let $T_{\Omega}$ be an abstract language over signature
$\Omega(S,\mathcal{F},\mathit{sig})$, where
$S=\\{\sigma_{1},\dots,\sigma_{n}\\}$. Let a function $\rho:S\to\mathbb{N}$
assign a natural number to every sort in the signature. Let $X^{\rho}$ be a
finite set of variables, containing $\rho(\sigma)$ variables for every sort
$\sigma$:

$X^{\rho}=\\{x^{\sigma_{1}}_{1},\dots,x^{\sigma_{1}}_{\rho(\sigma_{1})},\cdots,x^{\sigma_{n}}_{1},\dots,x^{\sigma_{n}}_{\rho(\sigma_{n})}\\}$

and disjoint from $\mathcal{F}$. Extend the signature function to the new
variables as

$\forall\sigma\in S,\forall
i\in[1\dots\rho(\sigma)],\mathit{sig}(x^{\sigma}_{i})=\sigma$

We denote the the set of terms with variables from $X^{\rho}$ as
$T_{\Omega}(X^{\rho})$. The terms of $T_{\Omega}(X^{\rho})$ are called _terms
with variables_ over the language $T_{\Omega}$. A term
$t_{\mathcal{X}^{\rho}}\in T_{\Omega}(\mathcal{X}^{\rho})$ defines a function
by substituting the arguments into the variables. We will refer to
translations (and interpretations) that can be expressed by terms with
variables as _substitutions_.

Let $f\in\mathcal{F}_{\Sigma}$, and let $\rho_{f}(\sigma)$ be the number of
times $\sigma$ occurs in the domain of the signature of $f$. The hypothesis
space is defined as $\mathcal{H}^{f}=T_{\Omega}(\mathcal{X}^{\rho_{f}})$.

Every relabelling is a substitution. The resulting task is close to the
formulation of kle, who suggested modelling desugarings as tree transducers
(Comon et al., 2007). The translations defined by translation rules in
$\mathcal{H}_{\text{subst}}$ are also definable by a deterministic top-down
tree transducer: $\mathcal{H}_{\text{subst}}$ guarantees that the output of a
translation is well-typed according to the core language’s signature
(corresponds to the grammar), and that the translation preserves the sorts.

A further difference is that in our hypothesis space a term constructor
determines the translation rule. The two translation rules for SPrim can not
be expressed in this hypothesis space. Expressing the two rules for SPrim is
possible with a bottom-up tree transducer or a non-deterministic top-down tree
transducer (both of which are more expressive than deterministic top-down tree
transducers), but requires additional states that do not correspond to the
sorts defined by the grammar.

While this hypothesis space is much more expressive than relabellings, only
two additional rules of the example intended translation can be covered:

$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{STrue}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}$
$\displaystyle={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CBool}(\mathit{true})}$
$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SFalse}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}$
$\displaystyle={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CBool}(\mathit{false})}$

The main reason is that the Pidgin source and core languages were specifically
chosen by kle to show potential problems with modelling the translation with a
tree transducer. In the following section, we introduce one of our main
contributions, a simple model which can express all of Pidgin’s translation
rules, as well as the multiple rules for SPrim.

###  4.4. Meta-program templates

In general, the translations could be written in an appropriate meta-language,
which could easily express all intended translation rules. But synthesising
translation rules in a general purpose language is a very challenging task: we
are looking for the most restricted hypothesis space that can still express
the translations. As a middle ground, we consider extending the former
hypothesis space $\mathcal{H}_{\mathrm{subst}}$ with a fixed finite set of
templates, written in a general-purpose meta-language that allows expressing
the remaining cases.

$\small\begin{array}[]{rcl}\sigma_{1},\dots,\sigma_{n},\sigma&\in&S\\\
f&\in&\mathcal{F}\\\ t&::=&x\mid c\mid f(t_{1},\ldots,t_{n})\end{array}$

Axiom $\displaystyle\Gamma;x:\sigma\vdash x:\sigma\mathstrut$
$\displaystyle{c:\sigma}\mathstrut$ C-rule $\displaystyle\Gamma\vdash
c:\sigma\mathstrut$ $\displaystyle{\Gamma\vdash
t_{1}:\sigma_{1}}\mathstrut$$\displaystyle{{\hskip 8.00003pt{\cdots}}\hskip
8.00003pt{\Gamma\vdash t_{n}:\sigma_{n}}}\hskip
8.00003pt{f:\sigma_{1}\times\dots\times\sigma_{n}\to\sigma}\mathstrut$ F-rule
$\displaystyle\Gamma\vdash f(t_{1},\dots,t_{n}):\sigma\mathstrut$

Figure 4. Terms with variables as proofs

$\small\begin{array}[]{rcl}t&::=&\dots\mid\mathbf{let}\,i=\mathtt{gensym}()\,\mathbf{in}\,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t_{1},t_{2})\\\
M,N&::=&t\mid\mathbf{let}\,(x_{1},x_{2})=\mathtt{unzip}(x)\,\mathbf{in}\,M\mid\mathbf{syntax\\_error}\mid\mathbf{case}\,y\,\mathbf{of}\,[]\to
M;(x:y)\to N:\sigma^{\prime}\end{array}$

~

$\displaystyle{\Gamma;x_{1}:[\sigma_{1}],x_{2}:[\sigma_{2}]\vdash
M:\sigma}\mathstrut$ Unzip
$\displaystyle\Gamma;x:[\sigma_{1}\times\sigma_{2}]\vdash\mathbf{let}\,(x_{1},x_{2})=\mathtt{unzip}(x)\,\mathbf{in}\,M:\sigma\mathstrut$
Throw $\displaystyle\Gamma\vdash\mathbf{syntax\\_error}:\sigma\mathstrut$

$\displaystyle{\Gamma\vdash M:\sigma^{\prime}}\mathstrut$$\displaystyle\hskip
8.00003pt{\Gamma;x:\sigma,y:[\sigma]\vdash N:\sigma^{\prime}}\mathstrut$ Case
$\displaystyle\Gamma;y:[\sigma]\vdash\mathbf{case}\,y\,\mathbf{of}\,[]\to
M;(x:y)\to N:\sigma^{\prime}\mathstrut$

$\displaystyle{\Gamma\vdash
t_{1}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}}\mathstrut$$\displaystyle\hskip
8.00003pt{\Gamma;x:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}\vdash
t_{2}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}}\mathstrut$
Fresh
$\displaystyle\Gamma\vdash\mathbf{let}\,i=\mathtt{gensym}()\,\mathbf{in}\,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t_{1}}},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t_{2}}}[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CVar}}(i)/x]):{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}\mathstrut$

Figure 5. Rules for meta-program templates

In our current approach, it is up to the user to determine the set of
templates used at an individual learning step. Our contribution is a general
framework (implemented as a library) that can incorporate various templates
and provide an enumeration of all well-typed translations formed by them. We
demonstrate the technique with a set of templates we wrote for the Pidgin
languages.

To formally describe the new system $\mathcal{H}_{\text{meta}}$, we start with
the re-formulation of $\mathcal{H}_{\text{subst}}$ as deductive rules, in a
sequent calculus style, shown in Figure 5. Our judgements describe meta-
language programs. They are of the form $\Gamma\vdash t:\sigma$, where
$\Gamma$ is the context (variable declarations, the argument names and their
sorts), $t$ is a term of the meta-language describing a translation rule, and
$\sigma$ is a sort of the output. The context is a set of pairs of variables
with their corresponding sort in the form of $x:\sigma$, where $x$ is a meta-
variable name (not an identifier in the source or core languages), and
$\sigma$ is a sort. $\Gamma$ will range over such contexts, and we extend a
context $\Gamma$ with additional variable declarations $x:\sigma_{1}$ and
$y:\sigma_{2}$ as $\Gamma;x:\sigma_{1},y:\sigma_{2}$. We identify
$\alpha$-equivalent meta-terms. In the implementation the meta-variable names
in the context $\Gamma$ are determined by the signature (the set of sorts),
but in the presentation we avoid this complication. Note that this only
concerns the meta-variables, and not any identifiers (if present) in the core
language: we did not assume to know the $\alpha$-equivalence relation of the
core language (if any).

Enumerating all translation rules corresponding to a source signature
$\sigma_{1}\times\dots\times\sigma_{n}\to\sigma$ is thus implemented as
enumerating all proofs of the judgement
$x_{1}:\sigma_{1},\dots,x_{n}:\sigma_{n}\vdash t:\sigma$. This way we reduce
the desugaring extension problem to enumerative synthesis, that allows us to
compare various hypothesis spaces and enumeration strategies.

We could have chosen different styles of sequent calculus to describe the same
system. Our style has the big advantage that proofs and terms (with variables)
directly correspond to each other: there are no permutations of the proof
rules that yield effectively the same terms, thus enumerating the terms is
much easier.

Now that we have expressed our translations as proof terms, we can extend them
with arbitrary templates from a functional meta-language. Figure 5 shows some
possible meta-program templates added as derivation rules. We use two kind of
templates.

The first group are meta-programs that act on the source terms: we call them
left-rules since they operate on the left side of the judgement. We may note
that some sorts are structurally equivalent to lists or tuples of other sorts,
and use them as such in the meta-programming language. For example, we
introduced
$\texttt{List}_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textit{SForBind}}}$
for a list of terms belonging to the sort SForBind, while the sort SForBind
itself is structurally equivalent to a tuple of an identifier and a source
term. This allows us to use functions like $\mathtt{unzip}$. In the
presentation we used the notation $[\sigma]$ to mean a sort that is
structurally equivalent to a list, and $\sigma_{1}\times\sigma_{2}$ to mean a
sort that is structurally equivalent to a tuple. The first rule, Unzip, turns
a list of tuples into two lists. With this primitive operation we can express
the rule for SFor. The Case rule allows us to destruct a list, and allows us
to express the two rules for SPrim (distinguished by the number of children)
as one. But the Case rule alone is not sufficient, as we need to do something
when the list of children is empty, which is allowed by our source grammar,
but results in an error in the source language interpreter. To represent
compile-time errors not caught by the grammar we introduce a meta-program for
syntax errors. Note that this assumes that translation rules are performed in
the error monad: compile time errors are observable side-effects, and we need
a way to express them.

The second group are meta-programs that encode typical core program templates.
This technique is currently demonstrated by a single rule: the Fresh rule
demonstrates fresh name generation, which allows us to express the translation
rule for SBetween. The meta-function $\mathtt{gensym}()$ generates unique
identifiers for the core language, which are bound to a meta-language variable
$i$. We use this fresh variable as the local variable introduced by CLet, and
in the scope of the variable we replace the meta-argument with dereferencing
it. This rule relies on additional domain knowledge: the binding and scoping
information of the core language (but can be auto-generated if this
information is available in addition to the grammar). Note that in the scope
we only allow dereferencing the identifier as a variable
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CVar}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}})}$),
not to use it in arbitrary positions identifiers may occur, for example as a
local variable introduced by a CLam.

Using $\mathcal{H}_{\mathsf{meta}}$, we can express the remaining desugaring
rules.

$\small\begin{array}[]{rcl}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SBetween}(t_{1},t_{2},t_{3})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&\mathbf{let}\,i_{1}=\mathtt{gensym}()\,\mathbf{in}\,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}(i_{1},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}},\\\
&&\mathbf{let}\,i_{2}=\mathtt{gensym}()\,\mathbf{in}\,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}(i_{2},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}},\\\
&&\mathbf{let}\,i_{3}=\mathtt{gensym}()\,\mathbf{in}\,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}(i_{3},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{3}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},}\\\
&&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CPrim2}(\land,\texttt{CPrim2}(<,\texttt{CVar}(i_{1}),\texttt{CVar}(i_{2})),\texttt{CPrim2}(<,\texttt{CVar}(i_{2}),\texttt{CVar}(i_{3}))))))}\\\
\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SPrim}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}o}},ts)}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&\mathbf{case}\,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}ts}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}\,\mathbf{of}\,[]\to\mathbf{syntax\\_error};\\\
&&\qquad\qquad(t_{1}:ts_{1})\to\mathbf{case}\,ts_{1}\,\mathbf{of}\,[]\to{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CPrim1}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}o}},t_{1})};\\\
&&\qquad\qquad\qquad\qquad\qquad\qquad(t_{2}:ts_{2})\to\mathbf{case}\,ts_{2}\,\mathbf{of}\,[]\to{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CPrim2}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}o}},t_{1},\
t_{2})};\\\
&&\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad(\\_:\\_)\to\mathbf{syntax\\_error}\\\
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SFor}(t_{1},bs,t_{2})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&\mathbf{let}\,(ids,ts)=\mathtt{unzip}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}bs}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket})\,\mathbf{in}\\\
&&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CApp}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},[\texttt{CLam}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}ids}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}),\texttt{CList}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}ts}})])}\end{array}$

Note that we could have included a more general rule instead of Fresh:

$\displaystyle{\Gamma;y:\texttt{Id}\vdash
M:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}}\mathstrut$
Fresh′
$\displaystyle\Gamma\vdash\mathbf{let}\,y=\mathtt{gensym}()\,\mathbf{in}\,M:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}\mathstrut$

This version only relies on $\mathtt{gensym}$ being a meta-function generating
identifiers. It is possible to express the intended translation with the more
general Fresh′ rule. This version, however, blows up the search space as fresh
names could be generated anywhere. In our scope-aware version we relied on the
domain knowledge that fresh names only need to be introduced in language
constructs that bind new names, and only allowed to be used as variable
references in the scope of the binding. This can be extended to other name-
binding constructs, and Fresh can be seen as an example of a general pattern:
we will show two other examples of it in Section 6.

But introducing the meta-rules breaks the nice property of the correspondence
between proofs and translations: there are multiple proofs corresponding to
essentially the same translation, because the left rules such as Unzip or Case
can be permuted with the right rules and the core constructors. This prevents
us to efficiently enumerate such programs with our simple enumeration
algorithm, and results in the explosion of the search space.

We remedy the problem by restricting the order of the templates by layering.
Note that the left rules can always be pulled to the top of the term: in the
meta language the left rules are functions while the rest are data. (To be
precise the Fresh rule contains both, but it does not affect the uniqueness of
the translation.) We divide the rules to right rules (the Axiom, the C-rule,
the F-rule and the Fresh rule) and left rules (Unzip, Case, and Throw rules),
and require that left rules are never used in the sub-terms (premises) of a
right rule. This layering does not completely solve the problem: there still
could be permutations amongst the left rules that lead to identical
translations, but it is hard to exclude them without analysing the rules.

As a summary, we may speculate how much user assistance is needed to set up
the necessary meta-rules. We can identify three general patterns: to
deconstruct source terms (Case), to allow compile time errors (Throw) and to
generate fresh names in binding positions (Fresh). We can imagine these meta-
rules to be auto-generated. But our last meta-rule, Unzip, does not completely
fall into these patterns, and shows that in some cases more user assistance is
needed.

###  4.5. Restricting and combining hypothesis spaces

The last hypothesis space, $\mathcal{H}_{\text{meta}}$, contains every
intended translation rule. But this hypothesis space is too large for our
simple enumerative algorithm, and in some test cases we failed to learn the
intended desugaring rule within our timeout of 1 hour on the test machine. We
introduce two techniques, layering and restriction, to define subsets of
$\mathcal{H}_{\text{meta}}$.

We have already used layering to prune some equivalent translations from the
enumeration. We allow the user to specify additional layers. One natural
additional layer is to only allow the Fresh rule (and similar fresh identifier
introducing rules) at the top (below left rules, but above core term
constructors). The reasoning is similar: it is likely that these rules would
be at the top if we could convert core language terms to $\beta$-normal form.
However, unlike the meta-language, the core language is a parameter of the
problem, and in general we do not know its equivalence relation. Therefore we
handle the layer for the left rules as fixed, while leaving introducing a
layer for the Fresh rule in the hands of the user, who can leverage domain
knowledge of the core language.

Layering alone is still not enough, and another straightforward technique to
define a subset of $\mathcal{H}_{\text{meta}}$ is to only allow a subset of
rules. We allowed the user to restrict meta-rules to a subset, relying on
domain knowledge. This is not surprising: a typical core language, even our
simplified Pidgin core, is much larger than the DSLs targeted by successful
program synthesis methods.

In the desugaring extension problem we may need to search for the translation
rules of multiple term constructors at the same time. We currently always use
fair interleaving: without domain specific knowledge about the languages we
can not assume a bias which will generalise well.

##  5\. Implementation

We used Haskell to carry out our investigations. Writing test cases requires
implementing source and core languages, translations between them,
enumerations of such translations, and implementing the search algorithm.

The implementation of the small source and core languages involved in the
tests as embedded languages is standard (simplified versions of these
implementations are shown in Appendix A). To deal with non-terminating
programs we implemented bounded evaluation (limiting the number of steps
allowed in the interpreter).

The implementation of the simple linear search over the enumerations based on
the testing framework shown in Figure 3 is also straightforward. The crucial
part of the implementation, which we discuss in some detail, is the
implementation of the enumeration of the translations, in particular, how to
enumerate efficiently the proofs of $\mathcal{H}_{\text{meta}}$.

We have implemented a library that can efficiently enumerate the proof terms
generated by arbitrary rules corresponding to our sequent calculus-like
formalism. The user of the library can write arbitrary Haskell functions that
either operate on the source language terms or serve as templates for core
language terms, corresponding to our two types of meta-rules. The sequent
calculus rules ensure that the library only enumerates well-typed terms.

We tested depth-first search and iterative deepening, but they proved to be
too memory intensive and slow. Our current solution builds on the FEAT Haskell
library (Duregård et al., 2012), that provides efficient functional
enumerations of algebraic data types (ADTs) out of the box.

Proofs of judgements of the form
$x_{1}:\sigma_{1},\ldots,x_{m}:\sigma_{n}\vdash T:\sigma$ can not be
represented naturally by an ADT. We want to restrict meta-variables to those
that are available in the environment
$x_{1}:\sigma_{1},\ldots,x_{m}:\sigma_{n}$, and we would need a separate ADT
for each environment in order to enforce this. But meta-rules can introduce
new environments. We implemented environment-dependent enumerations relying on
the library primitives, and we used memoisation and cached the generated
enumerations for the given environment. The enumerations are recursive in a
non-trivial way and our implementation quickly exhausted available memory
without this optimisation.

The enumerative search is embarrassingly parallel, and we expect a fully
parallel implementation to help a lot. So far we only did a preliminary
investigation of parallelism relying on Haskell’s deterministic parallelism
capabilities (Marlow et al., 2009), and while it clearly speeds up the search,
most likely better performance could be achieved with a more fine tuned
parallel implementation. Our experiments report timings with deterministic
parallelism employed. In recent versions of GHC the garbage collector can
exploit multiple cores: we also enabled this optimisation for the compiler.
The code to reproduce our case studies is available at
http://10.5281/zenodo.5475211.

##  6\. Evaluation

We evaluate our approach and the enumeration synthesis library on three case
studies. The first is the Pidgin languages that we used to demonstrate our
approach throughout the paper. As a preliminary exploration of how well the
method generalises, as well as to demonstrate some limitations of our
approach, we extend the Pidgin languages with two sets of language constructs:
list comprehensions and exception handling. We extend both the core language
and the source language, and investigate whether we can extend our sequential
learning algorithm to the new cases seamlessly. Our experiments were run on a
Intel E3-1245v5 @ 3.50GHz with 8 cores and 32 GB RAM, running Debian Linux 10
and GHC 8.8.4.

###  6.1. Hypothesis

Our hypothesis is that for the challenge problem we can set up a sequential
learning task where each individual desugaring extension problem can be solved
with our enumerative synthesis algorithm and combined to solve the overall
problem. Moreover we also hypothesise that when we extend the core and source
languages with new constructs we can extend the sequential learning task with
new steps as well, and solve these new desugaring extension problems with the
same algorithm.

As the hypothesis space is a parameter of the algorithm (and the desugaring
extension problems) and ultimately in the hand of the user, it is hard to
measure how well the method generalises: on one hand, we can set up a
hypothesis space that only contains the intended translation as a meta-rule,
and on the other hand we could fill the hypothesis space with so many meta-
rules that enumerative search is hopeless. Our method was to start with a (to
us) natural hypothesis space, and in the cases where we were not able to get
results within a 1 hour timeout, we repeated the test with additional user
assistance. While we do report various metrics from our tests, we think the
amount of user assistance needed for each step to successfully complete is the
most useful metric for an envisioned semi-automated assistant.

###  6.2. Pidgin languages

Setup. The Pidgin source and core languages was shown in Figure 2. We assumed
that part of the translation is known in advance. The sublanguage $\Sigma_{0}$
contains numbers, strings, identifiers and the constructors for lists, and we
assumed that their translation is known (which means that numbers, strings and
identifiers and list of identifiers are preserved, and lists of source terms
are translated to lists of core terms by individually translating the
elements).

Hypothesis space. The starting hypothesis space $\mathcal{H}^{1}$ contained
all core term constructors, including list constructors for term and
identifier lists. It did not contain number, string or identifier constants.
In general, we do not want to allow such constants in the hypothesis space:
they rarely occur in desugaring rules and they blow up the search space.
However, we need the Boolean constants true and false, which is clear, since
the Boolean sort is not part of the source language. We also included all
operators, which requires some domain knowledge about their role: while
operators are constants, they correspond to various functions. The hypothesis
space also contained all meta-rules listed in Figure 5: Case, Throw, Unzip and
Fresh.

We also use a second, specialised hypothesis space $\mathcal{H}^{2}$. This
hypothesis space only allowed the core term constructors CVar and CPrim2, the
meta-rule Fresh, and all constants from $\mathcal{H}^{1}$, reducing the size
of the hypothesis space significantly.

Results. We run the first test with $\mathcal{H}^{1}$, and we found all
intended translation rules within the time limit but one: this test did not
find the intended desugaring for SBetween.

We run a second test where we replaced the desugaring extension problem for
SBetween (step $\Sigma_{7}$) based on $\mathcal{H}^{1}$ with a new one based
on $\mathcal{H}^{2}$. The new sequential learning task gives us a full
solution of the challenge problem. It is summarised in Table 1.

Task | New constructors | Hyp. space | AST size | Index | #test set | Time
---|---|---|---|---|---|---
$\Sigma_{1}$ | SNum | $\mathcal{H}^{1}$ | 2 | 1 | 2 | 0s
$\Sigma_{2}$ | SStr | $\mathcal{H}^{1}$ | 2 | 1 | 2 | 0s
$\Sigma_{3}$ | SPrim | $\mathcal{H}^{1}$ | 12 | 16567100 | 5 | 3min9s
$\Sigma_{4}$ | ${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SVar}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SLet}}$ | $\mathcal{H}^{1}$ | 6 | 1298 | 2 | 0s
$\Sigma_{5}$ | ${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{STrue}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SFalse}}$ | $\mathcal{H}^{1}$ | 4 | 10 | 4 | 0s
$\Sigma_{6}$ | SAssign | $\mathcal{H}^{1}$ | 3 | 18 | 1 | 0.0s
$\Sigma_{7}$ | SBetween | $\mathcal{H}^{2}$ | 14 | 157160392 | 9 | 28min2s
$\Sigma_{8}$ | SIf | $\mathcal{H}^{1}$ | 4 | 171 | 2 | 0s
$\Sigma_{9}$ | ${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SLam}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SApp}}$ | $\mathcal{H}^{1}$ | 6 | 1813 | 2 | 0s
$\Sigma_{10}$ | SLetRec | $\mathcal{H}^{1}$ | 4 | 132 | 1 | 0s
$\Sigma_{11}$ | SList | $\mathcal{H}^{1}$ | 2 | 3 | 2 | 0s
$\Sigma_{12}$ | SListCase | $\mathcal{H}^{1}$ | 4 | 207 | 2 | 0s
$\Sigma_{13}$ | SFor | $\mathcal{H}^{1}$ | 11 | 57334664 | 3 | 9min29s
$\Sigma$ | total |  |  |  | 35 | 40min40s
Table 1. Case study – Pidgin languages

The rows of the table correspond to desugaring extension problems. In each
problem $\Sigma_{n}$ the translation of the sublanguages
$\Sigma_{0},\dots,\Sigma_{n-1}$ are assumed to be known. We work our way
downwards: the test sets can not use term constructors from below. To get some
rough measurement of the complexity of each task we noted the size of the
intended desugaring (AST size), and also the _index_ of the translation found
in the enumeration for each desugaring extension problem, that is, the number
of attempts tried before a solution was found. We also show the number of
handwritten tests we used to find the solution. The solution found was exactly
the intended translation in Figure 2 in all but one case: SBetween.

In the case of SBetween the algorithm finds an expression equivalent to our
intended translation but smaller:

$\begin{array}[]{rcl}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SBetween}(t_{1},t_{2},t_{3})}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}&=&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CLet}(\%i_{1},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{1}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},\texttt{CLet}(\%i_{2},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{2}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket},}\\\
&&{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{CPrim2}(\land,\texttt{CPrim2}(<,\%i_{2},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{3}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}),\texttt{CPrim2}(<,\%i_{1},\%i_{2})))))}\\\
\end{array}$

Decomposition. The desugaring extension problems’ test sets can not contain
source term constructors from later extensions, but the test set still needs
to exclude all non-intended translations. This means that we can not learn
SLam and SApp separately, as they only show their behaviour together: we can
see that they are grouped together in the task $\Sigma_{4}$.

kle did not specify the exact semantics of the source and core languages —
this give us a little bit of freedom implementing them. Our implementation
does not allow executing open programs containing non-declared variables, that
is, all variables must be declared in a SLam, SLet or SLetRec expression
before use, otherwise an exception is raised. This means that we can not use
SVar on its own without one of these: we grouped it together with SLet in task
$\Sigma_{9}$.

The last case where we needed to group multiple term constructors together was
the STrue, SFalse group. The symmetry of the Boolean constants means that we
need to learn them together and rely on the already fixed translations of the
and and or operations to rule out translations that map to the opposite
Boolean value in the core language.

Since all other groups only contain one term constructor, this decomposition
shows that quite often we do not need to learn more than one rule at a time.
This supports our hypothesis that the language can be partitioned into small
groups of term constructors.

Test cases. The majority of test programs are very small and simple: in most
cases we do not need large test programs, and it is plausible that they could
be generated by automatic testing. There are three exceptions. To learn the
full semantics of SBetween we needed test programs where the evaluation order
of arguments matters. To distinguish SLetRec from SLet we needed recursive
examples. The source term constructor SFor assumes a combinator function as
its first argument, which leads to an example that dwarfs the rest. This last
case is somewhat artificial, though.

In many cases our algorithm found a desugaring that is equivalent to the
intended semantics on pure terms, but differs in the evaluation order of the
arguments. Pidgin source has side effects: the SAssign operator. We utilised
it to add test cases that depend on the evaluation order.

Sometimes the order of the examples is important. The majority of the time is
spent evaluating various core programs that we get by the tested translations,
especially when – like in the case of SFor – we need recursive examples.
Recursive examples easily lead to non-terminating core programs, thus the time
spent checking prospective translations on them greatly depends on the maximum
number of steps allowed in the interpreter. If this bound is too low, we may
get an incorrect desugaring, if too high, the search may take a long time. We
can learn the intended semantics of SFor with only one test program, but since
it needs to be recursive and large, the search time suffers, and depends on
the value of the parameter making the learning process impractical. As
currently we can only tune this parameter manually (automatic tuning is left
to future research), it is important for performance to use simple, non-
recursive source programs as the first test cases in a test suite. With our
test setup (in which we added such a test program before the full example) we
found that a reasonably high bound parameter does not have a large effect on
the time of the search, so no manual tuning was needed, while the search time
was reduced by around 90%.

###  6.3. Basic list comprehensions

Setup. For our first extension of the Pidgin languages we consider basic list
comprehensions a la Wadler (1992b) with the following syntax:

$\small\begin{array}[]{rclcrcl}t&::=&\cdots\mid[t\mid q]&&q&::=&\epsilon\mid
x\leftarrow t,q\mid t,q\mid\mathrm{let}~{}x=t,q\end{array}$

This is a simplification over standard Haskell list comprehensions, which
support patterns in bindings and more general definitions in `let`. The
following table shows the extensions of the syntax of the Pidgin languages
required for this case study:

$\small\begin{array}[]{rcl}t\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textit{STerm}}&::=&\dots\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{SListComp}(t,q)}\\\
q\in{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textit{SQual}}&::=&{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{QEmpty}}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{QBind}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t,q)}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{QGuard}(t,q)}\mid{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{QLet}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},t,q)}\\\
e,e_{1},e_{2}\in{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\textit{CTerm}}&::=&\dots\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MVar}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}})}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MLam}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}i}},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}e}})}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{MApp}(\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}e_{1}}},\mathit{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}e_{2}}})}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{Return}(e)}\mid{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\texttt{Bind}(e_{1},e_{2})}\end{array}$

The Return and Bind primitives correspond to the following standard Haskell
functions:

    return :: a -> [a]   (>>=)  :: [a] -> (a -> [b]) -> [b]

The desugaring of comprehensions is described as a two-argument function
$D[t|q]$ in the GHC
documentation111https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/monad_comprehensions.html).
This does not quite fit our framework, but can be expressed by desugaring
qualifiers to functions
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}q}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}$
mapping core terms to core terms, and desugaring a comprehension by applying
the function to
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\llbracket}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rrbracket}$.
While it is natural to express the desugarings of qualifiers with meta-level
lambdas, our current framework does not allow meta-level abstractions.
Instead, we extended the core language with macros: MVar, MLam and MApp, that
provide textual substitution. Core language macros allow us to approximate a
higher-order meta-language.

The generic comprehension desugaring rules used in GHC actually allow for