Skip to main content
Erschienen in: Journal of Automated Reasoning 4/2020

04.07.2019

Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL

verfasst von: Mnacho Echenim, Hervé Guiol, Nicolas Peltier

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2020

Einloggen

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We formalize in the proof assistant Isabelle essential basic notions and results in financial mathematics. We provide generic formal definitions of concepts such as markets, portfolios, derivative products, arbitrages or fair prices, and we show that, under the usual no-arbitrage condition, the existence of a replicating portfolio for a derivative implies that the latter admits a unique fair price. Then, we provide a formalization of the Cox–Rubinstein model and we show that the market is complete in this model, i.e., that every derivative product admits a replicating portfolio. This entails that in this model, every derivative product admits a unique fair price. In addition, we provide Isabelle functions to compute the fair price of some derivative products.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Fußnoten
1
It can be argued that this assumption is incorrect because that there is always a nonzero probability that investors will not be payed what they are owed. But because these bills are backed by national governments, this probability is very close to 0.
 
2
This property is also called countable additivity in the literature.
 
3
The superscript may be omitted if there is no confusion.
 
4
This is a simplification as in practice, two prices are associated with each asset: a bid price, which represents the price traders are willing to pay to buy the asset, and an ask price, which represents the price traders are willing to sell the asset. Bid prices are always lower than ask prices, but on markets on which high volumes of assets are traded, both prices are typically very close.
 
5
Note that buying a basket option on Apple and Google is not the same as buying a call on Apple and another one on Google.
 
6
For the definition of qty-single, we use the notation \(f(a{:}{=}b)\), which in Isabelle represents an update of function f so that the image of a becomes b.
 
7
Closing out all positions means getting rid of all the assets in a portfolio, i.e., selling those with a long position, and buying back those with a short position.
 
8
A money market account represents a deposit account on which any amount of cash can be deposited/withdrawn at each time.
 
9
Recall that the model of an equity market does not model foreign-exchanges with several currencies, although more sophisticated models for this setting do exist. The latter are closer to reality, since they permit to account for, e.g., the fact that national banks may have different risk-free rates.
 
Literatur
1.
Zurück zum Zitat Avigad, J., Hölzl, J., Serafin, L.: A formally verified proof of the Central Limit Theorem. J. Autom. Reason. 59(4), 389–423 (2017)MathSciNetCrossRef Avigad, J., Hölzl, J., Serafin, L.: A formally verified proof of the Central Limit Theorem. J. Autom. Reason. 59(4), 389–423 (2017)MathSciNetCrossRef
2.
3.
Zurück zum Zitat Bingham, N.H., Kiesel, R.: Risk-Neutral Valuation: Pricing and Hedging of Financial Derivatives. Springer-Verlag, London (2004)CrossRef Bingham, N.H., Kiesel, R.: Risk-Neutral Valuation: Pricing and Hedging of Financial Derivatives. Springer-Verlag, London (2004)CrossRef
4.
Zurück zum Zitat Black, F., Scholes, M.: The pricing of options and corporate liabilities. J. Polit. Econ. 81(3), 637–654 (1973)MathSciNetCrossRef Black, F., Scholes, M.: The pricing of options and corporate liabilities. J. Polit. Econ. 81(3), 637–654 (1973)MathSciNetCrossRef
5.
Zurück zum Zitat Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving—5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pp. 93–110. Springer (2014) Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving—5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pp. 93–110. Springer (2014)
6.
Zurück zum Zitat Cox, J.C., Ross, S.A., Rubinstein, M.: Option pricing: a simplified approach. J. Fin. Econ. 7(3), 229–263 (1979)MathSciNetCrossRef Cox, J.C., Ross, S.A., Rubinstein, M.: Option pricing: a simplified approach. J. Fin. Econ. 7(3), 229–263 (1979)MathSciNetCrossRef
7.
Zurück zum Zitat Durrett, R.: Probability: Theory and Examples. The Wadsworth & Brooks/Cole Statistics/Probability Series. Dadsworth Inc. Duxbury Press, Belmont, CA (1991) Durrett, R.: Probability: Theory and Examples. The Wadsworth & Brooks/Cole Statistics/Probability Series. Dadsworth Inc. Duxbury Press, Belmont, CA (1991)
9.
Zurück zum Zitat Echenim, M., Peltier, N.: The binomial pricing model in finance: A formalization in Isabelle. In: de Moura, L. (ed.) Automated Deduction—CADE 26–26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pp. 546–562. Springer (2017) Echenim, M., Peltier, N.: The binomial pricing model in finance: A formalization in Isabelle. In: de Moura, L. (ed.) Automated Deduction—CADE 26–26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pp. 546–562. Springer (2017)
10.
Zurück zum Zitat Kou, S.G.: Discrete barrier and lookback options. Handb. Oper. Res. Manag. Sci. 15, 343–373 (2007) Kou, S.G.: Discrete barrier and lookback options. Handb. Oper. Res. Manag. Sci. 15, 343–373 (2007)
11.
Zurück zum Zitat Hölzl, J.: Construction and stochastic applications of measure spaces in higher-order logic. Ph.D. thesis, Institut für Informatik, Technische Universität München (2012) Hölzl, J.: Construction and stochastic applications of measure spaces in higher-order logic. Ph.D. thesis, Institut für Informatik, Technische Universität München (2012)
13.
Zurück zum Zitat Hölzl, J., Lochbihler, A., Traytel, D.: A Formalized Hierarchy of Probabilistic System Types—Proof Pearl. In: Proceedings of ITP, pp. 203–220 (2015) Hölzl, J., Lochbihler, A., Traytel, D.: A Formalized Hierarchy of Probabilistic System Types—Proof Pearl. In: Proceedings of ITP, pp. 203–220 (2015)
14.
Zurück zum Zitat Hull, J.: Options, Futures and Other Derivatives. Pearson/Prentice Hall, Upper Saddle River (2009)MATH Hull, J.: Options, Futures and Other Derivatives. Pearson/Prentice Hall, Upper Saddle River (2009)MATH
15.
Zurück zum Zitat Cutland, N.J., Roux, A.: Derivative Pricing in Discrete Time. Springer-Verlag, London (2013)CrossRef Cutland, N.J., Roux, A.: Derivative Pricing in Discrete Time. Springer-Verlag, London (2013)CrossRef
16.
Zurück zum Zitat Kaliszyk, C., Parsert, J.: Formal microeconomic foundations and the first welfare theorem. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 91–101, New York, NY, USA, 2018. ACM Kaliszyk, C., Parsert, J.: Formal microeconomic foundations and the first welfare theorem. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 91–101, New York, NY, USA, 2018. ACM
18.
Zurück zum Zitat Nipkow, T.: Social choice theory in HOL. J. Autom. Reason. 43(3), 289–304 (2009)CrossRef Nipkow, T.: Social choice theory in HOL. J. Autom. Reason. 43(3), 289–304 (2009)CrossRef
19.
Zurück zum Zitat Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle/HOL. Springer Publishing Company, Incorporated, Berlin (2014)CrossRef Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle/HOL. Springer Publishing Company, Incorporated, Berlin (2014)CrossRef
20.
Zurück zum Zitat Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, Berlin, Heidelberg (2002)CrossRef Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, Berlin, Heidelberg (2002)CrossRef
21.
Zurück zum Zitat Shreve, S.E.: Stochastic Calculus for Finance I: The Binomial Asset Pricing Model. Springer Finance, Berlin (2003)MATH Shreve, S.E.: Stochastic Calculus for Finance I: The Binomial Asset Pricing Model. Springer Finance, Berlin (2003)MATH
22.
Zurück zum Zitat Vestergaard, R.: A constructive approach to sequential Nash equilibria. Inf. Process. Lett. 97(2), 46–51 (2006)MathSciNetCrossRef Vestergaard, R.: A constructive approach to sequential Nash equilibria. Inf. Process. Lett. 97(2), 46–51 (2006)MathSciNetCrossRef
Metadaten
Titel
Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL
verfasst von
Mnacho Echenim
Hervé Guiol
Nicolas Peltier
Publikationsdatum
04.07.2019
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 4/2020
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-019-09528-w

Weitere Artikel der Ausgabe 4/2020

Journal of Automated Reasoning 4/2020 Zur Ausgabe