Synthesis of Recursive Programs in Saturation

Abstract

We turn saturation-based theorem proving into an automated framework for recursive program synthesis. We introduce magic axioms as valid induction axioms and use them together with answer literals in saturation. We introduce new inference rules for induction in saturation and use answer literals to synthesize recursive functions from these proof steps. Our proof-of-concept implementation in the Vampire theorem prover constructs recursive functions over algebraic data types, while proving inductive properties over these types.

1 Introduction

Program synthesis is the task of constructing a program P satisfying a given specification F, ensuring that P is correct by design [20]. In this paper we work with a functional specification F of the input-output relation of a program P, where F is given as a $\forall \exists$ formula in first-order logic [1, 20]. Validity of a specification formula F ensures that for every input value there exists an output value satisfying F, and therefore there is a function which for every input value gives such an output value. Our goal is to automatically find a (possibly recursive) program that P computes the output, while preserving F.

As a complementary approach to formal verification, synthesis is inherently more complex [28]. The complexity is further compounded when we consider reasoning about – and synthesizing – programs using recursion. As a remedy, in this paper we advocate for using automated first-order theorem proving as the reasoning back-end to (recursive) program synthesis.

The work [8] extended the saturation-based first-order theorem proving framework to saturation-based synthesis framework. The approach (i) uses saturation-based reasoning to prove that a specification F is valid; (ii) tracks the constructive parts of the proof of F; (iii) and uses them to synthesize a program P satisfying F. In this paper we complement [8] with support for recursive program synthesis. We use recent developments on automating induction in saturation [5, 7, 9, 25] and construct recursive programs based on applications of induction.

Fig. 1.

Axioms of $\textsf{half}$ and the $\forall \exists$-specification for the function computing double.

Illustrative Example. Consider the specification (SD) of Fig. 1, which describes the inverse of the $\textsf{half}$ function over natural numbers. Given the axiomatization of $\textsf{half}$ in Fig. 1, our approach synthesizes the recursive function $\textsf{double}$ as a solution of (SD), defined as:

$$\begin{aligned} \begin{aligned} \textsf{double}(\textsf{0}) &\simeq \textsf{0}\\ \forall x.\ \textsf{double}(\textsf{s}(x)) &\simeq \textsf{s}(\textsf{s}(\textsf{double}(x))) \end{aligned} \end{aligned}$$

(1)

The framework of [8] fails to synthesize a solution of (SD), as $\textsf{double}$ is a recursive program. To the best of our knowledge, there exists no automated approach supporting recursive function synthesis from functional input-output specifications in full first-order logic.

This paper provides a solution in this respect by exploiting the constructive nature of induction. Intuitively, each case of an induction axiom tells us how to construct the desired program for the next recursive step using the program for the previous recursive step. We capture this construction recipe contained in the applications of induction in saturation-based proof search, by utilizing answer literals $\textsf{ans}(r)$ [4]. When we use an induction axiom in the proof, we introduce a special term into the answer literal, serving for tracking the program corresponding to the induction axiom. As we prove the cases of the induction axiom, we capture their corresponding programs in the answer literal. Finally, when we derive a clause $C\vee \textsf{ans}(r)$, where C only contains symbols allowed in a program, we convert the special tracker terms from r into recursive functions, and obtain a program for the initial specification conditioned on $\lnot C$.

Contributions. We extend saturation-based first-order theorem proving with recursive program synthesis and bring the following contributions¹:

• We introduce induction axioms, dubbed magic axioms, which capture the constructive nature of induction (Sect. 5).

• We convert the magic axioms into formulas used by a saturation-based framework to derive programs using recursion over algebraic data types, i.e., special cases of term algebras. We state necessary requirements for the calculus used in saturation and prove correctness of synthesized programs (Sect. 6).

• We present an extension of the superposition calculus that fulfills our necessary requirement and advocate for superposition reasoning for recursive function synthesis (Sect. 7).

• We show that our approach, illustrated initially for natural numbers, naturally extends to programs over arbitrary term algebras (Sect. 8).

• We implement our work in the Vampire prover [16] and survey challenging examples it can synthesize (Sect. 9).

2 Preliminaries

We assume familiarity with standard multi-sorted first-order logic (FOL) with equality. We denote variables by x, y, z, w, u, terms by s, t, r, atoms by A, literals by L, clauses by C, D, formulas by F, G, all possibly with indices. Further, we write $\sigma$ for Skolem constants. We reserve the symbol $\square$ for the empty clause which is logically equivalent to $\bot$. We write $\overline{L}$ for the literal complementary to L. By $\simeq$ we denote the equality predicate and write $t\not \simeq s$ as a shorthand for $\lnot t\simeq s$. We include a conditional term constructor $\textsf{if}\!-\!\textsf{then}\!-\!\textsf{else}$ in the language, as follows: given a formula F and terms s, t of the same sort, we write $\textsf{if}\ F\ \textsf{then}\ s\ \textsf{else}\ t$ to denote the term s if F is true and t otherwise. An expression is a term, literal, clause or formula. We write E[t] to denote that the expression E contains the term t. For simplicity, E[s] denotes the expression E where all occurrences of t are replaced by the term s. Formulas with free variables are considered implicitly universally quantified, that is we consider closed formulas.

We use the standard semantics for FOL. For an interpretation function I, we denote the interpretation of a variable x, function symbol f and a predicate symbol p by $x^I, f^I, p^I$, respectively. We use the notation $e^I, F^I$ also for the interpretation of expressions e and formulas F, respectively. Further, for a variable or a constant a and a value v, we denote by $I\{a\mapsto v\}$ the interpretation function $I'$ such that $a^{I'}=v$ and $b^{I'} = b^I$ for any constant or variable $b\not =a$. We write $F_1,\ldots ,F_n \vdash G_1,\ldots ,G_m$ to denote that $F_1 \wedge \ldots \wedge F_n \rightarrow G_1\vee \ldots \vee G_m$ is valid, and extend the notation also to validity modulo a theory T.

We recall the standard notion of $\lambda$-expressions. Let t be a term and x a variable. Then $\lambda x. t$ denotes a $\lambda$-expression. For any interpretation I, we define $(\lambda x.t)^I$ as the function f given by $f(v) = t^{I\{x\mapsto v\}}$ for any value v. Moreover, we extend the notation of $\lambda$-expressions to also bind constants. Let c be a constant, then $\lambda c. t$ also denotes a $\lambda$-expression, and its interpretation $(\lambda c.t)^I$ is the function f given by $f(v) = t^{I\{c\mapsto v\}}$ for any value v.

A substitution $\theta$ is a mapping from variables to terms. A substitution $\theta$ is a unifier of two expressions E and $E'$ if $E\theta = E'\theta$; $\theta$ is a most general unifier (mgu) if for every unifier $\eta$ of E and $E'$, there exists a substitution $\mu$ such that $\eta =\theta \mu$. We denote the mgu of E and $E'$ with $\textsf{mgu}(E,E')$.

We work with term algebras [27], in particular with the special classes of the algebraically defined data types of the natural numbers $\mathbb {N}$, lists $\mathbb {L}$, and binary trees $\mathbb{B}\mathbb{T}$.² We denote the sorts of symbols and terms by  :  (colon), e.g., $f : \tau \rightarrow \alpha$ is a function symbol with domain $\tau$ and range $\alpha$. To emphasize the sort $\tau$ of a quantified variable x, we write $\forall x\!\in \!\tau$ or $\exists x\!\in \!\tau$. For a term algebra sort $\tau$, we denote its constructors with $\varSigma _\tau$. We fix an arbitrary ordering on the constructors, and denote the i-th constructor in the order by $c_i$, i.e., $\varSigma _\tau = \{c_1,\dots ,c_{|\varSigma _\tau |}\}$. For each $c_i$, we denote its arity with $n_{c_i}$. We denote with $P_{c_i}$ the set of argument positions of $c_i$ of the sort $\tau$. We only consider the standard models of term algebras. Programs we synthesize may contain terminating recursive functions $f : \tau \rightarrow \alpha$, where $\tau$ is a term algebra type. We define such function f by providing a set of equalities $\{f(c(\overline{x}))\simeq t[\overline{x},f(x_{j_1}),\dots ,f(x_{j_{|P_c|}})]\}_{c\in \varSigma _\tau }$, where $P_c = \{j_1,\dots ,j_{|P_c|}\}$, and t contains no occurrences of f except for the distinguished ones. An example of such a definition is (1).

Fig. 2.

Simplified superposition calculus $\mathbb {S}\text {up}$ .

Saturation and Superposition. Saturation-based proof search implements proving by refutation [16]: validity of F is proved by establishing unsatisfiability of $\lnot F$. Saturation-based first-order theorem provers work with clauses, rather than with arbitrary formulas. To prove a formula F, the provers negate F and further skolemize it and convert it to clausal normal form (CNF). The CNF of $\lnot F$ is denoted by $\textsf{cnf}(\lnot F)$, resulting in a set S of initial clauses. For example, the CNF of the negated and skolemized (SD) is

$$\begin{aligned} \textsf{half}(y)\not \simeq \sigma , \end{aligned}$$

(2)

where $\sigma$ is a fresh constant used for skolemizing x, and y is implicitly universally quantified. Saturation provers saturate S by computing logical consequences of S with respect to a sound inference system $\mathcal {I}$. Whenever the empty clause $\square$ is derived, the set S of clauses is unsatisfiable and F is valid. We may extend the initial set S with additional clauses $C_1,\dots ,C_n$. If C is derived from this extended set, we say C is derived from S under additional assumptions $C_1,\dots ,C_n$.

The superposition calculus $\mathbb {S}\text {up}$  [22] is the most common inference system for first-order logic with equality. Figure 2 shows a simplified version of $\mathbb {S}\text {up}$. The $\mathbb {S}\text {up}$ calculus is sound (if $\square$ is derived from F, then F is unsatisfiable) and refutationally complete (if F is unsatisfiable, then $\square$ can be derived from it).

3 Recent Developments in Saturation

In this section we summarize recent results relevant to our work.

Program Synthesis in Saturation. Synthesizing (non-recursive) programs in saturation has been initiated in [8]. Here, computable and uncomputable symbols in the signature are distinguished. Intuitively, computable symbols are those which are allowed to appear in a synthesized program. An expression is computable if all symbols it contains are computable. A symbol or an expression is uncomputable if it is not computable.

Let $A_1,\dots ,A_n$ be closed formulas. Then

$$\begin{aligned} A_1\wedge \ldots \wedge A_n\rightarrow \forall \overline{x}\exists y. F[\overline{x}, y] \end{aligned}$$

(3)

is a (synthesis) specification with inputs $\overline{x}$ and output y.

Consider a computable term $r[\overline{x}]$ such that $A_1\wedge \ldots \wedge A_n\rightarrow \forall \overline{x}.F[\overline{x}, r[\overline{x}]]$ holds. Such an $r[\overline{x}]$ is called a program for (3) and a witness for y in (3). If $A_1\wedge \ldots \wedge A_n\rightarrow \forall \overline{x}. (F_1\wedge \ldots \wedge F_n \rightarrow F[\overline{x},r[\overline{x}]])$ holds for computable formulas $F_1, \dots , F_n$, then $\langle {r[\overline{x}]}{\bigwedge _{i=1}^n F_i}\rangle$ is a program with conditions $F_1,\dots ,F_n$ for (3).

Saturation-based theorem proving was extended in [8] to a saturation-based program synthesis framework. To this end, the clausified negated specification (3) is extended by an answer literal $\textsf{ans}$:

$$\begin{aligned} A_1\wedge \ldots \wedge A_n\wedge \forall y.(\textsf{cnf}(\lnot F[\overline{\sigma }, y]) \vee \textsf{ans}(y)) \end{aligned}$$

(4)

The set of clauses (4) is then saturated. During saturation, upon deriving a clause $C[\overline{\sigma }]\vee \textsf{ans}(r[\overline{\sigma }])$, where $r[\overline{\sigma }]$ is computable and $C[\overline{\sigma }]$ is computable and does not contain $\textsf{ans}$, the program $\langle {r[\overline{x}]}{\lnot C[\overline{x}]}\rangle$ with conditions for (3) is recorded and the clause is replaced by $C[\overline{\sigma }]$. This step is called answer literal removal within saturation. Once saturation terminates by deriving the empty clause $\square$, the final program for (3) is constructed by composing the relevant recorded programs with conditions in a nested $\textsf{if}\!-\!\textsf{then}\!-\!\textsf{else}$. To support derivation of such clauses $C[\overline{\sigma }]\vee \textsf{ans}(r[\overline{\sigma }])$ and to ensure that answer literals only have computable arguments, the work of [8] extended the superposition calculus $\mathbb {S}\text {up}$ with new inference rules.

Induction in Saturation. Inductive reasoning has been integrated in saturation [5,6,7, 9, 25]. The main idea in this body of work is to apply induction by theory lemma generation: based on already derived formulas, generate a suitable induction axiom and add it to the search space. To this end, the following induction rule is used:

where L[t] is a ground literal, C is a clause, and $F\rightarrow \forall x.L[x]$ is a valid induction axiom. The conclusion of the Ind rule is clausified, yielding $\textsf{cnf}(\lnot F)\vee L[x]$. This clause is resolved with the premise $\overline{L}[t]\vee C$ immediately after applying the Ind rule and the resulting clause $\textsf{cnf}(\lnot F)\vee C$ is added to the search space.

An example of a valid induction schema is the structural induction axiom for natural numbers, where G[x] is any closed formula:

$$\begin{aligned} \big (G[\textsf{0}]\wedge \forall y.(G[y]\rightarrow G[\textsf{s}(y)])\big )\rightarrow \forall x.G[x] \end{aligned}$$

(5)

When we instantiate the schema with $G[x]:=L[x]$, we obtain an axiom that can be used in Ind. Since the rule requires $\overline{L}[t]$ to be ground, this instance of Ind cannot be applied on (2) and thus is not sufficient for proving (SD) of Fig. 1. To prove formulas with a free variable by induction, we extend Ind in Sect. 5.

Note that we can also use a complex formula G[t] in place of the literal L[t] in Ind, obtaining a more involved rule, possibly with multiple premises, similarly to a mutli-clause induction rule [7] or a induction with arbitrary formulas [6].

4 Saturation with Induction in Constructive Logic

We first summarize the key challenges our work resolves towards recursive synthesis in saturation, and then present our synthesis approach in Sects. 5–8.

The idea of extracting programs from proofs originates from results in constructive (intuitionistic) logic, starting with Kleene’s realizability [14]. In constructive logic, provability of a formula $\forall \overline{x} \exists y.F[\overline{x},y]$ implies that there is an algorithm which, given values for $\overline{x}$, outputs a value for y satisfying $F[\overline{x},y]$.

We note that the structural induction axiom (5) over natural numbers has computational content, as follows. The program r for $\forall x. G[x]$ can be built from a program $r_\textsf{0}$ for $G[\textsf{0}]$ and a program $r_\textsf{s}$ for $\forall y. (G[y] \rightarrow G[\textsf{s}(y)])$ as:

$$\begin{aligned} r(\textsf{0}) & \simeq r_\textsf{0}\\ r(\textsf{s}(y)) & \simeq r_\textsf{s}(r(y)) \end{aligned}$$

For this to be useful, we need to first prove $G[\textsf{0}]$, then prove $\forall x.(G[y] \rightarrow G[\textsf{s}(y)])$, and then use the induction axiom to derive $\forall x. G[x]$. Such an approach towards constructing programs does not however work in saturation-based theorem proving, as saturation does not reduce goals to subgoals [2]. Rather, we add the induction axiom as a theory lemma to the proof search and continue saturation, so we do not have proofs of either $G[\textsf{0}]$ or $\forall y. (G[y] \rightarrow G[\textsf{s}(y)])$. Constructing programs during saturation becomes even more complex when using answer literals, because clauses generated during saturation may contain these literals. For example, if we try to extract a proof of $G[\textsf{0}]$, we may find a proof with an answer literal in it.

To capture the constructive nature of induction and address the above challenges of program synthesis in saturation, we use the following trick. We modify the induction axiom so that it indirectly stores information about the programs for $G[\textsf{0}]$ and $\forall y. (G[y] \rightarrow G[\textsf{s}(y)])$. To do this, instead of adding the induction axiom (5), in Sect. 5 we add what we call a magic axiom for (5), where G has an additional argument for storing the program. In Sect. 6 we further convert our magic axioms into formulas to be used to derive recursive programs in saturation.

5 Induction with Magic Formulas

We first present our approach to proving formulas with a free variable by induction. We further extend this approach to synthesis in Sect. 6. While our approach works the same way with arbitrary term algebras, for the sake of clarity we first introduce our work for natural numbers and then for general term algebras in Sect. 8.

We use the following magic axiom:

$$\begin{aligned} \Bigl ( \exists u_\textsf{0}. G[\textsf{0}, u_\textsf{0}] \wedge \forall y . \bigl (\exists w . G[y, w] \rightarrow \exists u_\textsf{s}. G[\textsf{s}(y), u_\textsf{s}] \bigr ) \Bigr ) \rightarrow \forall z .\exists x. G[z, x] \end{aligned}$$

(6)

Note that all magic axioms are valid, as they are instances of the structural induction axiom (5) with the quantified formula $\exists x.G[t,x]$ in place of G[t]. The magicalness of (6) stems from its simple, yet powerful expressiveness: when used in proof search, the variables $u_\textsf{0}, u_\textsf{s}$ in the antecedent capture the programs for the base and step cases, allowing us to construct a program for x in the consequent.

Using axiom (6), we introduce the following variant of the Ind rule:

where the only free variable of L[t, x] is x and C does not contain x.

Example 1

Consider the specification (SD) from Fig. 1. To prove it using superposition, and not yet synthesize the function satisfying (SD) , we use the following magic axiom:

$$\begin{aligned} \Bigl ( \exists u_\textsf{0}. \textsf{half}(u_\textsf{0})\!\simeq \!\textsf{0}\wedge \forall y . \bigl (\exists w . \textsf{half}(w)\!\simeq \! y \rightarrow \exists u_\textsf{s}. \textsf{half}(u_\textsf{s})\!\simeq \!\textsf{s}(y) \bigr ) \Bigr ) \rightarrow \forall z .\exists x. \textsf{half}(x)\!\simeq \! z \end{aligned}$$

(7)

To use (7) in saturation, we clausify it and skolemize the variables y, w, x as $\sigma _y, \sigma _w, \sigma _x(z)$, respectively. The following is a refutational proof of (SD) :

Hence, the magic axiom (6) is sufficient to prove  (SD) . However, (6) does not suffice to synthesize the program for  (SD) from the above proof. Similarly to [8], for synthesis we would use

$$\begin{aligned} \textsf{half}(y)\not \simeq \sigma \vee \textsf{ans}(y) \end{aligned}$$

(8)

instead of clause 1 and obtain a derivation similar to the one above, but with the answer literal $\textsf{ans}(\sigma _x(\sigma ))$. As $\sigma _x$ is a fresh skolem function, it is uncomputable and not allowed in answer literals. Therefore, simply following the approach of [8] fails to synthesize a recursive program from the proof of  (SD) . We address the challenge of program construction for the skolem function $\sigma _x$ in Sect. 6.    $\square$

6 Programs with Primitive Recursion

We now construct recursive programs for proofs using induction over natural numbers (6). As mentioned in Sect. 4, the antecedent of the induction axiom gives us a recipe for constructing the program for the consequent. To capture this dependence of the consequent program x on the antecedent programs $u_\textsf{0}, u_\textsf{s}$, we convert the magic axiom (6) to its equivalent prenex normal form where $\forall u_\textsf{0}, u_\textsf{s}$ precedes $\exists x$:

$$\begin{aligned} \exists y, w.\forall u_\textsf{0}, u_\textsf{s},z.&\exists x. \Big ( \big (G[\textsf{0}, u_\textsf{0}] \wedge (G[y, w] \rightarrow G[\textsf{s}(y), u_\textsf{s}])\big ) \rightarrow G[z, x]\Big ) \end{aligned}$$

(9)

The prenex form (9) of the magic axiom (6) allows us to record the dependency on the programs resulting from the base and step cases of induction. For that, we introduce a recursive operator to be used for constructing programs.

Definition 1

(Primitive Recursion Operator). Let $f_1 : \alpha$, and $f_2 : \mathbb {N}\times \alpha \rightarrow \alpha$. The primitive recursion operator $\textsf{R}$ for natural numbers and $\alpha$ is:

$$\begin{aligned} \textsf{R}(f_1, f_2)(0) &\simeq f_1 \\ \textsf{R}(f_1, f_2)(\textsf{s}(y)) &\simeq f_2(y, \textsf{R}(f_1,f_2)(y)) \end{aligned}$$

Lemma 2

(Recursive Witness). The expression $\textsf{R}(u_\textsf{0}, \lambda y, w. u_\textsf{s})(z)$ is a witness for the variable x in (9).

Lemma 2 ensures that we can construct a program for the consequent of the magic axiom given programs for the base case and the step case. We next integrate this construction into our synthesis framework using answer literals. For that we take a close look at the skolemization of induction axiom (9), and define skolem symbols, denoted via $\textsf{rec}$, for the variable x, capturing the recursive program.

Definition 3

($\textsf{rec}$-Symbols). Consider formulas G[t, x] with a single free variable $x:\alpha$ containing a term $t : \mathbb {N}$. For each such formula we introduce a distinct computable function symbol $\textsf{rec}_{G[t, x]}: \alpha \times \alpha \times \mathbb {N}\rightarrow \alpha$. We will refer to such symbols $\textsf{rec}_{G[t, x]}$ as $\textsf{rec}$-symbols. When the formula G[t, x] is clear from the context or unimportant for the context, we will simply write $\textsf{rec}$ instead of $\textsf{rec}_{G[t, x]}$.

A term with a $\textsf{rec}$-symbol as the top-level functor is called a $\textsf{rec}$-term.

Definition 4

(Magic Formula). The magic formula for G[t, x] is:

$$\begin{aligned} \begin{aligned} &\forall u_\textsf{0}, u_\textsf{s},z. \\ &\qquad \Big ( \big (G[\textsf{0}, u_\textsf{0}] \wedge (G[\sigma _y, \sigma _w] \rightarrow G[\textsf{s}(\sigma _y), u_\textsf{s}])\big ) \rightarrow G[z, \textsf{rec}_{G[t,x]}(u_\textsf{0},u_\textsf{s},z)]\Big ) \end{aligned} \end{aligned}$$

(10)

It is easy to see that magic formula (10) is obtained by skolemizing the prenex normal form of magic axiom (9), where we replace the variables y, w by fresh constants $\sigma _y,\sigma _w$, and the variable x by a fresh $\textsf{rec}_{G[t, x]}$-symbol. The constants $\sigma _y,\sigma _w$ introduced in (10) are said to be associated with the $\textsf{rec}_{G[t, x]}$-term. An occurrence of any skolem constant $\sigma _y, \sigma _w$ is considered computable if it is an occurrence in the second argument of a $\textsf{rec}_{G[t, x]}$-term which it is associated with.

We introduce additional requirements for reasoning with $\textsf{rec}$-terms to ensure that they always represent the recursive function to be synthesized.

Definition 5

($\textsf{rec}$-Compliance). An inference system $\mathcal {I}$ is $\textsf{rec}$-compliant if:

• 1. $\mathcal {I}$ only introduces $\textsf{rec}$-terms in the instances of the magic formula (10),

• 2. $\mathcal {I}$ does not introduce uncomputable symbols into arguments of $\textsf{rec}$-terms in clauses it derives.

Using a $\textsf{rec}$-compliant inference system $\mathcal {I}$, we derive clauses containing $\textsf{rec}$-terms. These terms correspond to functions constructed using the operator $\textsf{R}$.

Definition 6

(Recursive Function Term). Let $\sigma _y, \sigma _w$ be associated with $\textsf{rec}(s_1, s_2, t)$. Then we call the term $\textsf{R}(s_1, \lambda \sigma _y, \sigma _w. s_2)(t)$ the recursive function term corresponding to $\textsf{rec}(s_1,s_2,t)$.

For a term r, we denote by $r^\textsf{R}$ the expression obtained from r by iteratively replacing all $\textsf{rec}$-terms by their corresponding recursive function terms, starting from the innermost ones. Similarly, formula $F^\textsf{R}$ denotes the formula F in which we replace all $\textsf{rec}$-terms by their corresponding recursive function terms.

Lemma 7

(Recursive Witness for Magic Formulas). Consider the formula obtained from (10) by replacing $\textsf{rec}_{G[t, x]}(u_\textsf{0},u_\textsf{s},z)$ by its corresponding recursive function term $\textsf{R}(u_\textsf{0},\lambda \sigma _y,\sigma _w.u_\textsf{s})(z)$:

$$\begin{aligned} \begin{aligned} &\forall u_\textsf{0}, u_\textsf{s},z. \\ &\quad \Big ( \big (G[\textsf{0}, u_\textsf{0}] \wedge (G[\sigma _y, \sigma _w] \rightarrow G[\textsf{s}(\sigma _y), u_\textsf{s}])\big ) \rightarrow G[z, \textsf{R}(u_\textsf{0},\lambda \sigma _y,\sigma _w.u_\textsf{s})(z)]\Big ) \end{aligned} \end{aligned}$$

(11)

For every interpretation I, there exists a mapping of skolem constants to values $\{\sigma _y\mapsto v_y, \sigma _w\mapsto v_w\}$ such that I extended by this mapping is a model of (11). As a consequence, formula (11) is satisfiable.

Lemma 7 implies that we can use formula (11) instead of (10) in derivation, while preserving the soundness of the derivations. Soundness of our approach to recursive program synthesis is given next.

Theorem 8

(Semantics of Clauses with Answer Literals and $\textsf{rec}$-terms). Let $C_1, \dots , C_m$ be clauses and F a formula containing no answer literals and no $\textsf{rec}$-symbols. Let C be a clause containing no answer literals. Let $M_1,\dots ,M_l$ be magic formulas. Assume that using a sound $\textsf{rec}$-compliant inference system $\mathcal {I}$, we derive $C\vee \textsf{ans}(r[\overline{\sigma }])$, where $r[\overline{\sigma }]$ is computable, from the set of clauses

$$\begin{aligned} \{\ C_1,\dots ,C_m,\ M_1,\dots ,M_l,\ \textsf{cnf}(\lnot F[\overline{\sigma }, y]\vee \textsf{ans}(y))\ \}. \end{aligned}$$

Then

$$M_1^\textsf{R},\dots ,M_l^\textsf{R},C_1,\dots ,C_m\vdash C^\textsf{R}, F[\overline{\sigma }, r^\textsf{R}[\overline{\sigma }] ].$$

That is, under the assumptions $M_1^\textsf{R},\dots ,M_l^\textsf{R}, C_1, \ldots , C_m, \lnot C^\textsf{R}$, the computable expression $r^\textsf{R}[\overline{x}]$ is a witness for y in $\forall \overline{x}\exists y.F[\overline{x},y]$.

Based on Theorem 8, if the CNF of $A_1,\dots ,A_n$ is among $C_1,\dots ,C_m$, then $r^\textsf{R}[\overline{x}]$ is a witness for y in (3) under the assumptions $M_1^\textsf{R},\dots ,M_l^\textsf{R}, C_1, \ldots , C_m, \lnot C^\textsf{R}$. The following ensures that we can construct recursive programs with conditions.

Theorem 9

(Recursive Programs). Let $r[\overline{\sigma }]$ be a computable term, and $C[\overline{\sigma }], C_1[\overline{\sigma }],\dots ,C_m[\overline{\sigma }]$ be ground computable clauses containing no answer literals and no $\textsf{rec}$-symbols. Assume that using a sound $\textsf{rec}$-compliant inference system $\mathcal {I}$, we derive the clause $C[\overline{\sigma }]\vee \textsf{ans}(r[\overline{\sigma }])$ from the CNF of

$$\begin{aligned} \{\ A_1, \dots , A_n,\ C_1[\overline{\sigma }],\dots ,C_m[\overline{\sigma }],\ M_1,\dots ,M_l,\ \lnot F[\overline{\sigma }, y]\vee \textsf{ans}(y)\ \} \end{aligned}$$

where $M_1,\dots ,M_l$ are magic formulas. Then,

$$\begin{aligned} \langle {r^\textsf{R}[\overline{x}]}{\bigwedge _{j=1}^{m}C_j[\overline{x}]\wedge \lnot C[\overline{x}]}\rangle \end{aligned}$$

is a program with conditions for (3).

From Theorem 9 we obtain the following key result on program synthesis.

Theorem 10

(Recursive Program Synthesis). Let $P_1[\overline{x}],\dots , P_k[\overline{x}]$, where $P_i[\overline{x}] = \langle {r_i^\textsf{R}[\overline{x}]}{\bigwedge _{j=1}^{i-1}C_j[\overline{x}]\wedge \lnot C_i[\overline{x}]}\rangle$, be programs with conditions for (3), such that $\bigwedge _{i=1}^n A_i\wedge \bigwedge _{i=1}^k C_i[\overline{x}]$ is unsatisfiable. Then the program $P[\overline{x}]$ defined as

$$\begin{aligned} \begin{aligned} P[\overline{x}] :=\ {} &\textsf{if}\ \lnot C_1[\overline{x}]\ \textsf{then}\ r_1^\textsf{R}[\overline{x}] \\ &\textsf{else}\ \textsf{if}\ \lnot C_2[\overline{x}]\ \textsf{then}\ r_2^\textsf{R}[\overline{x}] \\ &\qquad \dots \\ &\textsf{else}\ \textsf{if}\ \lnot C_{k-1}[\overline{x}]\ \textsf{then}\ r_{k-1}^\textsf{R}[\overline{x}] \\ &\textsf{else}\ r_k^\textsf{R}[\overline{x}], \end{aligned} \end{aligned}$$

is a program for (3).

7 Recursive Synthesis in Saturation

This section integrates the proving and synthesis steps of Sects. 5–6 into saturation. The crux of our approach is that instead of adding standard induction formulas to the search space, we add magic formulas.

Theorems 9–10 imply that to derive recursive programs, we can use any $\textsf{rec}$-compliant calculus, as long as the calculus supports derivation of clauses $C\vee \textsf{ans}(r)$, where r is computable and C is ground, computable, and contains no $\textsf{rec}$-terms nor answer literals. In our work we rely on the extended $\mathbb {S}\text {up}$ calculus of [8], which we (i) further extend by adding magic formulas alongside standard induction formulas, (ii) make $\textsf{rec}$-compliant by disallowing inferences containing uncomputable $\textsf{rec}$-terms, and (iii) extend by adding more complex rules for introducing conditions into $\textsf{rec}$-terms³. We illustrate these steps by our running example.

Example 2

Using the extended $\mathbb {S}\text {up}$ calculus, we synthesize the program for the specification of Fig. 1. With the magic formula corresponding to  (7) ,

$$\begin{aligned} \begin{aligned} &\forall u_\textsf{0}, u_\textsf{s}, z.\\ &\;\;\Bigl (\bigl (\textsf{half}(u_\textsf{0})\!\simeq \!\textsf{0}\wedge (\textsf{half}(\sigma _w)\!\simeq \! \sigma _y \rightarrow \ \textsf{half}(u_\textsf{s})\!\simeq \!\textsf{s}(\sigma _y)) \bigr ) \rightarrow \textsf{half}(\textsf{rec}(u_0,u_\textsf{s},z))\!\simeq \! z\Bigr ), \end{aligned} \end{aligned}$$

(12)

we obtain the following derivation⁴:

The program recorded in step 10 of the proof is $\textsf{rec}(\textsf{s}(\textsf{0}),\textsf{s}(\textsf{s}(\sigma _w)),x)^\textsf{R}= \textsf{R}(\textsf{s}(\textsf{0}), \lambda \sigma _w. \textsf{s}(\textsf{s}(\sigma _w)))(x) = f(x)$, where f is defined as:

$$\begin{aligned} \begin{aligned} f(\textsf{0}) &\simeq \textsf{s}(\textsf{0}) \\ f(\textsf{s}(n)) &\simeq \textsf{s}(\textsf{s}(f(n))) \end{aligned} \end{aligned}$$

Note that while the synthesized program satisfies the specification  (SD) , it does not match the expected definition of the $\textsf{double}$ function from (1). Since the $\textsf{half}$ function is rounding down, and the specification does not require the synthesized function to produce even results, the base case was resolved in step 9 with  (H2) , leading to $f(\textsf{0})\simeq \textsf{s}(\textsf{0})$. As a result, we have $f(n) = \textsf{s}(\textsf{double}(n))$ for any n.    $\square$

Example 2 demonstrates that specification  (SD) has multiple solutions and saturation can find a solution different from the intended one. In the next example we modify the specification to have a single solution and synthesize it.

Example 3

To synthesize the $\textsf{double}$ function, we modify the specification:

After negating and skolemizing (SD’) and adding the answer literal, we obtain:

$$\begin{aligned} \textsf{half}(y)\not \simeq \sigma \vee \lnot \textsf{even}(y) \vee \textsf{ans}(y) \end{aligned}$$

(13)

In this case we use the magic axiom for the conjunction $G[t, x] := \textsf{half}(x)\simeq t \wedge \textsf{even}(x)$:

$$\begin{aligned} \begin{aligned} &\Big (\exists u_\textsf{0}. (\textsf{half}(u_\textsf{0})\simeq \textsf{0}\wedge \textsf{even}(u_\textsf{0})) \wedge \\ &\qquad \forall y.\big (\exists w. (\textsf{half}(w)\simeq y\wedge \textsf{even}(w)) \rightarrow \exists u_\textsf{s}. (\textsf{half}(u_\textsf{s})\simeq \textsf{s}(y)\wedge \textsf{even}(u_\textsf{s}))\big )\Big )\\ &\quad \rightarrow \forall z.\exists x.(\textsf{half}(x)\simeq z\wedge \textsf{even}(x)) \end{aligned} \end{aligned}$$

(14)

We clausify the magic formula corresponding to (14), and further resolve it with the premise (13) to obtain:

$$\begin{aligned}\begin{gathered} \textsf{half}(u_\textsf{0})\not \simeq \textsf{0}\vee \lnot \textsf{even}(u_\textsf{0})\vee \textsf{half}(\sigma _w)\simeq \sigma _y\vee \textsf{ans}(\textsf{rec}(u_\textsf{0},u_\textsf{s},\sigma ))\\ \textsf{half}(u_\textsf{0})\not \simeq \textsf{0}\vee \lnot \textsf{even}(u_\textsf{0})\vee \textsf{even}(\sigma _w)\vee \textsf{ans}(\textsf{rec}(u_\textsf{0},u_\textsf{s},\sigma ))\\ \textsf{half}(u_\textsf{0})\!\not \simeq \!\textsf{0}\vee \lnot \textsf{even}(u_\textsf{0})\vee \textsf{half}(u_\textsf{s})\!\not \simeq \!\textsf{s}(\sigma _y)\vee \lnot \textsf{even}(u_\textsf{s})\vee \textsf{ans}(\textsf{rec}(u_\textsf{0},u_\textsf{s},\sigma )) \end{gathered}\end{aligned}$$

The refutation of these clauses follows a similar course to the proof in Example 2. However, $u_\textsf{0}$ occurring in the literal $\lnot \textsf{even}(u_\textsf{0})$ forces the proof to use  (H1) instead of  (H2) , and thus the final derived answer literal will be $\textsf{rec}(\textsf{0},\textsf{s}(\textsf{s}(\sigma _w)),\sigma )$, corresponding exactly to the function definition of $\textsf{double}$ from (1). Note that a derivation of this program in this case requires a saturation prover to apply induction on conjunctions of literals.   $\square$

8 Generalization to Arbitrary Term Algebras

Our approach from Sects. 5– 7 generalizes naturally to arbitrary term algebras. This section summarizes the key parts of this generalization.⁵

Let $\tau$ be a (possibly polymorphic) term algebra with constructors $\{c_1,\dots ,c_n\}$, where we denote the sort of each $c_i$ by $\tau _{i,1}\times \dots \times \tau _{i,n_{c_i}}\rightarrow \tau$, and $P_{c_i} = \{j_1, \dots , j_{|P_{c_i}|}\}$ for each $i=1,\dots ,n$. Let $\alpha$ be any sort. The magic axiom for G[t, x], where $t :\tau , x : \alpha$, is:

$$\begin{aligned} \biggl ( \bigwedge _{c \in \varSigma _{\tau }} \forall _{i = 1}^{n_c} y_{c,i} . \bigl ( (\bigwedge _{j \in P_c} \exists w_{c,j}. G[y_{c,j}, w_{c,j}]) \rightarrow \exists u_c . G[c(\overline{y_c}), u_c] \bigr ) \biggr ) \rightarrow \forall z .\exists x. G[z, x] \end{aligned}$$

(15)

The corresponding magic formula uses the skolem function $\textsf{rec}_{G[t, x]} : \alpha ^{n_c}\times \tau \rightarrow \alpha$:

$$\begin{aligned} \forall _{c\in \varSigma _\tau } u_c. \forall z. \Big ( \bigwedge _{c \in \varSigma _{\tau }} \bigl ( \bigwedge _{j \in P_c} G[\sigma _{y_{c,j}}, \sigma _{w_{c,j}}] \rightarrow G[c(\overline{\sigma _{y_c}}), u_c] \bigr ) \rightarrow G[z, \textsf{rec}_{G[t, x]}(\overline{u},z)]\Big ) \end{aligned}$$

(16)

Note that each $\sigma _{y_{c_i,j}}, \sigma _{w_{c_i,j}}$ introduced in (16) is considered computable only in the ith argument of its associated $\textsf{rec}$-term. We define the recursion operator $\textsf{R}$ for $\tau$ and $\alpha$ analogously to Definition 1:

$$\begin{aligned}\begin{gathered} \textsf{R}(f_1,\ldots ,f_n)(c_1(\overline{x}))\ \simeq \ f_1(x_1,\ldots ,x_{n_{c_1}}\!, \textsf{R}(f_1,\ldots ,f_n)(x_{j_1}\!), \ldots , \textsf{R}(f_1,\ldots ,f_n)(x_{j_{|P_{c_1}\!|}})) \\ \cdots \\ \textsf{R}(f_1,\ldots ,f_n)(c_n(\overline{x}))\ \simeq \ f_n(x_1,\ldots ,x_{n_{c_n}}\!, \textsf{R}(f_1,\ldots ,f_n)(x_{j_1}\!), \ldots , \textsf{R}(f_1,\ldots ,f_n)(x_{j_{|P_{c_n}\!|}})) \end{gathered}\end{aligned}$$

where for each i we have $f_i : \tau _{i,1}\times \dots \times \tau _{i,n_{c_i}}\times \alpha ^{|P_{c_i}|}\rightarrow \alpha$. Using $\textsf{R}$, we state an analogue of Lemma 7:

Lemma 11

(Recursive Witness for Magic Formulas Using $\tau$). Consider the formula obtained from (16) by replacing $\textsf{rec}_{G[t, x]}(\overline{u},z)$ by its corresponding recursive function term:

$$\begin{aligned} \begin{aligned} &\forall _{c\in \varSigma _\tau } u_c. \forall z. \Big ( \bigwedge _{c \in \varSigma _{\tau }} \bigl ( \bigwedge _{j \in P_c} G[\sigma _{y_{c,j}}, \sigma _{w_{c,j}}] \rightarrow G[c(\overline{\sigma _{y_c}}), u_c] \bigr ) \\ &\ \rightarrow G[z, \textsf{R}(\lambda _{i=1}^{n_{c_1}} \sigma _{y_{c_1\!,i}}. \lambda _{k\in P_{c_1}}\! \sigma _{w_{c_1\!,k}}.\, u_{c_1},\ \ldots ,\ \lambda _{i=1}^{n_{c_n}} \sigma _{y_{c_n\!,i}}. \lambda _{k\in P_{c_n}}\! \sigma _{w_{c_n\!,k}}.\, u_{c_n})(z)]\Big ) \end{aligned} \end{aligned}$$

(17)

For every interpretation, there exists its extension by some $\{\sigma _{y_{c,i}}\!\mapsto \! v_{y,c,i}, \sigma _{w_{c,k}}\!\mapsto v_{w,c,k}\}_{c\in \varSigma _\tau ,i\in \{1,\dots ,n_c\},k\in P_c}$ such that the extension is a model of (17). As a consequence, formula (17) is satisfiable.

Using Lemma 11, we derive the analogues of Theorems 8–10 for an arbitrary term algebra $\tau$. We then employ magic formulas (16) in MagInd when in the premise $L[t, x]\vee C\vee \textsf{ans}(r[x])$ we have $t:\tau$. We finally note that our synthesis method generalizes also to sorts other than term algebras, as long as the induction axiom used for the sort carries the constructive meaning described in Sect. 4.

9 Implementation and Examples

Implementation. We extended the first-order theorem prover Vampire  [16] with a proof-of-concept implementation of our method for recursive program synthesis in saturation. Our implementation consists of approximately 1,100 lines of C++ code and is available online at https://github.com/vprover/vampire/tree/synthesis-recursive.

We implemented the MagInd rule as well as a version of MagInd using a magic axiom with base case $\textsf{s}(\textsf{0})$ for natural numbers and $\textsf{cons}(a,\textsf{nil})$ for any a for lists. To support synthesis requiring induction on specifications $\lnot F[t,x]$, where F[t, x] is an arbitrary formula with the only free variable x, we use an encoding as follows. We change the specification $\forall \overline{x}\exists y.F[\overline{x},y]$ to $\forall \overline{x}\exists y.p(\overline{x},y)$, where p is a fresh uncomputable predicate, and we add an axiom $\forall \overline{x}, y. (p(\overline{x}, y) \leftrightarrow F[\overline{x}, y])$.

Table 1. Synthesis examples using natural numbers $\mathbb {N}$, lists $\mathbb {L}$ and binary trees $\mathbb{B}\mathbb{T}$. The x-variables in the program and synthesized definitions are the inputs. While our framework synthesizes all these examples, our implementation in Vampire only synthesizes those marked with “✓”. Note that for “Length of 2 concatenated lists” we consider $\texttt {+\!+}$ to be uncomputable.

Examples. Our implementation can synthesize the programs for the specifications  (SD) and (SD’). We also synthesize further examples over the term algebras⁶ of natural numbers $\mathbb {N}$, lists $\mathbb {L}$, and binary trees $\mathbb{B}\mathbb{T}$. We display the specifications alongside the programs synthesized by our framework in Table 1. Our framework synthesizes programs for each of the examples⁷ , yet our implementation supports so far only a limited set of magic formulas; therefore, the “Vampire ” column of Table 1 lists which examples are solved in practice.

Experimental Comparison. To the best of our knowledge, no other approach in program synthesis supports the setting we consider: functional relational specifications of recursive programs, given in full first-order logic, without user-defined templates. For this reason, we could not compare the practical aspects of our work with other techniques, but overview related works in Sect. 10. In particular, we note that the tools surveyed in overview in Sect. 10 support a more restrictive/decidable logic than the the full first-order setting exploited in our approach. As such, the benchmarks of Table 1 cannot be translated into the input languages of techniques surveyed in Sect. 10.

10 Related Work

Our approach is conceptually different from existing methods in recursive program synthesis, as we are not restricted to decidable logical fragments, nor to user-defined program templates. Our work supports program specifications in full first-order logic (with theories) and does not require syntactic templates for the programs to be synthesized. In the sequel, we only discuss related approaches that support full automation in program synthesis, without templates or user guidance.

We extend the recursion-free synthesis framework of [8], while exploiting ideas from deductive synthesis [17, 20, 29] using answer literals [4]. We bring recursive program synthesis into the landscape of saturation-based proving and construct programs from saturation proofs with magic axioms. Unlike our setting, the works of [19, 29] construct recursive programs from proofs by induction, by reducing the program specification to subgoals corresponding to the cases of the induction axiom. Modern first-order theorem provers mostly implement saturation-based proof search, which however does not support a goal-subgoal architecture. Our approach integrates induction directly into saturation and enables automated reasoning with term algebras.

Fully automated methods supporting recursive program synthesis include Synquid  [23], Leon  [15],  Jennisys  [18], SuSLik  [24], Cypress  [12], Burst  [21], and Syntrec  [11]. Except for Burst and Syntrec, all these works decompose goals into subgoals. Our work complements these methods, by turning saturation into a recursive synthesis framework over first-order theories. As such, our work also differs from Synquid, where term enumeration combined with type checking is used over program specifications within decidable logics. Leon uses recursive schemas corresponding to our recursive operator $\textsf{R}$, instantiates them by candidate program terms, and checks if they satisfy the specification. Unlike Leon, we support a complete handling of quantifiers via superposition reasoning. Jennisys uses a verifier to generate input-output examples, which differs from our setting of using inductive formulas as logical specifications. Burst generates programs by composition from existing ones, using quantifier-free fragments of first-order logic. Contrarily to this, we support full first-order logic and induction, without using subgoal proof strategies. Finally, we note that Syntrec guarantees bounded/relative correctness of the synthesized programs (using syntactic program templates), while our approach proves correctness of the synthesized program without further restrictions.

The syntax-guided synthesis (SyGuS) framework [1] supports specifications for recursive functions and can encode our examples from Sect. 9. However, to the best of our knowledge, SyGuS methods, including the SMT-based approach of [26], do not support recursive synthesis. While the semantics-guided synthesis framework [13] also supports recursive functions, its (to the best of our knowledge) only solvers Messy  [13] and Messy-Enum  [3] synthesize programs from input-output examples and using grammars, respectively, rather than purely from logical specifications.

11 Conclusions

We extend saturation-based framework to recursive program synthesis by utilizing the constructive nature of induction axioms. We introduce magic axioms as a tracking mechanism and seamlessly integrate these axioms into saturation. We then construct correct recursive programs using answer literals in saturation, as also demonstrated by our proof-of-concept implementation. Extending our work with tailored handling of (more general) magic axioms, and respective superposition inferences, is an interesting line for future work. Devising and implementing further, and potentially more general, synthesis rules and induction schemes is another task for future research, allowing us to further strengthen the practical use of our work.