摘要
本文提出了一種程序合成算法，用於解決處理代數數據類型的遞歸函數的合成問題。該算法建立在證明論的基礎上，在合成過程中利用類型信息和輸入輸出示例對搜索空間進行修剪；同時，該算法還引入了一種名為精簡樹的數據結構。利用這一數據結構，算法可以為目標代碼所需的約束條件構建出簡明的表達形式。為了評估算法，作者對算法進行了原型實現，本文采用的數據集由 40 多個較小的基準程序、若干較大的複雜程序組成。實驗結果表明：該算法的時間開銷與合成結果規模已經達到甚至超過了當前的最新技術水平。
關鍵詞
函數式編程；程序合成；類型理論；證明搜索
1 引言
本文提出了一種用於合成處理代數數據類型的、具有純粹函數性質的遞歸程序的技術。作者團隊的方法改進了“程序合成是一種證明搜索”（Proof Search）的古老觀念：除使用類型信息外，算法還使用具體的輸入輸出示例對搜索空間進行縮減，並獲得了十分顯著的縮減效果。作者將這些額外的信息（輸入輸出示例）利用於構建一種名為精簡樹的數據結構，並通過這種數據結構有效地對非平凡（規模較大）的程序進行了合成。
圖 1：一個程序合成問題示例（上）和合成結果實現（下）
圖 1 的小例子簡單地展示了程序合成的過程。算法的原型採用 OCaml 語法實現，但注意該算法並不僅侷限於這一種語法。算法的輸入包括：類型簽名、關於必要輔助函數的定義以及合成目標。圖 1 所示的過程定義了 nat（自然數）和 list 兩種類型，同時沒有輔助函數。合成目標則是一個名為 stutter、映射類型為 list->list 的函數。該函數的一部分由緊隨“|>”標記後的一系列輸入輸出示例指定。這些示例用於進一步完善目標類型，比如圖 1 中的示例表明了 stutter 函數應該返回一個列表，並且這個列表應該由輸入的列表中的每個元素重複一次組成。如第三個示例所示：stutter [1;0]對應的輸出為[1;1;0;0]。
本文提出的合成算法可以在很短的時間（約 0.001s）內產生合成結果。stutter 函數的合成結果如圖 1 的下半部分所示。可以看到：算法將合成一個完備的函數。該函數在輸入列表中為每個 Cons 單元創建了兩個副本，並通過遞歸傳遞 f1 l2 實現了函數的“結巴功能”（stuttering）。
這種具有通用性的程序合成技術擁有許多潛在的應用場景，例如：利用程序示例編寫電子表格宏、在大型 API 庫語境下完成代碼補全、生成緩存一致性協議等。本文主要關注類型化編程語言中涉及結構化數據類型的遞歸程序，以及高階程序的合成問題。這個領域上是對上述研究領域的補充。
將示例與類型相結合：作為一種基於證明搜索的技術，編程語言的類型結構是本文提出的算法避免產生不良類型項的關鍵參照。同時，在合成過程中，該算法只在解空間中對 β-normal 和 η-long 形式的程序進行搜索。
關於如何將示例輸入輸出與類型信息相結合，作者的意見是採用“修改鍵入規則”的方式。採用這種方式，算法可以將示例“推入”派生樹的葉子節點，從而使派生樹可以充當生成程序的框架。這樣做可以使算法在搜索過程的早期就對候選項進行評估，從而才有可能大幅度縮減搜索空間。本文提出的算法沒有遵循“先枚舉再評估”的樸素策略，而是採用了更為細緻的“在枚舉時評估”的方式。
路線圖：本文引入了一種類似機器學習模式的類型系統。該系統通過結合輸入輸出示例對合法程序派生集進行約束。類型系統可以看成程序合成問題的非確定性規範，其最終的目的是找到具有有效類型的項。為了將規則轉化成算法，作者將類型系統劃分為兩個部分：1）一種名為精簡樹的數據結構，用於協助驗證搜索空間中眾多候選解的重疊部分；2）一種枚舉搜索方法，用於實現解的搜索。作者團隊將算法實現為一個原型工具：MYTH。該工具採用 OCaml 語法進行代碼合成算法的設計，在合成效率和合成規模方面均比肩甚至超過現有的技術水平。
2 技術概覽
假設現在有三種數據：一種具有代數數據特徵的數據類型 match、一些頂級函數定義和幾個顯式遞歸函數，一個程序合成問題可以通過：（1）一些數據類型定義和頂級 let-綁定（let-binding）,（2）一個目標類型以及（3）一些目標類型的示例來定義。一個程序合成任務就是生成與示例一致且符合目標類型的程序。
面向類型的程序合成過程主要包括兩個部分：1）基於目標類型，使用給定的輸入輸出示例對約束進行完善；2）推測出與給定示例結果一致的目標類型值。
類型細化：以圖 1 中 stutter 函數的合成過程為例。首先，從目標類型 list->list 我們得知：生成程序的頂層結構必須採用“let rec f1 (l1:list) : list = ?”的形式；之後，在合成 stutter 函數主體的過程中，三個輸入輸出示例告訴我們：在 l1（輸入）為[ ]的“設定”（stutter 函數的假設評估）下，函數的期望輸出為[ ]；而在 l1 為[0]的設定下，期望輸出為[0; 0]；最後在 l1 為[1; 0]的設定下，期望輸出為[1; 1; 0; 0]。在合成主體時，三個示例輸入輸出會分別精煉為一個新的示例設定。這個示例設定保證輸出值是目標類型，並且與對應的輸入值綁定。
推測：現在要使用 list 類型對函數主體進行填充。通過觀察我們可知：沒有一個單獨的 list 構造函數可以同時滿足這些示例（因為有一些示例同時以 Nil 和 Cons 開頭）。解決這一點，可以嘗試枚舉或者推測一些包含變量的良好類型術語，例如 l1。但 l1 並不能同時滿足所有示例，比如在 l1 為[0]的設定下修改 l1 為[0; 0]之後，其他的項可能是良好類型，也有可能是不良類型，但是都不滿足結構性遞歸的條件。這個時候，類型推測就會失敗。
注意：除了一些不良類型項和非結構性遞歸項之外，一些良好類型項也需要被排除。例如良好類型項 “match Nil with Nil -> e1 | Const -> e2”，它與不含 match 的較小項（在本例中為 e2）等效，作者稱之為“與常量構造函數相匹配的項”。這種項通常也需要排除在外。由於引入了額外的 lambda 表達式和應用，這類不好的項被大量引入。為了避免產生這種無效的冗餘項，推測階段只能生成無法進一步約簡的、β-normal 形式的項。
匹配細化：這部分引入 match 表達式。作者首先推測 match 的可能匹配項：這種項必須具有一些代數類型，並且必須由上下文中的變量構造而來。唯一滿足這些條件的項就是 l1，則接下來考慮如何完成項：
當匹配到模板時，作者根據 match 在每個設定下的配股結果分配示例。這種情況下：l1 在第一個設定下的評估結果為 Nil，在其餘兩個設定下的評估結果為 Cons(_, _)。由此，可以將第一個示例發送到 Nil 分支，將其他兩個示例發送到 Cons 分支。如此在下一階段中，可以通過細化的設定解決 Nil 和 Cons 兩個子目標類型。Nil 分支可以立刻解決：通過符合示例設定“[]”的 l1 表達式可以完成關於 Nil 的匹配細化。
遞歸函數：解決 Cons 分支則需要進行新一輪的推測，同時解決方案中需要對 f1 進行遞歸調用。那麼面對這種基於類型和示例的方法，應當如何生成遞歸函數呢？答案是：在引入 f1 這種遞歸函數時，可以將對應這種函數的輸入輸出示例解釋為函數的一部分，從而對 f1 的功能進行合理近似。在這裡，f1 的實例就是給出的三個示例設定定義的分部函數。在給定上下文中該類信息的情況下，推測過程可以很快的確定“Cons(n1, Cons(n1, f1 l2))”就是 Cons 分支的一種匹配情況。
3 實現
3.1 系統的一致性、終止點以及確定性
一致性：由於作者允許在分部函數的域中應用函數值，合成過程中系統無法確定是否存在互相矛盾的示例集（即作者的系統無法確定函數是否等價）。因此在 MYTH 中，無法提前對輸入的 X 進行一致性檢測。
MYTH 採用了“按照程序大小粗粒度增長”的順序，對程序空間進行搜索。這解決了上一段中提到的問題。給定一組一致性示例，MYTH 的解空間中一定存在一個可以滿足所有示例的程序。這個程序將專門用於對示例（例如一組嵌套的模式匹配項）的精確處理。
終止點：為了達到終止點，系統必須在遞歸函數調用過程中不斷添加結構性遞歸檢查，同時對數據類型施加正向限制。結構性遞歸檢查是 Coq 定理證明器（Coq Theorem Prover）語法檢查部分的一種更簡單、更粗粒度的形式。如圖 2 所示，作者給出的函數都是僅接收一個參數的柯里函數（Curried Function），這要求傳遞給 fix 的參數都是結構性遞減的。這種結構性遞減的值只能通過對 fix 的原始參數進行模式匹配獲取，這種形式較 Coq 來說更為嚴格。
作者的策略是對僅搜索所有與示例一致的、具有目標類型特徵的可能解。這種搜索可能是無止境的，尤其是當用戶沒有提供足夠的示例時，這種情況就更易發生。因此，作者使用由受項大小影響的迭代加深策略對這個過程進行控制。比如當用戶嘗試合成一個規模為 1 的有效程序，但關於解的搜索卻失敗了的時候，系統將增加規模大小以進行下一輪搜索。該過程將持續到搜索成功（找到滿足要求的程序）或規模達到用戶規定的上限為止。
3.2 精簡樹
圖 3：stutter 函數的精簡樹
圖 3 給出了一個精簡樹示例，該精簡樹對應圖 1 中 stutter 方法的合成過程。如圖 3 所示精簡樹的節點分為兩種：
（1）目標節點：目標節點包含目標類型，並代表了程序合成過程中可以進行 E-guess 的位置。目標節點對生成的內容進行包裝，例如圖 3 最高處包含 list->list 的節點，就是一個目標節點。
（2）精簡節點：精簡節點代表有效地 I-refinement，這些節點將取消對生成內容的包裝。例如圖 3 中包含 match l1 的節點，就是一個精簡節點，代表 l1 上的一個 match 操作。
4 結果分析
遞歸函數合成領域已經出現了眾多優秀的研究成果，其中最著名的是 Escher 和 Leon。在本研究中，作者團隊使用的數據集與這兩項工作十分類似，具有相似的程序複雜性（數據集中的程序平均包含 15~30 個 AST 節點）。在這種情況下，MYTH 通常具有與這兩項工具相近或是更優的執行效率。MYTH 對大部分程序的合成時間可忽略不計，僅在合成某些規模較大的程序時耗時稍長，但都在可以接受的範圍內。
致謝
國家重點研發計劃課題：基於協同編程現場的智能實時質量提升方法與技術（2018YFB1003901）和國家自然科學基金項目：基於可理解信息融合的人機協同移動應用測試研究（61802171）
本文由南京大學軟件學院 2020 級碩士錢瑞祥轉述
閱讀更多 慕測科技 的文章
