2020-11-18

Datalog に入門する

Datalog Souffle

とある論文がデータのスキーマ変換を行うために Datalog を用いていた。Prolog は触ったことあるし、Datalog って言葉も聞いたことはあったが、具体的にどんな言語で何が嬉しいのか知らなかったのでちょっと調べてみた。
ついでに Datalog のインプリタとして Soufflé という処理系も触ってみた。

Datalog とは

Datalog は、論理型プログラミング言語である Prolog のサブセットであり、主に演繹データベースのクエリ言語として用いられる。クエリは論理的な制約として記述され、その制約を満たすデータをデータベースから抽出する。最近では Datomic のような分散データベースのクエリ言語としても用いられている。
Datalog として標準化された言語が言語仕様があるわけではなく、処理系によって構文が異なっていたり、独自の拡張がされていたりする。たとえば、集約関数をサポートするものなどがある。
一般に Datalog の表現力は Prolog より制限されたものであり、チューリング完全ではない。この制限がクエリの効率的な実行（推論）を実現している。また、Datalog は完全に宣言的な言語であるといえる。つまり、記述された命令の順序に意味はない。
Datalog を用いたクエリは first-order logic を用いて記述される。また、Datalog のプログラムを構成する要素として extensional predicate (事実の集合、facts と呼ばれる) と intensional predicate (事実から事実を導くルール, rules と呼ばれる) がある。
- たとえば、データベースの中身は facts であり、抽出したいデータの集合も facts である。このときクエリは rules として記述され、データベースの facts から抽出したいデータの fatcs を導出するものであるといえる。

Datalog - Wikipedia

ここまでのメモ。

facts から facts へ変換するルールを rules として記述するだけなので、データベースへの問い合わせだけでなく、異なるスキーマをもつデータ間の変換の操作を Datalog を用いて表現できる。これが Datalog がさまざまなドメインで利用されている背景と言えそう。

Soufflé とは

Datalog の雰囲気が分かったところで、具体的な処理系である Soufflé を触ってみる。公式サイトは以下。

Soufflé は、もともとは Oracle Labs でプログラムの静的解析用に開発されたツールであるが、今ではデータ分析などさまざまな領域において利用されている。ソースコードは Github 上で公開されており、2020年現在もメンテナンスが行われている。ひとつの特徴として、Datalog プログラムを C++ へのトランスパイルが可能であることが挙げられる。これによって、マルチコアなど最新の計算資源を活用したプログラムを書けるのが強みである。

Soufflé のインストール

インストール手順は公式ページにある通り。

Install Soufflé | Soufflé • A Datalog Synthesis Tool for Static Analysis

使っている OS が Ubuntu 20.04.1 LTS (Focal Fossa) なので、apt のためのリポジトリの指定時に bionic の代わりに focal を指定した。

Datalog プログラムの例

以下の公式ページに載っている Datalog プログラムの例を見てみる。
なお本記事に記載するすべてのソースコードは公式ページからの引用である。

Examples | Soufflé • A Datalog Synthesis Tool for Static Analysis

今回のプログラムは、手続き型言語のポインタ解析を行うシンプルな例である。具体的には、変数のフィールドやエイリアスは考慮するが、制御フローは考慮していない。ちゃんと言うと field-sensitive かつ flow-insensitive な Points-to analysis になっている。

ソースコードを上から順に見てゆく。
今回の解析対象の手続き型のプログラムの構造は以下である。

// Encoded code fragment:
//
//  v1 = h1();
//  v2 = h2();
//  v1 = v2;
//  v3 = h3();
//  v1.f = v3;
//  v4 = v1.f;
//

変数として v1, v2, v3, v4 の4つ、オブジェクトとして h1, h2, h3 の3つがある。このポインタ解析では各変数が指しうるオブジェクトの集合を求める。答えから言ってしまうと、今回のポインタ解析では変数 v1 はオブジェクト h1 または h2 を指し、v2 は h2, v3 は h3, v4 は h3 を指しうる、という結果になる。
ちなみに、本当は変数 v1 は h2 しか指さないのだが、制御フローを考慮していないので、h1 を指しうると誤検知している。静的解析は安全側に倒す（つまり真の解より広めの範囲を返す）のが一般的であるためこういうことになっている。

次に独自の型を定義している。symbol というのは文字列型だと思っていればよさそう。変数 var、オブジェクト obj、フィールド field がそれぞれ文字列により一意に定められるということ。

.type var <: symbol
.type obj <: symbol
.type field <: symbol

ここから facts を与えてゆく。
まずは4つの関係 (relation) を定義する。このような "関係" という考え方は Prolog と同様であり、データ間に成り立つ事実であると思えばよい。たとえば、assign( a:var, b:var ) は「変数 a が、変数 b の指すオブジェクトを指す」という a と b の2項関係である。

// -- inputs --
.decl assign( a:var, b:var )
.decl new( v:var, o:obj )
.decl ld( a:var, b:var, f:field )
.decl st( a:var, f:field, b:var )

そして facts を具体的に与えてゆく。与える facts は解析対象のプログラムに対応している。たとえば、プログラム中で変数 v2 が v1 に代入されているので、assign("v1","v2") が与えられる。

// -- facts --
assign("v1","v2").

new("v1","h1").
new("v2","h2").
new("v3","h3").

st("v1","f","v3").
ld("v4","v1","f").

ここから最終的に求めたいポインタ解析の結果を導くための rules を定義してゆく。
以下は、エイリアス関係を表現するための alias( a:var, b:var ) である。

// -- analysis --
.decl alias( a:var, b:var ) 
alias(X,X) :- assign(X,_).
alias(X,X) :- assign(_,X).
alias(X,Y) :- assign(X,Y).
alias(X,Y) :- ld(X,A,F), alias(A,B), st(B,F,Y).

変数 a と b がエイリアスの関係にあるのは、4通りのパターンがあることが分かる。
1つ目の alias(X,X) :- assign(X,_). という rule であるが、これは「代入文の左辺に登場する変数はその変数自身とエイリアスの関係にある」という当たり前のケースである。2つ目のケースも同様である。
3つ目の alias(X,Y) :- assign(X,Y). では「代入文があれば左辺の変数は右辺の変数のエイリアスになる」という rule である。
4つ目の alias(X,Y) :- ld(X,A,F), alias(A,B), st(B,F,Y). がやや複雑なケースであり、変数 A, B がエイリアスであり、X = A.F と B.F = Y という代入があるとき、変数 X, Y がエイリアスになるという rule である。

最後に、ポインタ解析の結果となる pointsTo( a:var, o:obj ) という関係を定義する。

.decl pointsTo( a:var, o:obj )
.output pointsTo
pointsTo(X,Y) :- new(X,Y).
pointsTo(X,Y) :- alias(X,Z), pointsTo(Z,Y).

この rules はシンプルであり、new した場合と、エイリアスの変数が指しうるオブジェクトを自身も指しうる場合の2つからなる。
この関係が最終的に求めたいものであるので、.output pointsTo という命令を書くことで pointsTo.csv というファイルに結果が出力される。以下がその例である。各行が fact になっており、変数とそれが指しうるオブジェクトを意味している。

$ cat pointsTo.csv 
v1      h1
v1      h2
v2      h2
v3      h3
v4      h3

このポインタ解析の例では、「どうやって指しうるポインタを求めるか？」というアルゴリズム的な視点が不要であり「どんな関係が成り立つか？」を定義するだけでよい。これが Datalog のような論理型のプログラミング言語の利点である。実際、この程度のポインタ解析でも非論理型のプログラミング言語で実装するのはけっこうめんどくさい。

その他 Soufflé について

上記は簡単な例であったが、チュートリアルを進めていくと Soufflé のより高度な機能について知ることができた。あとは何か実装したくなったら調べながらやればよさそう。以下は Soufflé に関するメモ。

入出力となる facts はcsv だけでなく SQLite3 データベースにも対応している。つまり、RDB に対するクエリとして使用したり、結果を RDB のテーブルとして格納できる。これは便利そう。
チュートリアルの中に、集合 A の要素の順序関係を示す Succ(x:symbol, y:symbol) という関係があったが、これを使って順序の先頭 First(x: symbol) を表現するのに悩んだ。答えは First(x) :- A(x), ! Succ(_, x). である。 $\{ x \mid x \in A \land \nexists y \in A. \text{Succ}(y, x) \}$ を求めればよいと思ったが、これを $\{ x \mid x \in A \land \forall y \in A. !\text{Succ}(y, x) \}$ と変形して、 $y$ の部分を Datalog の _ で置換するのが正しい。このあたりは Prolog らしい部分であり、慣れが必要そう。
Prolog のクエリとしてよくある ?:-parnt(X, Y) みたいな形式は Soufflé ではサポートされてないっぽい。インタラクティブな使い方より、ファイルを入出力とするバッチ処理的な用途が想定されていそう。

所感

データ統合やデータ交換などのデータ活用の文脈では、スキーママッピングと呼ばれる、あるデータスキーマを別のスキーマにマッピングするような操作は重要である。このマッピングの方法にはいろいろあるが、わりと表現力の高いクラスとして GLAV というものがあり、これが Datalog の表現力と近いらしい。これが今後 Datalog の重要性が高まってゆくであろうという理由のひとつである。
一方で、SQL と比較するとやはりクエリを書くのが難しい。クエリの実行時の性能が想定よりも悪いとき、チューニングするのも至難の業だと思われる。人類には早すぎる。

2020-11-06

Spring Transaction Management: @Transactional In-Depth を読む Part 2

トランザクション管理 spring

Part 1 のつづき。

元記事は以下。

www.marcobehler.com

How Spring’s or Spring Boot’s Transaction Management works

Spring のトランザクション管理や transaction abstraction framework は実際何をしているのか？
JDBC では setAutocommit(false) がトランザクションを開始する唯一の手段であったが、Spring ではトランザクションを開始するための複数の方法がある。とはいえ、Spring もトランザクションを開始し、コミットまたはロールバックするとうことには変わりない。

How to use Spring’s Programmatic Transaction Management?

実際に使われることはあまりないが、Spring でトランザクション管理をするもっとも初歩的な方法は、 TransactionTemplate か PlatformTransactionManager を使うやり方である。

そのコード例は以下である。

@Service
public class UserService {

    @Autowired
    private TransactionTemplate template;

    public Long registerUser(User user) {
        Long id = template.execute(status ->  {
            // execute some SQL that e.g.
            // inserts the user into the db and returns the autogenerated id
            return id;
        });
    }
}

JDBC の例を比較すると、以下のような特徴がある。

データベース接続を開始したり終了するような面倒な処理がない。代わりに、Transaction Callbacks を使用している。これは template.execute の部分のことを指している。execute メソッドの引数としてSQL文のみを定義しておけば、適切なトランザクション管理のもと execute メソッドをコールバックとして実行してくれる。
SQLException を catch する例外処理が不要。

これは Spring を用いた手続き的なトランザクション管理の例であった。次に宣言的なトランザクション管理の方法を見よう。

How to use Spring’s XML Declarative Transaction Management?

Spring では、@Transactional アノテーションが導入される前、XML によってトランザクションが定義されていた。詳細は見ないが、スタート地点として以下のコードを見てみる。

<!-- the transactional advice (what 'happens'; see the <aop:advisor/> bean below) -->
    <tx:advice id="txAdvice" transaction-manager="txManager">
        <!-- the transactional semantics... -->
        <tx:attributes>
            <!-- all methods starting with 'get' are read-only -->
            <tx:method name="get*" read-only="true"/>
            <!-- other methods use the default transaction settings (see below) -->
            <tx:method name="*"/>
        </tx:attributes>
    </tx:advice>

上記のコードは XML で AOP advice (Aspect Oriented Programming) を定義している。この定義した advice の ID が txAdvice である。

以下のコードで txAdvice を UserService クラスのメソッドに適用している。

<aop:config>
    <aop:pointcut id="userServiceOperation" expression="execution(* x.y.service.UserService.*(..))"/>
    <aop:advisor advice-ref="txAdvice" pointcut-ref="userServiceOperation"/>
</aop:config>

<bean id="userService" class="x.y.service.UserService"/>

UserService クラスは以下のような感じである。

public class UserService {

    public Long registerUser(User user) {
        // execute some SQL that e.g.
        // inserts the user into the db and retrieves the autogenerated id
        return id;
    }
}

以上のコードは Java だけ見ればシンプルに書ける一方で、XML は複雑で冗長なものとなっている。
XML よりよいトランザクションの定義の方法はないか？そこで @Transactional アノテーションの登場である。

How to use Spring’s @Transactional annotation ( Declarative Transaction Management )

モダンな Spring のコードを見てみよう。

public class UserService {

    @Transactional
    public Long registerUser(User user) {
       // execute some SQL that e.g.
        // inserts the user into the db and retrieves the autogenerated id
        // userDao.save(user);
        return id;
    }
}

ここまでシンプルに書くためには以下の２つのことをしなければならない。

あなたの Spring Configuration に @EnableTransactionManagement アノテーションを付与すること。（Spring Boot は自動的にやってくれている。）
Spring Configuration の中でトランザクションマネージャーを定義すること。
すると、Spring は自動的に判断して、任意の Bean の @Transactional アノテーションのついた public メソッドが1つのトランザクション内で実行されるようになる。

つまり、@Transactional アノテーションを機能させるために必要なことは以下だけである。

@Configuration
@EnableTransactionManagement
public class MySpringConfig {

    @Bean
    public PlatformTransactionManager txManager() {
        return yourTxManager; // more on that later
    }

}

具体例には、@Transactional アノテーションの付いた UserService のコードは以下に相当する処理をする。

public class UserService {

    public Long registerUser(User user) {
        Connection connection = dataSource.getConnection(); // (1)
        try (connection) {
            connection.setAutoCommit(false); // (1)

            // execute some SQL that e.g.
            // inserts the user into the db and retrieves the autogenerated id
            // userDao.save(user); <(2)

            connection.commit(); // (1)
        } catch (SQLException e) {
            connection.rollback(); // (1)
        }
    }
}

の部分は JDBC の標準的なトランザクション管理のコードである。
の部分はあなたが書いたコードである。

この例はちょっとした魔法のようであるが、次は Spring がどうやってこのコードを生成したのか見ていこう。

眠くなってきたので Part 2 はこのあたりで終わりにする。
ここから濃い話が続く感じなので気が向いたら読もう。
今のところ @Transactional をメソッドに付けると、その中身がトランザクションとして実行されることは分かった。

2020-11-03

Spring Transaction Management: @Transactional In-Depth を読む Part 1

spring トランザクション管理

トランザクション管理って難しい。
Spring を用いてトランザクション管理を解説している以下の記事がよさげだったので整理しながら読んでみる。

www.marcobehler.com

この記事を読み終わるころには、Spring の @Transactional アノテーションがどのように動作するのか理解できるようになるらしい。知りたい。ただし、ACIDつまりトランザクションとは何であるのかは理解していることを想定している。

なので簡単に ACID やトランザクションという概念についてまとめておく。

データベース操作の列のうち、ACID を満たすものを「トランザクション」と呼ぶ。
ACID は atomicity, consistency, isolation, durability の４つの性質のことである。抜粋すると、操作列が途中で失敗したらロールバックできるし、複数の操作の並列アクセスによる排他の問題は発生しないような性質。
すこし視点を変えると、一連の操作を ACID なものとして扱いたいとき、一連の操作が「トランザクションであること」を明示してやることになる。そうすればロールバックも排他制御も自前で実装しなくてよい。

以下、元記事の章ごとに重要そうなところをメモってゆく。

Introduction

この解説では、Spring 特有のトランザクション管理の方法から始めるのではなく、 JDBC transaction management のおける古典的なトランザクション管理の方法から解説する。
Spring の @Transactional アノテーションは、この古典的な考えを基礎としているので、まずはその基礎を知ることが重要である。

How plain JDBC Transaction Management works

How to start, commit or rollback JDBC transactions

Spring の @Transactional アノテーションでも、Hibernate でも、その他のデータベースライブラリであっても、結局のところ「データベーストランザクションを開いて閉じる」という点は同じである。この「開いて閉じる」ことを「管理する」と呼ぶ。

JDBC におけるトランザクション管理をするコードの例を以下に示す。

import java.sql.Connection;

Connection connection = dataSource.getConnection(); // (1)

try (connection) {
    connection.setAutoCommit(false); // (2)
    // execute some SQL statements...
    connection.commit(); // (3)

} catch (SQLException e) {
    connection.rollback(); // (4)
}

データベースへ接続する。
このメソッド名からは直感的でないが、setAutoCommit(false) の実行が Java においてトランザクションを開始する唯一の方法である。このメソッドを実行すると、あなたはトランザクションのマスターになれるわけだ。
トランザクションをコミットする。
例外が発生したらロールバックする。

ざっくり言うと、@Transactional アノテーションが用いられたとき、Spring はこの4つの処理をやっているだけである。
@Transactional アノテーションがどのように動作するか詳しく見る前に、知っておくべきことを先に説明する。

How to use JDBC isolation levels and savepoints

Spring の @Transactional アノテーションをすでに使ったことがある人であれば、以下のようなコードを見たことがあるかもしれない。

@Transactional(propagation=TransactionDefinition.NESTED,
               isolation=TransactionDefinition.ISOLATION_READ_UNCOMMITTED)

このアノテーションは以下の基本的な JDBC のコードになるだけである。

import java.sql.Connection;
// isolation=TransactionDefinition.ISOLATION_READ_UNCOMMITTED
connection.setTransactionIsolation(Connection.TRANSACTION_READ_UNCOMMITTED); // (1)
// propagation=TransactionDefinition.NESTED
Savepoint savePoint = connection.setSavepoint(); // (2)
...
connection.rollback(savePoint);

Spring の TransactionDefinition.ISOLATION_READ_UNCOMMITTED は、JDBC ではデータベースの接続の isolation level として反映される。
Spring の TransactionDefinition.NESTED は、JDBC ではデータベースの savepoint として表現されるだけである。

こんな感じで JDBC を考えれば、Spring は全然難しいことをしてるわけではない！

眠くなったので今日はここまで。続きは後日。

2020-10-22

Kotlin で gRPC のチュートリアルをやってみた

gRPC kotlin

REST はまぁ分かる。SOAP はなんとなく分かる。gRPC はまったく分からない。ってことで gRPC について少し調べてみた。

gRPC について

gRPC は 2015 年に Google によって公開された Remote Procedure Call (RPC) プロトコルである。RPC プロトコルなので location transparency を実現するものである。つまり、ユーザが手続きを呼び出すとき、その手続きがローカルにあるかリモートにあるかを意識する必要がないのが利点である。

REST とは異なり、gRPC はクライアントとサーバ間のストリーム通信等がサポートされている。gRPC はトランスポート層に HTTP/2 を採用しているものの、ユーザはこれを意識する必要がなく、呼び出す手続きや引数・戻り値だけケアすればよいのも利点。

クライアントとサーバのインターフェースとして protocol buffers という Interface Definition Language (IDL) を採用している。このインターフェースはプログラミング言語やプラットフォームに中立的な形をもつため、クライアントとサーバが異なるプログラミング言語で実装されていても容易に通信できる。

protocol buffers で記述したインターフェースの例を以下に示す。

service HelloService {
  rpc SayHello (HelloRequest) returns (HelloResponse);
}

message HelloRequest {
  string greeting = 1;
}

message HelloResponse {
  string reply = 1;
}

SayHello が手続きの名前であり、リクエストとレスポンスの型がそれぞれ HelloRequest と HelloResponse である。HelloRequest の型は構造体として定義され、フィールドとして greeting という名前の文字列をもつ。= 1 はフィールドに ID を付与するものであり、通信時のデータのシリアライズのときに使用される。HelloResponse も同様である。

要するに、protocol buffers を用いて、クライアントとサーバが通信するときのルールを定めている。REST のように URL や HTTP メソッドでリソースを指定するのではなく、gRPC では手続き名とリクエストとレスポンスの型を定義している。

具体的な通信を実装するときは、クライアントは、手続きに合うリクエストを作り、レスポンスを処理する必要がある。同様に、サーバは、リクエストを処理し、その結果をレスポンスとして返却する必要がある。このような処理は特定のプログラミング言語を用いてそれぞれ実装する必要がある。そこで protocol buffers で定義されたインターフェースに合うように、特定のプログラミング言語でクライアント・サーバを実装するためのソースコードを自動生成する機能がある。このような protocol buffers から各言語へのトランスパイラやランタイムは Github 上で配布されている。

Kotlin の Quick Start やってみた

gRPC を用いた通信を実装してみたかったので、もっとも簡単なチュートリアルである Quick Start をやってみた。使用するプログラミング言語ごとにコースがあるのだが、最近気に入っている Kotlin を選択。このコースでは、サーバもクライアントも Kotlin で書かれる。

チュートリアルでは IDE の使用を想定していないが、ソースコードを変更しながらいろいろ実験してみたかったので、Intellij IDEA Community Edition 2020.2 を使用。Gradle 5.2.1。以下、チュートリアルのセクションごとの Intellij を用いるための設定メモ。

Get the example code

git clone したあとに Intellij で examples ディレクトリを開く。自動的に Gradle が走ってビルドしてくれる。けっこう時間かかる。

Run the example

サーバの起動は、Intellij 上で

server/src/main/kotlin/io/grpc/examples/helloworld/HelloWorldServer.kt

のファイルを開いて main 関数を実行。このときパスの設定が上手く行ってないので、エディタ上ではエラーが表示されるが実行はできる。このエラーはあとで解消する。

クライアントの起動は、以下のファイル中の main 関数を実行。

client/src/main/kotlin/io/grpc/examples/helloworld/HelloWorldClient.kt

クライアントが起動した直後、Received: Hello world というメッセージを出力して終了することを確認。

Update the gRPC service

以下の protocol buffers を定義したファイルをチュートリアルの通りに書き換えて保存。

protos/src/main/proto/io/grpc/examples/helloworld/hello_world.proto

Update the app

更新した hello_world.proto から gRPC のためのサーバ・クライアント用の Kotlin ファイルを自動生成する。まず、stub/build.gradle.kts に以下のように１行追加することで自動生成されるファイルの場所を変更する。

protobuf {
    protoc {
        artifact = "com.google.protobuf:protoc:${rootProject.ext["protobufVersion"]}"
    }
    plugins {
        id("grpc") {
            artifact = "io.grpc:protoc-gen-grpc-java:${rootProject.ext["grpcVersion"]}"
        }
        id("grpckt") {
            artifact = "io.grpc:protoc-gen-grpc-kotlin:${rootProject.ext["grpcKotlinVersion"]}:jdk7@jar"
        }
    }
    generatedFilesBaseDir = "$projectDir/src" // added
    generateProtoTasks {
        all().forEach {
            it.plugins {
                id("grpc")
                id("grpckt")
            }
        }
    }
}

Intellij の Gradle ウィンドウから stub 配下の build を実行すると、stub/main 以下にいくつかのソースコードが自動生成される。

このとき、stub/main ディレクトリ直下に grpc と grpckt ディレクトリが生成されるが、これらがプロジェクトのソースコードとして認識されていないので認識させる。具体的には、この２つのディレクトリそれぞれを Intellij のエクスプローラー上で右クリックし、"Mark Directory as Source Root" をクリック。これでエディタ上で

server/src/main/kotlin/io/grpc/examples/helloworld/HelloWorldServer.kt

などを開いたときに出ていたエラーが消える。

あとは Update the server や Update the client の通りにソースコードを修正。自動生成されたスタブ（クライアント側）やサービス（サーバ側）がプロジェクトによって正しく認識されているので、エディタ上での自動補完なども効くはず。

Run the updated app

Run the example で述べた手順と同様にサーバとクライアントを起動すればよい。自分で手を加えた修正が実行結果に反映されたことを確認したら本チュートリアルは終わり。

おまけ：サーバを Kotlin、クライアントを Go で通信

同じ Quick Start のチュートリアルの Go のコースをやると、Go 言語で書かれたクライアントが作成できる。ポート番号を合わせて、Kotlin のチュートリアルで作成したサーバと通信してみた。

$ go run greeter_client/main.go Alice
2020/10/22 01:35:42 Greeting: Hello Alice
2020/10/22 01:35:42 Greeting: Hello again Alice

確かに通信できている。これが protocol buffers を用いたプログラミング言語をまたぐ gRPC 通信の例。

参考リンク

2020-09-26

リストや木構造に対する再帰的な操作の合成

論文メモプログラム合成

けっこう有名だけど、ちゃんと読んだことなかった論文。手法 $\lambda^{2}$ というプログラム合成の手法。

タイトル

Synthesizing Data Structure Transformations from Input-Output Examples

PLDI2015

Synthesizing data structure transformations from input-output examples | Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

概要

リストや木構造のような再帰的なデータ構造に対して、高階関数の map や fold を含むプログラムを合成する手法を提案。

手法の入出力

手法の入力

入出力例 $a_i \mapsto b_i$ の集合 $\mathcal{E}_\text{in}$

手法の出力

プログラム
- $\forall i. (e\ a_i ) \rightsquigarrow b_i$
- コストモデル $\mathcal{C}$ において最小なもの

DSL の定義

DSL は代数型と再帰をもつラムダ式に基づいたものである。具体的な定義は以下。

f:id:t-keita:20200920015838p:plain

$\bigoplus$ は演算子であり、任意のものを追加することができるが、predefined なものとして map, mapt, filter, foldl, foldr, foldt, recl が定義されている。各命令のセマンティクスは以下の通りである。

f:id:t-keita:20200926013503p:plain

map, filter, fold はお馴染みの関数だが、recl ってなにもの？

Hypothesis によるプログラムの抽象化

欠けている（具体的されていない）構造をプレースホルダとしてもつ可能性のあるプログラムを hypothesis と呼ぶ。プレースホルダは自由変数として表現され hole と呼ばれる。hole をもつ hypothesis は open hypothesis と呼ばれる。なお open でない、closed hypothesis は program のはず。

たとえば、 $x$ や $\lambda x.f^{\ast} x$ は、それぞれ自由変数 $x$ と $f^{\ast}$ をもつので open hypothesis である。なお $x$ や $f^{\ast}$ が hypothesis に対する hole である。一方で、 $\lambda x. \texttt{map} (\lambda y. y + 1)\ x$ は、束縛変数しか持たないので closed hypothesis である。

合成アルゴリズムでは、hypothesis に含まれる hole を、具体的なプログラムや別の hypothesis に置換してゆくことで入出力の制約を満たすプログラムを見つける。

Synthesis Algorithm

まずは合成アルゴリズムの全体像から見てゆく。

f:id:t-keita:20200926010500p:plain:w400

$Q$ は subtask のキューである。 $e$ を hypothesis, $f$ を ( $e$ に含まれる) hole, $\mathcal{E}$ を入出力例とするとき、subtask は $(e, f, \mathcal{E})$ の3つ組から構成される。 hypothesis $e$ として最も簡単な形のプログラム $\lambda x.f$ から開始し、hole を DSL の命令に置換ししてゆく。なお、１行目は $\mathcal{E}$ でなく $\mathcal{E_\text{in}}$ が正しそう。

subtask の $e$ が closed hypothesis であれば、プログラムとして不足のない形であるため、入出力の制約を満たすか調べるのみである。(lines 4-7)

subtask の $e$ が open hypothesis であれば、hole $f$ をより複雑な構造 $h$ で置換してゆく。hole $f$ の型を出力例 $\mathcal{E}$ から推論し、その型に合う hypothesis $h$ を求める。このとき新たな hypothesis を作る処理は InductiveGen 内で行われる。詳細は後述。(lines 8, 9)

hypothesis $e$ に含まれる hole $f$ を hypothesis $h$ で置換し、その結果を $e'$ とする。得られる hypothesis が close である場合はキューに追加するのみである。得られる hypothesis $e'$ が open である場合、 $e'$ に含まれる hole $f^{\ast}$ に対し、 $f^{\ast}$ が満たすべき入出力例 $\mathcal{E}^{\ast}$ を求める。この処理は Deduce 内で行われる。(lines 10-15)

合成が成功する場合の具体例として、たとえば以下のように hypothesis の形が具体化されてゆく。

$\lambda x.f$
$\lambda x.(\texttt{foldl}\ h'\ [\ ]\ x)$ where $h' = \lambda a. \lambda e. f'$
$\lambda x.(\texttt{foldl}\ h'\ [\ ]\ x)$ where $h' = \lambda a. \lambda e. f'$ and $f' = \texttt{cons} (e, a)$

このとき $\lambda x.f$ の入出力の制約が以下であるとき、

$[\ ]\mapsto [\ ]$
$[0 ]\mapsto [0 ]$
$[0\ 1]\mapsto [1\ 0]$
$[0\ 1\ 2]\mapsto [2\ 1\ 0]$

$h' = \lambda a. \lambda e. f'$ の入出力の制約は以下となる。

$([\ ], 0) \mapsto [ 0 ]$
$([ 0 ], 1) \mapsto [1\ 0 ]$
$([1\ 0], 2) \mapsto [2\ 1\ 0 ]$

このように、hypothesis の構造を展開するのにあわせて、新たな hypothesis が満たすべき入出力の制約を演繹的に求めてゆくのがこの手法の特徴である。

Hypothesis Generation

Figure 2 のアルゴリズム中の InductiveGen( $\tau$ ) の詳細を見てゆく。ここでは、型 $\tau$ を満たす hypothesis を作る。

closed hypothesis を作るには、Figure 3 の命令のうち $\tau$ と型の整合性が取れるものを列挙するのみである。つまり、演算子として再帰的に hypothesis を持てるのは Figure 3 の命令のみという前提？DSL の演算子として独自に追加した命令が再帰的な構造を持つことは許されない？

closed hypothesis を作るため、Figure 3 以外の DSL の構文要素を列挙してゆく。このとき、型が $\tau$ と整合性が取れるもののみを再帰的に列挙する。型の整合性によって探索空間を削減しているものの、組み合わせ爆発が起きそうなところである。stream を採用しているのはこれを軽減するためっぽい。(とはいえ、解となる最小のプログラムのコストが n の場合は、やはりコストが (n-1) 以下のプログラムをすべて列挙する必要がある。)

Inference of New Examples Using Deduction

Figure 2 のアルゴリズム中の Deduce の詳細を見てゆく。ここでは、subtask $(e, f, \mathcal{E})$ から新たな $e'$ と $f^{\ast}$ が定まったとき、適切な入出力の制約 $\mathcal{E}^{\ast}$ を演繹的に求める。具体化には $e'$ の命令の種類に応じて Figure 4 の規則に従うように $\mathcal{E}^{\ast}$ を構成すればよい。

一部の具体例を見る。

①
f:id:t-keita:20200926024114p:plain:w400
新たに map を使う hypothesis を作ったとき、その時点での入出力 $\mathcal{E}$ のなかに入力と出力のリストの長さが異なるものがあったら、適切な $\mathcal{E}^{\ast}$ は存在しない ( $\bot$ )。たとえば、 $[1,2,3 ] \mapsto [1,2 ]$ を実現する map は存在しない。

②
f:id:t-keita:20200926024808p:plain:w400
新たに map を使う hypothesis を作ったとき、その時点での入出力 $\mathcal{E}$ のリストの要素のなかに、同じ入力値に対して異なる出力値が対応するようなものがあれば、適切な $\mathcal{E}^{\ast}$ は存在しない ( $\bot$ )。たとえば、 $[1,2,1 ] \mapsto [5, 6, 7 ]$ を実現する map は存在しない。なぜなら、1 に対応する値が 5 と 7 の2種類存在し、写像 (map) になっていないから。

上記2つの規則①,②は、整合性が取れないことを検出するためのものであったが、次の規則は整合性が取れた時に $\mathcal{E}^{\ast}$ が満たすべき要件について述べている。
f:id:t-keita:20200926025617p:plain:w400
たとえば、 $\mathcal{E} = \{ [1,2 ] \mapsto [5, 6 ] \}$ のとき、 $\mathcal{E}^{\ast} = \{ 1 \mapsto 5, 2 \mapsto 6 \}$ が得られる。

その他の規則に関しては論文参照。

Evaluation

論文参照。

所感

トップダウンで deductive な合成のアプローチ。わりと素直なやり方だと思う。入出力の制約を高階関数の引数に伝播させる仕組みが面白い。
演算子の引数のなかにリスト型のものが2つ以上存在するときは、入出力の制約を伝播するのは難しそう。たとえば、リストとリストを結合する演算子をサポートする場合など。このあたりは FlashMeta あたりが上手く扱っていた気がする。
ページ数は多いしフォーマルな記述がある一方で、例がたくさんあって理解しやすい。soundness や completeness についても議論がある。論文の書き方として参考になる。
具体化されていない構造をもつプログラムは、この論文では hypothesis と呼ばれているが、最近では sketch と呼ばれることが多い印象。ただ Morpheus の論文では、hypothesis と sketch という両方の用語を使っていた。

2020-09-22

Go言語で標準出力を上書きする方法（プログレスバーなど）

コマンドラインツールを作るとき、進捗状況をリアルタイムで表示したい。

Ubuntu の例ではこういう感じ。

f:id:t-keita:20200922025024g:plain

ソースコード

上記の Go 言語でのサンプルコードは以下の通り。

タイマーとか使うのが面倒だったので、適当に長めのループを回して、全体の p % に達したタイミングで標準出力の表示を上書きしている。おまけに | 記号がグルグル回転する簡単なアニメーションも作ってみた。

package main

import "fmt"

var marks = []string{"|", "/", "-", "\\"}

func mark(i int) string {
    return marks[i%4]
}

func main() {
    cnt := 5000000000
    for i := 1; i <= cnt; i++ {
        if i%(cnt/100) == 0 {
            p := i / (cnt / 100)
            fmt.Printf("\rLoading: %s %2d%%", mark(p), p)
        }
    }
    fmt.Println("\nDone.")
}

ポイントは fmt.Printf("\rLoading: %s %2d%%", mark(p), p) という部分。

\r によって "キャリッジリターン" を出力している。

キャリッジリターン

キャリッジリターン (carriage return, CR) は制御文字の1つであり「カーソルを行頭に移動させる」という意味を持つ。Go 言語を含め、多くのプログラミング言語でエスケープ文字 \r によってキャリッジリターンが表現される。

Carriage return - Wikipedia

標準出力とターミナルの挙動

標準出力 (stdout) はストリームである。ストリームにはデータが送られるのみで、すでに送ったデータが削除されることはない。ターミナル上の表示では文字データが上書きされているように見えるが、文字データの削除や更新が行われているわけではなく、ただ文字データが次々に送られているだけである。

今回の例では、Linux のターミナルが、キャリッジリターンを受け取ったときに、カーソルを行頭まで戻しているため、文字データが上書きされているように見えている。

実際、先ほどのプログラムの実行結果を log.txt にリダイレクトし、そのファイルの中身を xxd コマンドで見てみる。

$ go run main.go > log.txt
$ xxd log.txt | head
00000000: 0d4c 6f61 6469 6e67 3a20 2f20 2031 250d  .Loading: /  1%.
00000010: 4c6f 6164 696e 673a 202d 2020 3225 0d4c  Loading: -  2%.L
00000020: 6f61 6469 6e67 3a20 5c20 2033 250d 4c6f  oading: \  3%.Lo
00000030: 6164 696e 673a 207c 2020 3425 0d4c 6f61  ading: |  4%.Loa
00000040: 6469 6e67 3a20 2f20 2035 250d 4c6f 6164  ding: /  5%.Load
00000050: 696e 673a 202d 2020 3625 0d4c 6f61 6469  ing: -  6%.Loadi
00000060: 6e67 3a20 5c20 2037 250d 4c6f 6164 696e  ng: \  7%.Loadin
00000070: 673a 207c 2020 3825 0d4c 6f61 6469 6e67  g: |  8%.Loading
00000080: 3a20 2f20 2039 250d 4c6f 6164 696e 673a  : /  9%.Loading:
00000090: 202d 2031 3025 0d4c 6f61 6469 6e67 3a20   - 10%.Loading:

標準出力に送られたすべての文字データがちゃんと残っていることが確認できる。ちなみに、Unicode ではキャリッジリターンは 16 進数で 0d であり，この文字も一定間隔で出現していることが分かる。

まとめ

コマンドラインツールで出力を上書きするような表現は、標準出力のストリームにキャリッジリターンを送ることで実装できる。
標準出力に指定されたターミナルは、キャリッジリターンを読んだとき、カーソルを行頭に移動させているだけであり、文字データの削除や更新を行っているわけではない。
なお、標準出力にキャリッジリターンを送ることができるプログラミング言語であれば、同様のやり方で同様のふるまいを実装できるはず。

2020-09-16

論文：機械学習を用いたボトムアップなプログラム合成

論文メモプログラム合成

タイトル

BUSTLE: Bottom-up program-Synthesis Through Learning-guided Exploration

arXiv, Submitted on 28 Jul 2020

[2007.14381] BUSTLE: Bottom-Up Program Synthesis Through Learning-Guided Exploration

手法の入出力

手法の入力

入出力例の集合
- 論文上では $\mathcal{I}$ と $\mathcal{O}$ の２つ組という雑な表現になっているが、実際は任意の $i \in \mathcal{I}$ に対してユニークに $o \in \mathcal{O}$ が定まるものとしている。

手法の出力

プログラム
- ただし、任意の $(i, o) \in (\mathcal{I}, \mathcal{O})$ に対して $P(i) = o$ を満たす。

DSL の定義

プログラム合成手法では、DSL (Domain-Specific Language、ドメイン固有言語) をドメインごとに定義し、その上でプログラムを構築するアプローチが一般的である。本手法では、文字列を操作するための DSL を独自に定義している。

f:id:t-keita:20200916013428p:plain

入出力例からのプログラム合成 (Programming by Example) の実用化の代表的である、Excel に搭載されている FlashFill で用いられる DSL よりも複雑な文法となっており、課題設定として難易度の高いものとなっている。

Property Signatures

property signatures は入出力例を特徴ベクトルに変換する手法である。機械学習をプログラム合成に適用する研究は近年盛んに行われているが、property signatures は ICLR2020 で発表されたばかりの手法である。

Learning to Represent Programs with Property Signatures | OpenReview

まず、property signatures を具体例を用いて説明する。以下の図 (Listing 1) の io_pairs は入出力例であり、p1, p2, p3 は入出力例を引数にとって Mixed, AllFalse, AllTrue のいずれかを返す関数である。たとえば p1 は「入力文字列が出力文字列に含まれているか」を返す関数である。p1, p2, p3 は入出力例 io_pairs を引数にとり、それぞれ Mixed, AllFalse, AllTrue を返す。この [Mixed, AllFalse, AllTrue] というリストが io_pairs の property signatures である。

f:id:t-keita:20200916013907p:plain

もう少し厳密に書くと、入力 $\mathcal{I}$ と出力 $\mathcal{O}$ の型をそれぞれ $\tau_\text{in}$ , $\tau_\text{out}$ とすると、 $(\tau_\text{in}, \tau_\text{out}) \rightarrow \texttt{Bool}$ という型をもつ関数を property とする。各入出力例に property を適用した結果を集約することで、入出力例に対して AllTrue（すべて True の場合）、AllFalse (すべて False の場合)、Mixed（それ以外）を出力する。この値を property signature とする。あらかじめ定められた $k$ 個の property から出力される $k$ 個の property signature のリストが property signatures である。

なお、property を定義するのは人間である。

Bottom-Up Synthesis with Learning

この手法のアルゴリズムの重要な部分は以下の Algorithm 1 で表現されている。

f:id:t-keita:20200916020953p:plain

青字で書かれた部分を無視すると一般的な bottom-up な合成アルゴリズムである。bottom-up なアルゴリズムでは、プログラムの大きさ（具体的には構文木のノード数）の小さいものから順番に列挙してゆくだけである。たとえば、大きさが 9 以下のプログラムをすべて列挙できているとき、次に列挙するのは大きさが 10 のものである。構文木のトップレベルに使用する命令 $op$ を固定したとき、 $op$ の引数の合計の大きさが 9 となるように引数を列挙する。たとえば、 $op$ が２つの引数を取るのであれば、第一引数と第二引数のプログラムの大きさとして (1,8), (2,7), ..., (8,1) の場合をそれぞれ列挙する。

青字で書かれた部分を考慮した場合、プログラムの大きさに加えて property signature を用いた重みづけを行うことで正解に至りそうなプログラムを優先的に列挙する。具体的には、16 行目でボトムアップに構築したプログラムの出力 $\mathcal{V}$ と出力 $\mathcal{O}$ における property signature を計算し、17 行目で重みの更新を行う。このとき、binary classifier $p(- \mid \mathcal{I}, \mathcal{V}, \mathcal{O})$ によって、現在のプログラムの出力 $\mathcal{V}$ が入力 $\mathcal{I}$ から出力 $\mathcal{O}$ へ至る中間結果としてどの程度もっともらしいのか確率を計算する。この確率が 1 に近いほど重みは小さく、0 に近いほど重みが大きくなるように重みの更新が行われる。

Model Architecture and Training

binary classifier $p(- \mid \mathcal{I}, \mathcal{V}, \mathcal{O})$ のためのニューラルネットワークはシンプルな構造をもつ。property signatures を使うことで人間の知見が表現されているので deep な構造を回避できているという。学習データセットは自動生成している。詳しくは論文参照。

Evaluation

論文参照。

所感

機械学習を用いたプログラム合成は近年 ML 系のコミュニティでよく発表されている。そっち系の論文10 本くらいは読んだが、ほとんどの機械学習手法が、入出力例が属するドメインからパターンを抽出することにフォーカスしている。そのため、手法に対してドメインをまたぐ汎用性は期待しないほうがよい印象。どの論文を見てもドメインに依存しない汎用的なアイデアを提案しているのだが、ドメインに依存せずに性能が出るとは言っていないので要注意。
関連研究にもあるが、"Write, execute, assess: Program synthesis with a REPL" (NeurIPS2019) とアイデアが似ていて、具体的な研究の貢献がよく分からない。手法のコアである bottom-up synthesis と property signatures はもちろん既存技術であるし、作りかけのプログラム (partial program) の実行結果と出力例を比較するというアイデアも execution-guided synthesis という名で知られている。ただし、本手法のアルゴリズムはかなりシンプルなので、先行研究と同じような性能が出るのであれば本手法のやり方を参考にするのはよいかもしれない。
作りかけのプログラムの実行結果と出力を比較する execution-guided synthesis は、結局のところ「出力の部分構造が、合成すべきプログラムの部分構造に対応する」という考えに基づいているような気がする。出力文字列の一部が常に大文字なら、プログラムとして大文字を返す命令を含むべき、みたいな。これはもちろん一般的な合成関数にはまったく当てはまらない。 $(g \circ f) (a)$ が $f(a)$ の名残をとどめていることが重要そう。
bottom-up なアプローチはどうしても入出力例の制約を活かしづらく、有益でないプログラムを無駄に探索してしまう印象がある。top-down な手法との比較結果を見てみたい。