日本ソフトウェア科学会第 36 回大会 (2019 年度) 講演論文集

パラメトリシティに基づくプログラム微積分
森畑 明昌

漸増計算とは，ある入力に対して一度出力を求めた後，入力が僅かに変化した場合に，前回の出力を用いて新しい入力に対する出力を高速に得る手法である．Cai ら（PLDI 2014）は，ラムダ式で記述されたプログラムを漸増計算を達成するプログラムへと変形する操作を提案し，これを「微分」と名付けた．この「微分」は数学的な微分との類
似はあるものの，両者の関係性は不明であった．しかも，Cai らによる「微分」はラムダ式の構文に操作や証明が依存しており，一般化や他の手法との関連性の議論が困難であった．本発表ではまず，Cai らの「微分」を多相型のパ
ラメトリシティの観点から再定式化する．これにより，プログラムの具体的な表現から離れ，型で表された抽象的な情報のみで議論を行うことができ，理論的な見通しが良くなる．さらに，この「微分」と全く同様の操作により，数学的な「微分」を得られること，具体的にはそれが Elliott の自動微分手法（ICFP 09）の一般化となることを示す．
さらに，同様の方法で離散的「微分」や数学的「微分」の逆演算である「和分」「積分」を行う可能性について論じる．

When an input is slightly modified, incremental computing enables efficient calculation of the corresponding
output by using the previous output. Cai et al. (PLDI 2014) proposed a program transformation that takes
a programs in a lambda calculus and results in a program, called derivative, that achieves incremental computing. Though their derivatives are somewhat similar to the mathematical derivatives, their relationshipwas unclear. Moreover, their transformation and its proof were tightly connected to syntactic manipulations,and therefore, it was difficult to study its generalization and its relationships to other methods. This presentation reformulates the transformation by Cai et al. via parametricity of parametric polymorphic types.
This reformulation enables us to abstractly discuss the properties based on types. Then, this presentationshows that the same approach can derive mathematical derivatives. In fact, the transformation turned out
to be a generalization of the automatic differentiation method by Elliott (ICFP 2009). In addition, thispresentation discusses possibilities of applying the same approach to summation and integration, which are
the inverses of finite differentiation and continuous (i.e, mathematical) differentiation, respectively.

mental evaluation）に分けられる．静的な手法では，

1 はじめに漸増計算を行わないプログラムを，漸増計算を達成す

漸増計算とは，計算 f に対する入力 x の計算結果

るプログラムへと変換する．動的な手法では，プログ

y = f x が既に求まっている際に，入力が少しだけ変ラムを変換するのではなく，その解釈を変更すること′′化して x = x ⊕ dx となったとき，y を用いて f x ので漸増計算を実現する．

計算を効率よく行う手法である．ここで，dx は（通Cai らは [2] 単純型付きラムダ計算を対象とした静常小さな）変更，⊕ はその変更の適用を表す演算子

的な漸増計算手法を提案し，この手法を漸増的ラムダである．

計算（incrementalizing lambda calclus）と名付けた．

漸増計算手法は大きく静的な手法（漸増計算変換，

漸増的ラムダ計算では，漸増変換を行うためのプログ

incrementalization）と動的な手法（漸増評価，incre-

ラムを得る「微分」と呼ばれるプログラム変換が定義されている．特に，関数 f :: A → B を「微分」するこ

Program Differentiation and Integration based on
Parametricity.
Akimasa Morihata, 東 京 大 学 大 学 院 総 合 文 化 研究 科,
Dept. of Arts and Sciences, the University of Tokyo.

とで，以下の等式を満たす関数 f ′ :: A → ∆A → ∆Bが得られるこれは，f の入力を dx だけ変化させた時の f の結果は，f x と f ′ x dx を組み合わせて得られる，ということを意味する．なお，∆A および ∆B

つけるだけではなく，得られた微分手法が Elliott のはそれぞれ A および B に対する変更の型である．

前向き自動微分 [4] である点でも興味深い．

f (x ⊕ dx ) = f x ⊕ f ′ x dx

さらに，これら差分・微分の考え方が，その逆演算

漸増的ラムダ計算は興味深い手法だが，実用・理論

である和分・積分へ至る可能性について述べる．差の両面から以下のような疑問が残っていた．

分・微分が定義されたとしても，和分・積分をどう定• 単純型付きラムダ計算だけでなく，実用的なプ義すべきかは自明には定まらない．本研究では，和ログラミング言語のプログラムに対しても同様

分を「入力の変更過程によってもたらされる出力のの「微分」が定義できるか？

変化の集約」との観点から定式化する．この観点は，• 漸増的ラムダ計算の「微分」は数学的な「微分」とどのような関係にあるか？

Morihata [10] の漸増計算手法で入力の複雑な変更を扱うために用いられたものであり，漸増計算の観点か

まず，実用的な観点からは，単純型付きラムダ計算

らは自然なものである．そして，プリミティブ演算がは再帰等が表現できないため不十分である．しかし，和分・積分可能であれば，これを組み合わせて得られ

Cai らの変換や証明は構文に依存したものとなっておるプログラムも和分・積分可能であることを示す．

り，再帰をはじめ様々なプログラミング言語の構成要
素が自然に取り扱えるかは非自明であった．また，理2 準備論的な観点からは，漸増的ラムダ計算の「微分（以下本稿では原則として Haskell [11] を用いてプログラ

これを数学的な微分と区別して差分と呼ぶ）」が本当

ムを表現する．特に，式 e が型 τ を持つ状況を e :: τに数学的な「微分」であると言えるのかは定かでなと記述する．fst と snd はそれぞれ組の最初の要素とい．もし差分が微分に繋がるのであれば，「プログラ

2 つ目の要素を抽出する関数である． Haskell では 2

ム微分積分学」のようなものに繋がる可能性があるた

項演算子は通常カリー化形式として扱うが，本稿ではめ，この点は是非明らかにしたい．

反カリー化形式で，つまり組を引数とする関数として

以上のような状況をふまえ，本発表では以下の 3 点
を示す．

扱う．
本研究の議論は Cai らの漸増的ラムダ計算 [2] を基

まず，漸増的ラムダ計算の差分化を多相型のパラメ

礎としている．漸増的ラムダ計算では，基本型とそのトリシティの観点から定式化し直す．この再定式化に操作が一定の性質を満たすことを仮定し，それらをラ

よって差分化の操作で得られるプログラムが変わるわ

ムダ計算によって組み合わせたプログラムについてのけではない．そのため，この再定式化自身は非常に大性質を論じている．この状況を捉えるため，本研究できな貢献というわけではない．しかし，これにより，は ML 系のプログラミング言語におけるモジュール

証明の見通しが良くなり，実用的なプログラムへの一を用いる．

般化も簡単になる．実際，以降の議論はこの再定式化

モジュールは定数および関数の集まりからなる．以に基づいている．また，漸増的ラムダ計算の着想であ

下，定数を定数関数と同一視し，「定数および関数」をる「プリミティブ演算を差分化し，その結果を高階関

単に「関数」と呼ぶことにする．特に，以下では特定数を介して伝播する」という点をより明確に表すことの型 X の値を扱う関数群からなるモジュールに注目ができる点も長所である．

する．関数 f1 :: τ1 (X), f2 :: τ1 (X), . . . , fn :: τn (X)

次に，漸増的ラムダ計算の差分化と同様の手法で数からなるモジュールを M = (f1 , f2 , . . . , fn )，その学的な微分が得られることを示す．具体的には，プリシグネチャを S(X) = [τ1 (X), τ2 (X), . . . , τn (X)] とミティブ演算が（差分化可能なだけでなく）微分可能

し，M :: S(X) と記述する．例えば，整数値リスト

である場合，それを高階関数で組み合わせたプログラ

に関するモジュール MList = ([ ], (:), null, uncons) のムが差分化と全く同様にして微分できることを示す．

シグネチャは SList (X) = (X, (Int, X) → X, X →この結果は，漸増的ラムダ計算の差分化を微分に結びMaybe(Int, X)) として MList :: SList ([Int]) となる．

以下，モジュールは言語の一級市民とし，これを引を f の差分関数と呼ぶ）が存在することである．

数とする関数を考える．直感的にはモジュールを単にf (x ⊕ dx ) = f x ⊕ ffd (x, dx )関数の組（ないしレコード）と捉えれば良い．例えCai ら [2] は，モジュールの各関数が差分化可能でば MList を引数とする形で，リストの要素順序を逆あるとき，そのモジュールを用いて記述したプログラ

転する reverse 関数を以下のように定義できる．
reverse :: ∀X. SList (X) → X → Int

ムに対し，その差分化関数を導出するプログラム変換

reverse (e, c, unc) x = aux x e

算子を含まない単純型付きラムダ式に制限されていを与えている．このプログラム変換の対象は不動点演

where aux x h = case unc x of

たが，Giarrusso ら [5] はこれを一般のラムダ式に拡Nothing → h

張している．いずれの変換も，ラムダ式に対する構文

Just a y → aux y (c (a, h))モジュールを引数とすることで，リスト以外であっても同様に列をなすような値であれば反転を求められるような定義となっていることに注意せよ．

3 漸増的ラムダ計算
漸増的ラムダ計算では，モジュールの各関数が漸増計算に適している場合に，そのモジュールを組み合わせて記述したプログラムが漸増計算を達成することを示している．本稿では，各モジュールについて以下の性質を要求する †1 ．
まず，基本型 A に対し，その局所的な変化の型 ∆Aおよび変化を適用する演算子 (⊕A ) :: (A, ∆A) → A
が存在するとする．なお，以下の議論では簡単のため，x ⊕A 0A = x を満たす変換の単位元 0A :: ∆A の存在を仮定する．誤解のない範囲で添字は省略する．

∆A はあくまで局所的な変化を表し，より一般的な変化は A → A の関数として扱う．例えば，リスト型

的な変換として定式化されている．そのため，プログ
ラム全体の変換が必要となるためライブラリとしての実装が困難である，言語の構成要素を増やした際の再証明が面倒である，等の問題点がった．本研究ではこのプログラム変換をパラメトリシティを用いること
で再定式化する．
まず，モジュール M = (f1 , . . . , fn ) :: S(A) に対し，差分付加モジュール M̂fd = (fˆ1 , . . . , fˆn ) :: S(Âfd)
fd

fd（ただし Âfd = (A, ∆A)）を以下の通り定義する．
fˆi (x, dx ) = (fi x, fi (x, dx ))fd

fd

このとき，差分関数導出定理は以下となる．
定理 3.2. モジュール M :: S(A) とその差分付加モジュール M̂fd :: S(Âfd)，そしてパラメトリック多相型の関数 g :: ∀X. S(X) → X → X について，以下が成り立つ．g M̂fd (x, dx ) = (y, dy) であるとき，• g M x=y
• g M̂fd (x ⊕ dx ) = y ⊕ dy ．

[A] に対する ∆[A] は先頭要素の追加・削除のみを含

証明. パラメトリック多相型に関するパラメトリシ

むかもしれない．加えて，a ∈ A に対して適用可能な

ティ [12] [15] により証明を行う．まず，g M x = y

局所的な変更の部分集合 Ua ⊆ ∆A を a の近傍と呼ぶ．なお，具体的にどのような変化を局所的だと捉えは fst ◦ g M̂fd = g M と等価であるが，これは各
fi ∈ M について定義より明らかに fst ◦ fˆi = fi であるかは応用によるため，本研究では定義の具体的な内ることより導かれる．また，g M̂fd (x ⊕ dx) = y ⊕ dy

実には深入りしない．

は (⊕) ◦ g M̂fd = g M ◦ (⊕) と等価であるが，これ定義 3.1. 関数 f :: A → B †2 が差分化可能であるとは，各 fi ∈ M が差分化可能であること，すなわち(⊕) ◦ fˆi = fi ◦ (⊕) を満たすことより導かれる．

は，以下を満たす関数 ffd :: (A, ∆A) → ∆B （これfdfd

定理 3.2 は，g M の差分関数が snd ◦ g M̂fd であ†1 これは Cai らの定式化よりはやや弱い条件だが，以下に見るように我々の目的には十分である．
†2 この関数を含め，以下現れる関数軍についての議論は適当な関手 F および G を用いて f :: FA → GA という型の関数の場合に自然に拡張できる．この議論は直裁なので本稿では深入りしない．

ることを述べている．すなわち，型 A の値を計算す
る関数について，A に関する計算を全て差分付加することで差分関数が得られることになる．これは実際

に既存研究 [2] [5] でのプログラム変換の骨子である．

変更がごく僅かな場合の極限にどうなるかを論じるのが数学での微分である．我々の導出が微分にまでス

4 高階差分ケールするかは興味のあるところである．

関係データベース処理などの文脈では高階差分，す関数の微分を議論するためには，その関数の定義

なわち差分関数の差分など，が有用であることが知域及び値域が一定の性質を満たさなければならない．

られている [8]．高階差分も全く同様の手法で導出で本研究では，関数 f :: A → B について以下の状況を

きる．

考える．

いま，基本型 A に対し，その k 階までの変化の型
0i∆ A（0 ≤ i ≤ k，∆ A = A，∆i+1i

A = ∆(∆ A)iと す る ）お よ び 変 化 を 適 用 す る 演 算 子 (⊕ ) ::
i−1

i

i−1

まず，型 A（ないし B ）の値に対する変更 ∆A が，(⊕) に加え，距離関数 d :: ∆A × ∆A → R をもつものとする．略記法として ||dx || = d(dx , 0) とし，これA（1 ≤ i ≤ k）が存在す

を dx の大きさと呼ぶ．これらは「変更を小さくしたるとする．関数 f :: A → B が k 階差分化可能である

際の極限」を議論する際に用いる．さらに，微分値のとは，全ての 1 ≤ i ≤ k について，以下を満たす関数

型を (A → B)d ⊆ ∆A → ∆B とする．(A → B)d は

f (i) fd :: (∆i−1 A, ∆i A) → ∆i−1 B （これを f の i 階以下の性質を満たすことをを要求する．

(∆

A, ∆ A) → ∆差分関数と呼ぶ）が存在することである．
f (0) fd = ff (i−1) fd (x ⊕ dx ) = f (i−1) fd x ⊕ f (i) fd (x, dx )こ の 場 合 に つ い て も ，モ ジュー ル M =(f1 , . . . , fn ) :: S(A) に対する，k 階差分付加モジュール Mˆ(k) fd = (fˆ1 , . . . , fˆn ) :: S(Aˆ(k)fd )（ただしfd

fd

Aˆ(k) fd = (A, ∆A, . . . , ∆k A)）を以下のように定義する．
fˆi fd (x0 , x1 , . . . , xk ) =(1)• (A → B)d が関数合成に関して閉じていること ，す な わ ち 任 意 の f ∈ (A → B)d お よ びg ∈ (B → C)d について g ◦ f ∈ (A → C)d ．
• 変 更 を 顕 著 に 増 幅 し な い こ と ．す な わ
ち 任 意 の fd∈

(A → B)d ，a∈

A，およ び 十 分 小 さ な a の 近 傍 Ua に つ い て ，
1 ),fd (a⊕da))supda 1 ,da 2 ∈Ua d(fd (a⊕daが有限の値をd(da 1 ,da 2 )

持つ．
(k)

(fi x0 , fi fd (x0 , x1 ), . . . , fi fd (xk−1 , xk ))このとき以下の定理が成り立つ．これは定理 3.2 の一般化であるが，証明は全く同様である．
定理 4.1. モジュール M :: S(A) とその k 階差分付
加モジュール Mˆ(k) fd :: S(Aˆ(k)fd )，そしてパラメト

定義 5.1. 差分化可能関数 f :: A → B が入力 x で微
分値 f ′ :: (A → B) をもつとは †3 ，xdd(ffd (x, dx ), fx′ dx )=0||dx ||→0||dx ||
を満たすことである．ここで ffd は f の差分関数でlimある．関数 f が入力 x で微分可能であるとは，関数リック多相型の関数 g :: ∀X. S(X) → X → X について，以下が成り立つ．g Mˆ(k) fd (x0 , x1 , . . . , xk ) =f が入力 x での微分値をもつことであり，関数 f が(y0 , y1 , . . . , yk ) であるとき，分値を持つこととする．関数 f が微分可能であると微分可能であるとは，f の定義域のすべての入力で微• g M x0 = x1

き，f の微分 fd :: A → (A → B)d とは fd x が f の• g M̂fd (xi ⊕ xi+1 ) = yi ⊕ yi+1 ．

x での微分値となるような関数である．

定理 4.1 は，g M の i 階差分関数が g M̂fd の i 番

上記定義は，引き算の代わりに距離関数を用いて目（ただし最初の要素を 0 番目とする）の要素の計いる点を除き，標準的な微分の定義である．ただし，算に対応することを述べている．

この定式化では，(A → B)d は線形写像の集合とは限らない．微分値が実際に満たすべき制約（例えば線形

5 微分
ここまでの議論は，漸増計算を前提として，入力の変更を出力へ伝播することを考えてきた．特に入力の性）は目的や型 A に依存すると思われるためここで†3 ||dx || → 0 を 0 に近づける方向が問題となる場合は十分考えられるが，本稿ではそれに踏み込まない．適切な定式化のもとで方向微分を考えるのは自然である．

は深入りしない．

である．よって全体としては確かに 0 に漸近する．

差分の場合と同様，微分可能な関数のみからなるモジュールで書かれたプログラムは微分可能である．
まず，モジュール M = (f1 , . . . , fn ) :: S(A) に対し，
微分付加モジュール Md = (fˆ1 , . . . , fˆn ) :: S(Âd)
dd（ただし Âd = (A, (A → A)d )）を以下の通り定義する．ここで fi d は fi の微分である．
fˆi (x, f ′ ) = (fi x, fi x ◦ f ′ )dd

このとき，以下の定理が微分を導出する．
定理 5.2. モジュール M :: S(A) とその微分付加モジュール M̂d :: S(Âd )，そしてパラメトリック多相型の関数 g :: ∀X. S(X) → X → X について，以下が成り立つ．g M̂d (x, id) = (y, gx′ ) であるとき，gx′
は g M の x での微分値である．
証明. パラメトリック多相型に関するパラメトリシ

定理 5.2 は定理 3.2 同様微分値を付加したモジュールを用いることで系統的にプログラムの微分を得る
ことができることを示している．実は，この結果はElliott による前向き自動微分手法 [4] の一般化となっている．定式化上は，Elliott が型クラスを用いているのに対し，本研究ではモジュールとパラメトリシ
ティを用いてる点に差異があるが，得られる微分は同
一である．

6 和分
差分・微分が適切に定義できた以上，それらの逆にあたる和分・積分を定義したくなるのは自然な要求である．しかし，和分・積分の定義はそれほど自明ではない．

ティ [12] [15] により，各 fi について，「f ′ が点 y 上で数学的に採用される積分の標準的な定義の一つはの変化 dy をもたらす計算に対する適切な微分値であ「微分の逆演算」としての定義である．これに基づけ′るとき，fi d y ◦ f も適切な微分値となる」ことを示ば，関数 ffd :: (A, ∆A) → ∆B が与えられたとき，せばよい．つまり，適切に dx を小さく取ることによf (x ⊕ dx ) = f x ⊕ ffd (x, dx )′り，d(fi fd (dy), (fi d y ◦ f ) dx ) が十分に（||dx || に比を満たす関数 f :: A → B を求めるのが和分の操作と例する程度以上に）小さくなることを示せばよい．

なる．しかし，よく知られているように，この定義を以下，証明の概要を述べる．正確な議論には標準的満たす積分は一意には定まらない．通常の微積分学のな ǫ − δ 論法を使えばよい．d が距離関数であること

文脈では，積分定数を用いてこの問題を解決するが，を用いて以下のように式変形する

プログラムの微積分でも同じような処理が可能であ

′

≤

=

≤

d(fi fd dy, (fi d y ◦ f ) dx )||dx ||d(fi fd dy, fi d y dy)+||dx ||d(fi d y dy, (fi d y ◦ f ′ ) dx )||dx ||d(fi fd (dy), fi d y dy) ||dy ||+||dy||||dx ||′d(fi d y dy, fi d y (f dx )) d(dy, f ′ dx )d(dy, f ′ dx )||dx ||d(fi fd (dy), fi d y dy) ||f ′ dx || + d(dy, f ′ dx )+||dy||||dx ||′′d(fi d y dy, fi d y (f dx )) d(dy, f dx )d(dy, f ′ dx )||dx ||

y dy)(dy),fd(fは fi の微分dx が 0 に近づく時， ifd ||dy||i dd(dy,f ′ dx )′は f が微分値であることか可能性から， ||dx ||||f ′ dx ||ら，それぞれ 0 に近づく．一方で， ||dx || およびd(fi d y dy,fid y (f ′ dx ))は微分値の性質により有限値
d(dy,f ′ dx )るかは定かでない．
もう一つの標準的な定義は，いわゆる定積分を基本とし，面積として積分を定義するものである．本稿でもこの方針を採用する．すなわち，関数 f :: A → Bが与えられた時，a1 , aZ2 ∈ A に対して，
a2

f dx

a1

を「f の引数を a1 から a2 まで変化させた時の f の値の総和」と捉えるものである．この定義を成立させるためには，以下の 2 点を解決する必要がある．

• 型 B 上で「総和」という演算が定義されていなければならない．

• 「a1 から a2 まで変化させる」方法が定義されていなければならない．
Ra
前者については， a 2 f dx の結果を B ではなく B
1に対する変更と取ることで，変更の累積を「総和」として用いる．この定義は以下の 3 点の理由から自然
である．

• 定積分

Rb

f (x)dx を原始関数の値の差 F (b) −aF (a) と定義するのは自然である．型 B の値同士の差であるから，B に対する変更だと捉えるの(Pxa f ) b :: A → B とする．このとき，gb (x ⊕ dx ) = gb x ⊕ f (x, dx )である．
証明. 和分の定義により直截である．
定理 6.2 は差分関数の和分は元の関数とほぼ一致す

は自然である．

• 積分結果に B 上での初期値を与えることで B のることを述べている．また定理 6.3 は，本質的には和値を得ることができる．この初期値を積分定数と分の差分関数が元の関数となることを示している．

捉えれば，積分の曖昧性の自然な表現だと理解で差分や微分の場合と同様，和分可能な関数のみからなるモジュールで書かれたプログラムは和分可能できる．

• Morihata [10] は，入力が非自明に変化した際のある．まず，モジュール M = (f1 , . . . , fn , (⊕)) ::漸増計算を考え，入力の変化に対する出力の変化を累積する手法を示している．これは本稿で考え

S(A, ∆A) に 対 し ，和 分 付 加 モ ジュー ル Msum =(fˆ1 , . . . , fˆn , λx, f. f x) :: S(A, A → A) を以る「積分」と同じ処理であり，「積分」の実用上の下の通り定義する．

sum

sum

fˆi sum (x, f ′ ) =有用性を示唆する．

f′ x

X

fi

x

また，後者の問題については，目的ごとに用いるべ

和分可能関数は変更 ∆A を本質的に計算に用いるたき手法は異なると考えられるので，各具体的な演算ご

め，変更の適用 (⊕) がモジュールに含まれていなけとに規定されるものとする．

ればならないことに注意せよ．このとき，以下の定理

以上をふまえ，以下にまずは和分の定義を与える．
定義 6.1. 関数 f :: (A, ∆A) → ∆B ，値 a1 , a2 :: A，Pa
に対し，和分 a21 f :: B → B は以下を満たす値で

ある．
Pa
•
a f = λx. x
Pa2 ⊕daP•
f = λx. ( aa21 f ) x ⊕ f (a2 , da)a1

和分結果は局所的な変更とは限らないことに注意せよ．以下の定理が示すように，和分は差分の逆演算にほぼ対応する．
定理 6.2. ffd が f の差分関数ならば，
a⊕daX(ffd ) (f a) = f (a ⊕ da)aである．

が和分を導出する．
定理 6.4. モジュール M :: S(A, ∆A) とその和分付加
モジュール Msum :: S(A, A → A)，そしてパラメトリ
ック多相型の関数 g :: ∀X, Y. S(X, Y ) → (X, Y ) → Y
Paについて，g Msum (a1 , λx. a2 ) = a21 g M である．
証明. パラメトリック多相型に関するパラメトリシ
ティ [12] [15] により，和分の性質を満たすことを示す．

g Msum (a, λx. a) = λx. x は，各 fi についての和分の性質から明らかである．よって，g Msum (a1 , λx. a2 ⊕da) = λx. g Msum (a1 , λx. a2 ) x ⊕ g Msum (a2 , da)を示せばよい．このためには各 fi について，f ′ x =y ⊕ dy ならば fi sum (x, f ′ ) = λz. fi sum (x, λx. y) z ⊕fi (y, dy) が十分である．これも fi の和分の性質から

証明.

(
=
=

Pa⊕da
a

ffd ) (f a)従う．

{ 和分の定義 }(λx. x ⊕ ffd (a, da)) (f a)

7 積分{ 差分関数の定義 }

積分も和分と同様に定義できる．5 節と同様，変更

f (a ⊕ da)
定理 6.3. f :: (A, ∆A) → ∆B に対し，gb x =∆A 上に距離関数 d が定義されているとする．さらに，積分を極限として議論するため，変化が小さい時の積分値についての距離を考えたい．これを可能とするため，「十分に小さな変化を行う関数 f :: A → A」

については，それが局所的な変更と同一視できるこによって得られた関数合成が続く関数の入力を 2 区間と，つまり f = λx. x ⊕ da なる da :: ∆A が存在すに適切に分解することにより明らかである． 4 番目のること，を仮定し，定義域をそのような関数の上に性質も各 fi が上に有界であることより明らかに従う．

拡張する．すなわち，上述のような f については，

3 番 目 の 性 質 を 示 す た め に は ，各 fi に つ い てd(f, dx ) = d(da, dx ) とする．

「f ′ = λy. y ⊕ dy ′ が x から x ⊕ dx までの和分に

定義 7.1. 関数 f :: (A, ∆A) → ∆B が区間 a1 , a2 :: ARa
で積分値 a 2 f :: B → B をもつとは以下の条件を満よってもたらされるはずだった y からの変化 dy を積(y, f ′ ) が適
分により見積もったものだとして，fˆi

1

たすことである．
Ra• a f = λx. x
Rc
Rc
Rb• a f = ( b f) ◦ ( a f)

• lim||da||→0R
d( aa⊕da f,f (a,da))= 0．
||da||• a の 十 分 小 さ な 近 傍 Ua に お い て ，RRd( aa⊕da 1 f, aa⊕da 2 f )supda 1 ,da 2 ∈Uaが有限の値をd(da 1 ,da 2 )もつ．
関数 f が定義域上の任意の区間で積分値を持つとき，
これを積分可能であると呼ぶ．

1 つめと 2 つめの条件は，積分が和分とほぼ同等の性質を満たすことの表明である．積分は和分と違い，被積分関数が積分結果の正確な変化を記述しない．たint

切な積分となる」ことを示せばよい．つまり，適切にdx を小さく取ることにより，真の和分を dz として
R f′ yd( yfi , dz ) が十分に（||dx || に比例する程度以上に）小さくなることを示せばよい．

以下，証明の概要を述べる．正確な議論には標準的な ǫ − δ 論法を使えばよい．d が距離関数であることを用いて以下のように式変形する．
R f′ yd( yfi , dz )≤=||dx ||
R f′ yR y⊕dyd( yfi , yfi ) d(f ′ , dy)≤||dy ||||dx ||
R f′ yR y⊕dyd( yfi , yfi ) d(f ′ , dy)

だし，十分変化を小さく取れば，被積分関数が積分結果の変化に漸近することが期待される．これを述べているのが 3 つ目の条件である．4 つめの条件は，被積分関数が発散しないことを要求しており，これも自然である．

||dx ||
R f′ yR y⊕dyR y⊕dyfi , dz )d( yfi , yfi ) + d( yd(f ′ , dy)||dx ||R y⊕dyd( yfi , dz ) ||dy ||+d(f ′ , dy)||dx ||R y⊕dyd( yfi , dz ) ||f ′ || + d(f ′ , dy)||dy ||

和分と同様，積分可能な関数のみからなるモジュー

ここで，仮定より

M = (f1 , . . . , fn , (⊕)) :: S(A, ∆A) に対し，積分付
加モジュール Mint = (fˆ1 , . . . , fˆn , λx, f. f x) ::

に漸近し，

int

int

x

このとき，以下の定理が積分を導出する．
定理 7.2. モジュール M :: S(A, ∆A) とその積分付加

モジュール Mint :: S(A, A → A)，そしてパラメトリ
ック多相型の関数 g :: ∀X, Y. S(X, Y ) → (X, Y ) → Y
Raについて，g Mint (a1 , λx. a2 ) = a 2 g M である．
1||dx ||Rd( yy⊕dy fi ,dz )d(f ,dy)および||dx ||||dy||R ′Rd( yf y fi , yy⊕dy fi )||f ′ ||

ルで書かれたプログラムは積分可能である．モジュール

S(A, A → A) を以下の通り定義する．
Z f′ xfˆi int (x, f ′ ) =
fi

+

′

d(f ′ ,dy)は0と ||dx || は有限なので，全体としても 0 に漸近する．
なお，残念ながら本稿で定義した積分は本稿で定義した微分の逆演算ではない．微分は (A → B)d の値をもつことが求められているが，積分は (A × ∆A) → ∆Bの関数を対象としており，型が合わない．詳しい関係
性についての議論は今後の課題である．

8 関連研究証明. パラメトリック多相型に関するパラメトリシ

本研究は漸増計算との関わりが深い．漸増計算につティ [12] [15] により，積分の性質を満たすことを示す．

いては多数の研究の歴史があるので，ここでは特に関1 番目の性質は各 fi の積分の性質により明らかであ連の深い研究について挙げる．

る．2 番目の性質も，各 fi の積分の性質，およびこれ

本研究は Cai ら漸増的ラムダ計算 [2] を基礎として

いる．Cai らは構文的なラムダ式の変換として微分係はないように見える．

（本研究で言うところの差分）を定義した．f :: A → B

本研究は，差分化から始め，極限を取ることで El-の差分関数の型が (A, ∆A) → B となるところも含

liott の前向き自動微分 [4] を導出した．前向き自動微め，本研究では基本的にこの手法を踏襲している．差分には他の手法もある．特に Siskind と Pearlmutter

異はパラメトリシティを用いている点だが，本研究で[13] による手法は，小さな変化を表す記号を伝播す導出される差分関数は Cai らの微分によって得られる点で，より差分化に近い．実際，Siskind と Pearl-る関数と意味上一致する．ただし，Cai らは単純型付

mutter の手法と漸増的ラムダ計算を融合する試みもきラムダ計算を考えているのに対し，本研究ではパラなされている [7]．しかし，Siskind と Pearlmutter のメトリシティが成り立つ範囲で任意のプログラムを考

手法は理論的な取り扱いが難しいことが知られていえている点が異なる．

る [9]．本研究では差分と微分を理論的に見通しよく

Giarrusso ら [5] は Cai らの手法を再帰関数を含む繋ぐことに成功している．

ラムダ計算に拡張し，さらに効率改善のためにある種著者の知る限り，漸増計算や微分に比べて，和分やのメモ化を加えた．本研究では議論を単純化するた積分についての議論は少ないようである．数少ない例

めに Giarrusso らの提案は取り入れていないが，実外である Morihata [10] の漸増計算手法についてはす

用上はメモ化は重要である．メモ化を本研究の定式でに述べた．他の可能性については今後調べてゆき

化で素直に導入できるかの検討は今後の課題である．

たい．

ただし，Giarrusso らはプログラムが A 正規形（の変種）であり全ての変数が lambda lifting されてい9 まとめと今後の課題

ることを仮定しており，本研究が一般的なプログラム

本研究では漸増的ラムダ計算を基礎に，これを多相を想定しているのとは状況が異なることは注意すべ型のパラメトリシティの観点から再定式化することきである．

で，微分・積分へと議論を発展させた．特に，漸増的漸増的ラムダ計算の考え方は，例えば漸増的双方向ラムダ計算の差分化が一般的なプログラムに適用で変換手法の導出 [6] などに利用されている．本研究のきることを示したこと，同様の手法でプログラムの微議論がこれら実用的な問題に適用できるかの確認も分が得られること，さらにそれら議論が和分・積分へ重要な課題である．

繋がることを示したことは主要な貢献である．

漸増的ラムダ計算の顕著な特徴は，静的な手法で本研究はプログラムの微分・積分を考える上での萌あること，そして高階関数を扱えることである．既存

芽的なものであり，今後の課題は多数残っている．

の漸増計算手法の多くは動的である．特に，高階関数

まず，本研究では基本的に 1 引数関数の微積分を考を扱える動的な漸増計算手法としては self-adjusting

えた．微積分学では多引数関数の微積分が非自明であ

computing [1] が代表的である．静的で高階関数を扱ることが知られている．本研究の手法は全微分へはほえる漸増計算手法としては，他にも部分評価に基づくぼ自明に拡張できる．しかし，偏微分についての議論

もの [14] がある．本研究との関連や融合の可能性につは今後の課題である．

いての調査は今後の課題である．

プログラムに関して微分積分が適切に定義できた

高階関数型言語に微分を取り入れる他の試みとして

暁には，既存の微分積分学での成果を援用できると望は，Ehrhard と Regnier による differential lambda

ましい．特に，テイラー展開や解析接続は，プログラ

calculus [3] が挙げられる．彼らの体系が，微分を複ムの性質の解析等において有用であると期待される．

雑な計算の局所的な線形近似と捉えることで，線形性

これらの可能性の検討についても今後の課題である．

を中心として構成されているのに対し，本研究では漸

本研究では，プリミティブ演算が一定の性質を満た

増計算，つまり差分化から議論を始め，線形性についす場合に，それを用いて構成されたプログラムが同ては全く触れなかった．そのため，両者には直接の関様の性質を維持する，という構造に注目し議論を行った．この構造を用いることで，他にも様々な変換が可能であることが期待される．例えば，自動微分の文脈では，今回考えた前向き自動微分だけでなく，後ろ向き自動微分なども存在し，機械学習の文脈等で重要となっている．後ろ向き自動微分を同様に扱う手法は今後の課題である．他の例として，例えば凸関数であれば大域最小値をニュートン法などで簡単に求めることができるが，これをプログラムの性質として扱うことも興味深い可能性だと考えている．
謝辞

関連研究を紹介してくださった北京大学の胡振江教授に感謝する．本研究は JSPS 科研費

19K11896 および 2019 年度国立情報学研究所公募型共同研究（19FA01）の助成を受けている．
参 考 文 献[ 1 ] Acar, U. A., Blelloch, G. E., and Harper, R.:
Adaptive functional programming, ACM Trans.
Program. Lang. Syst., Vol. 28, No. 6(2006), pp. 990–
1034.
[ 2 ] Cai, Y., Giarrusso, P. G., Rendel, T., and Ostermann, K.: A theory of changes for higher-orderlanguages: incrementalizing λ-calculi by static differentiation, ACM SIGPLAN Conference on Programming Language Design and Implementation,
PLDI ’14, Edinburgh, United Kingdom - June 09- 11, 2014, O’Boyle, M. F. P. and Pingali, K.(eds.),
ACM, 2014, pp. 145–155.
[ 3 ] Ehrhard, T. and Regnier, L.: The differential
lambda-calculus, Theor. Comput. Sci., Vol. 309,
No. 1-3(2003), pp. 1–41.
[ 4 ] Elliott, C. M.: Beautiful differentiation, Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009,
Edinburgh, Scotland, UK, August 31 - September 2,
2009, Hutton, G. and Tolmach, A. P.(eds.), ACM,
2009, pp. 191–202.
[ 5 ] Giarrusso, P. G., Régis-Gianas, Y., and Schuster, P.: Incremental \lambda -Calculus in CacheTransfer Style - Static Memoization by Program
Transformation, Programming Languages and Sys-

tems - 28th European Symposium on Programming,
ESOP 2019, Held as Part of the European Joint
Conferences on Theory and Practice of Software,
ETAPS 2019, Prague, Czech Republic, April 6-11,
2019, Proceedings, Caires, L.(ed.), Lecture Notes
in Computer Science, Vol. 11423, Springer, 2019,
pp. 553–580.
[ 6 ] Horn, R., Perera, R., and Cheney, J.: Incremental relational lenses, PACMPL, Vol. 2,
No. ICFP(2018), pp. 74:1–74:30.
[ 7 ] Kelly, R., Pearlmutter, B. A., and Siskind, J. M.:
Evolving the Incremental λ Calculus into a Modelof Forward Automatic Differentiation (AD), CoRR,
Vol. abs/1611.03429(2016). Extended abstract presented at the AD 2016 Conference, Sep 2016, Oxford
UK.
[ 8 ] Koch, C., Ahmad, Y., Kennedy, O., Nikolic,M., Nötzli, A., Lupei, D., and Shaikhha, A.:
DBToaster: higher-order delta processing for dynamic, frequently fresh views, VLDB J., Vol. 23,
No. 2(2014), pp. 253–278.
[ 9 ] Manzyuk, O.: A Simply Typed λ-Calculus of
Forward Automatic Differentiation, Electr. Notes
Theor. Comput. Sci., Vol. 286(2012), pp. 257–272.
[10] Morihata, A.: Incremental computing with data
structures, Sci. Comput. Program., Vol. 164(2018),
pp. 18–36.
[11] Peyton Jones, S.(ed.): Haskell 98 Language andLibraries: The Revised Report, Cambridge University Press, Cambridge, UK, 2003.
[12] Reynolds, J. C.: Types, Abstraction andParametric Polymorphism, Information Processing,Vol. 83(1983), pp. 513–523.
[13] Siskind, J. M. and Pearlmutter, B. A.: Nesting forward-mode AD in a functional framework,
Higher-Order and Symbolic Computation, Vol. 21,
No. 4(2008), pp. 361–376.
[14] Sundaresh, R. S. and Hudak, P.: Incremental Compilation via Partial Evaluation, Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida, USA, January 21-23, 1991, Wise,
D. S.(ed.), ACM Press, 1991, pp. 1–13.
[15] Wadler, P.: Theorems for Free!, FPCA’89 Conference on Functional Programming Languages andComputer Architecture. Imperial College, London,
England, 11-13 September 1989, ACM, New York,
1989, pp. 347–359.