形式的に記述された金融取引契約の等式変換の正しさ
2010SE177 大薮雅人
担当教員:横山哲郎

1

はじめに

次に x, y, z を同じ標本空間上で定義された確率変数 RV Rとすると，x +RV y や x −RV y も同じ標本空間上の確率変数である．また，max RV y z は y と z の内，最大値を返す演算である．これらより，確率変数の足し算 +RV と最大値を返す max RV に関して，以下の分配法則

金融取引契約とは，金融や保険業界で用いられる取引契約のことで，これらの契約はより単純な契約を組み合わせてできている．この点に注目して，文献 [1] では，契約を関数型言語の結合子を用いて形式的に記述することで，既存の契約だけではなく，新たな契約も簡単に記述
x +RV max RV y z = max RV (x +RV y) (x +RV z) (1)することができ，その価値も評価することができる方法が成り立つ．
を提案している．また，この文献の中で，契約の等式変換の一部は紹介されているが，その論証はされておらず， 2.2 価値評価過程における代数規則と証明
形式的に記述された等式変換の正しさは示されていない． 確率変数の足し算 +RV を価値評価過程の足し算 +PR ，
本研究の目的は，この形式的に記述された金融取引契 確率変数の最大値を返す max
RV を価値評価過程の最大約の新たな等式変換を発見し，その論証を行うことで正 値を返す max，確率変数の単項マイナス演算子−RVPRしさを示し，その結果から金融取引契約の最適化に応用 を価値評価過程の単項マイナス演算子 −PR に持ち上げできる等式変換の例を示すことである．ただ，これらの ることで定義する．それぞれの型と定義を以下に示す．
等式変換には，一見等しそうだが等しくない等式が含ま+PR , max PR :: PR R → PR R → PR R
れていることもあるので，注意して取り組む必要がある．
以上の目的を達成するために，以下の 3 つの課題を設(+PR ) = lift 2 (+RV )定した．1 つ目は，形式的に記述された金融取引契約の等max PR = lift 2 max RV式変換の探索を行うことである．2 つ目は，発見した等式−PR :: PR R → PR R
変換や文献 [1] の中で紹介されている等式変換の論証を行(−PR ) = lift (−RV )うことである．3 つ目は，それらの結果から金融取引契約の最適化に応用できる等式変換の例を示すことである． ここにおける lift ，lift とは，2以上の課題を解決することにより，以下の 2 つの効果
lift :: (a → b) → PR a → PR bが期待される．1 つ目は，形式的に記述された金融取引契

lift f a t = f (a t)
約間の関係の正しさを示すことにより，より多くの形式的な金融取引契約の正しさを示すことができるようにな
lift 2 :: (a → b → c) → PR a → PR b → PR c
ることである．2 つ目は，金融取引契約の最適化に応用
lift 2 f a b t = f (a t) (b t)
できる等式変換の例を示すことで，より簡単な契約の組み合わせとして表すことができるようになることである． である．これらより，価値評価過程における足し算 +PRと最大値を返す演算 max PR に関して，以下の分配法則

2等式変換の論証

x +PR max PR y z = max PR (x +PR y) (x +PR z) (2)
新たに発見した形式的に記述された金融取引契約の等式変換とその正しさを論証をすることにより示す．また， が成り立つ．証明を以下に示す．
LHS = { +PR の定義と max PR の定義 }一見等しそうだが等しくない等式が等しくならないこと
lift 2 (+RV ) x (lift 2 max RV y z)も反例を示すことにより示す．まず，確率変数上での代数= { lift 2 の定義 }規則を説明し，その代数規則を価値評価過程における代λt → x t +RV max RV (y t) (z t)数規則へと持ち上げる．次に，金融取引契約の形式的な= { +RV の max RV への左分配法則 (1) }記述に必要な命名慣習，関数および合成的意味論を説明
λt → max RV (x t +RV y t) (x t +RV z t)
する．そして，それらを踏まえて等式変換の論証を行う．
= { lift の定義 }22.1

確率変数の上の代数規則

型 a 上の価値評価過程 p とは，時刻から型 a を持つ確率変数への関数である．また，確率変数 p(t) は，時刻 tにおける p の可能な値を示すものである．これを非公式な型定義として以下のように書くことができる．

PR a = Date → RV alift 2 max RV (lift 2 (+RV ) x y) (lift 2 (+RV ) x z)
= { max PR の定義と +PR の定義 }RHS

また，K ，exchk (・) の価値評価過程を以下に示す．

K :: a → PR a
exchk (・) : Currency → PR R
K (x) は常に値 x を持つ過程，exch k1 (k2 ) は通貨 k2 における 1 単位の価値を通貨 k1 で表現した過程である．

金融取引契約に対する合成的意味論を反例を示すことで，証明する．(E2) の特別な場合とし契約 zero ，one と契約を引数にとる関数 and ，or およ て，同じ通貨同士との為替レートが考えられる．この場び give を定義する1 ．それぞれの型と定義を以下に示す． 合の価値評価過程を以下に示す．

2.3(A1) exchk (k ) = K (1)zero :: Contract
one :: Currency → Contract

そして，c1 =zero ，c2 =one k のとき，両辺はそれぞれgive :: Contract → Contract

Ek [[LHS ]] = { 定義 }and :: Contract → Contract → Contractor

Ek [[give (zero ‘or ‘ one k)]]= { E3, E5 }:: Contract → Contract → Contract−PR max PR (Ek [[zero]]) (Ek [[one k]])= { E1, E2 }zero は，権利も義務もない契約，(one k) は，通貨 k を1 単位受け取る契約である．また，(give c) は，c の権利をすべて義務として，逆に義務を権利として取得する
関数，(c1 ‘and ‘ c2 ) は，c1 と c2 の両方を取得する関数，(c1 ‘or ‘ c2 ) は，c1 か c2 の一方 (両方ではない) を取得する関数である．次に，金融取引契約に対する合成的意味論を取り入れる．関数 Ek [[c]] は，契約 c をとって，「時間の中の各瞬間に対して，その瞬間に c を取得したときの価値を通貨 k で表したもの」を記述する過程へと写像するものである．今回用いる意味論を以下に示す．

−PR max PR (K (0)) (exchk (k ))= { A1 }−PR max PR (K (0)) (K (1))= { K (0) と K (1) の関係 }−PR K (1)
Ek [[RHS ]] = { 定義 }Ek [[max PR (give zero) (give one k)]]= { E3, E5 }max PR (−PR Ek [[zero]]) (−PR Ek [[one k]])= { E1, E2 }Ek [[・]] :: Contract → PR R
(E 1)

Ek [[zero]] = K (0)(E 2)

Ek [[one k2 ]] = exchk (k2 )(E 3)

Ek [[give c]] = −PR Ek [[c]]max PR (−PR K (0)) (−PR exchk (k ))= { A1 }max PR (−PR K (0)) (−PR K (1))= { K (0) と K (1) の関係 }−PR K (0)(E 4) Ek [[c1 ‘and ‘ c2 ]] = Ek [[c1 ]] +PR Ek [[c2 ]]
(E 5)
2.4

Ek [[c1 ‘or ‘ c2 ]] = max PR (Ek [[c1 ]]) (Ek [[c2 ]])新たに発見した等式変換とその証明以上の内容より，and の or に対する分配法則2c1 ‘and ‘ (c2 ‘or ‘ c3 ) = (c1 ‘and ‘ c2 ) ‘or ‘ (c1 ‘and ‘ c3 ) (3)が成り立つ．証明を以下に示す．
Ek [[LHS ]] = { 定義 }Ek [[c1 ‘and‘ (c2 ‘or ‘ c3 )]]= { E4 }Ek [[c1 ]] +PR Ek [[c2 ‘or ‘ c3 ]]= { E5 }Ek [[c1 ]] +PR max PR (Ek [[c2 ]]) (Ek [[c3 ]])= { +PR の max PR への左分配法則 (2) }max PR (Ek [[c1 ]] +PR Ek [[c2 ]]) (Ek [[c1 ]] +PR Ek [[c3 ]])= { E4 }max PR (Ek [[c1 ‘and‘ c2 ]]) (Ek [[c1 ‘and‘ c3 ]])= { E5 }Ek [[(c1 ‘and‘ c2 ) ‘or ‘ (c1 ‘and‘ c3 )]]Ek [[RHS ]]同様に，一見等しそうだが等しくない等式

1 本稿では，契約を c で，通貨を k で表す．
2 本稿では，中置演算子を ・‘ ‘ で表す．

おわりに

本稿では，新たに発見した形式的に記述された金融取引契約の等式変換の正しさを，その論証を行うことで示した．また，一見等しそうだが等しくない等式についても，その反例を示すことで等しくならないことを示した．
これらの論証により，形式的に記述された金融取引契約間の関係の正しさを示し，金融取引契約の最適化に応用できる等式変換の例を示すことができた．また，より多くの形式的な金融取引契約の正しさを示し，より簡単な契約の組み合わせとして表すことができるようになった．
今後の課題としては，更なる金融取引契約の等式変換の論証を行い，その結果を用いることで金融取引契約の数理構造を明らかにしていくことが考えられる．

[1] Jones, S.P., Eber, J-M. and Seward, J.: Composing contracts: an adventure in ﬁnancial engineering(functional pearl). ACM SIGPLAN Notices, Vol.35,
No.9, pp.280-292 (2000).

一見等しそうだが等しくない等式とその証明

give (c1 ‘or ‘ c2 ) 6= give c1 ‘or ‘ give c23

参考文献= { 定義 }2.5となるので，この等式は等しくならないことがわかる．これは，(4) の左辺の契約では，契約相手に選択権があるのに対して，右辺では，契約の保有者が選択を行うという両者の現実世界での解釈が異なっていることにも合致する．

(4)[2] Anton van Straaten:
Composing Contracts,
available from hhttp://contracts.scheming.org/Contracts.htmli(accessed 2013-11-01).