- Financial derivatives are an important tool of today's finance sector. Despite their often negative public perception after the crisis of 2008, they are a tool originally developed to reduce risks in trading real goods. Understanding and evaluating derivatives is an important problem in practice. We present a declarative language of derivative contracts which is independent of pricing models. We also present a denotational semantics, enabling a calculus of contracts. The given denotational semantics enables also the application of abstract interpretation and static analysis techniques developed in the programming language community.
I. INTRODUCTION
Financial derivatives are an important tool of today’s finance
sector. Despite their often negative public perception after the
crisis of 2008, they are a tool — originally — developed to
reduce risks in trading real goods such as wheat or copper. But
at the same time financial derivatives introduce possibilities
to speculate over the value of something without owning the
actual something. Both uses lead eventually to their important
role in banking and investment. Naturally, financial derivatives
are a well studied topic in economics and mathematics, e.g.
[
But the interest to investigate financial contracts from a language perspective seems to be growing. In 2010 the U.S. Securities and Exchange Commission published a “concept release” with a request for comments, which included a proposal to require the publication of Python programs which represent the contract of Asset Backed Securities, a special kind of financial derivative contracts.
But what are financial derivatives? At first they are
contracts, i.e. legal documents defining rights and obligations
of two or more parties. Second, they are derived, i.e. the
rights and obligations defined by the contract depend on
some external variables. We call these external variables:
Observables. They differ from values defined in a contract
by their ability to change over time. E.g. possible observables
are the temperature at Kaiserslautern or the course of some
shares at some stock exchange. This notion of observables
was already used in [
Henceforth, financial derivative contracts are contracts which are based upon observables describing rights and obligations in terms of payed money from one party to another.
We will further restrict this notion to contracts between two parties. One of them is the holder, he becomes the holder by acquiring the derivative contract. The other party remains anonymous as we will always analyze contracts from the view point of the holder.
The last restriction we place on the notion of derivatives, is that the contracts under consideration may grant the right to choose between alternatives only to the holder of the contract.
The contributions of this article are:
1) An overview of work done in informatics, especially
from a software language point of view, on financial
derivatives.
2) A formal definition of a language — based on [
Section II covers the sparse related work in informatics.
Section III defines our language of derivative contracts, which
is an extension of the language of [
The earliest attempt at defining a software language for financial products, as far as we know, is a joint academic and industrial project resulting in the definition and implementation of RISLA. It is based on the insight, “that a product can be characterized by describing its cash flows.” [4, p. 2]. Its purpose was to simplify the integration of new financial products into the existing business software systems of banks. Therefore, the project developed a compiler from RISLA to COBOL, which generated the necessary routines to integrate a financial product into the existing software infrastructure. The focus on integrating financial products into business software systems lead to a language design containing information about the expected user interface in the business software system. RISLA was not used to analyze the contract or perform pricing1 on it. From the very sparse publicized documentation of it, it is not clear whether choices of the holder of a derivative are expressible or not.
1Pricing is a mathematical analysis which defines a notion of a fair price,
see e.g. [
In 2000, Peyton-Jones and Eber [
In [
Andersen, et al. present in [
In [
III. A LANGUAGE OF DERIVATIVE CONTRACTS
The language for contracts we are going to present has been designed to enable standard mathematical analysis, like option valuation, on contracts written in that language. But at the same time, we did not want to include any assumptions which are introduced by a certain approach of analysis. The language should also allow to resolve any ambiguities about contracts, such might occur e.g. in a text document describing a contract, but must not be possible in this language.
Such a formally defined language should also be amenable to a mathematical treatment of contracts. Such a treatment should include a notion of equality of contracts, that corresponds to our intuition about contracts in real life. Nevertheless, it has to be a mathematical equality, i.e. enabling the substitution of equals and the formulation of mathematical laws on derivative contracts.
Last but not least, a language of contracts should be composable and support abstraction, i.e. support the naming of recurring patterns of contracts. The goal to support composition and abstraction is compatible with the design, we present later in this section, but we will not discuss it in this paper. Instead we will focus on the goals mentioned before.
Before we come to the language definition of derivative contracts, we will have a look at several examples of derivatives specified in it.
bond is a contract granting the holder the right to receive an
amount of money k at a specified time t in the future. This
example has been taken from [
The meaning of this contract is the following. At time t, the holder acquires the contract Scale (Const k) One). Which is a contract granting the right to immediately receive k units of money. For a more detailed description of the keywords, see Section III-C.
derivative contract granting the holder the right but not the obligation to sell one item of e.g. a share of Siemens at a previously fixed price, here 100, at a predefined time, in this example 5.
(Or ( Scale ( Lift2 ( ) (Unknown ”Siemens”) (Const 100))) Zero) 3) Barriers: The previous derivative contains the possibility to achieve very high pay-offs when the value of a Siemens share drops to almost zero. Therefore, it is common to include, barriers into derivatives. E.g. a derivative contract could state, when the value of one Siemens share gets below 50, the complete option is void. This is easily expressed with Until : Until (Comp < (Unknown ”Siemens”) (Const 50)) (When (At 5) (Or ( Scale ( Lift2 ( ) (Unknown ”Siemens”) (Const 100))) Zero))
of options use the mean of price of a share to determine the payoff. In order to construct an observable expression which represents the average of some observable, we have to add the values of observable at different times. In order to allow this, our language contains the constructor Reduce.
(Reduce + (Between (5,10)) (Unknown ”Siemens”)) (Const 5) The observable above computes the average price of one Siemens share between time 5 and 10. Reduce collects all values of the third argument at times at which the second argument evaluates to true. These values are summed — the first argument. The initial value is the left neutral element of the given operation. The operation here is addition, therefore it is zero in this example.
These history dependent observables are not expressible in
the language in [
Our language for derivatives is based on the language in [
As usual N denotes the natural numbers including 0, Z denotes the positive and negative integers, R denotes the real numbers and B denotes the set of boolean values. We use V = Z [ R [ B as the values of observables. Every time t is element of N . And S denotes the set of names of unknown observables. These names are strings. We use the following convention for variable names: t 2 N , k; v 2 V, and n 2 S.
Fig. 1 contains the syntax definition of observable expressions in a style which is common in the programming language community. The single elements of the definitions are either mathematical statements m 2 f:::g or are algebraic data type declaration. In the following, o denotes, depending on the context, the set of all observable expressions, or one concrete expression.
Unknown n is an observable representing an external variable varying over time. In this work we will restrict the language to unknown observables with R as value domain.
Const k is an observable of value k 2 V for all times. Time is an observable with domain N . Its value is t at every time t.
Lift u o is the application of a unary operator u on o. Lift2 b o1 o2 is the application of a binary operator b on o1 and o2.
2Although, we don’t present the language as an Haskell-embedded domain specific language our implementation is done as an Haskell-embedded domain specific language. We deliberately choose not to discuss such an embedding and the resulting benefits in this paper. Such benefits would include added expressiveness, modularization and abstraction capabilities, and a simplified implementation.
Comp m o1 o2 is the comparison of o1 and o2 with the comparison operator m at every point in time.
C2D o is the conversion of a continuous-valued observable o, i.e. an observable with domain R, to a discretevalued observable, i.e. an observable with domain N . D2C o is the conversion of a discrete-valued observable o, i.e. an observable with domain N , to a continuousvalued observable, i.e. an observable with domain R. Reduce s o1 o2 is the fold with the binary function s over the sequence of values of o2 at, when o1 evaluates to true. The start value of the fold is the left neutral element of the function s.
At t is syntactic sugar for: Comp (==) Time (Const t). Between (t1,t2) is syntactic sugar for: Lift2 (&&) (Comp (<=) (Const t1) Time) (Comp (<) Time (Const t2))
Fig. 2 defines the syntax of contracts. We’ll give an informal description of the meaning of the constructs here: Zero is the contract which grants no rights and no obligations.
One is the contract which grants the holder the right to receive one unit of money at the time of acquisition. Scale o c is a contract which is the same as c with every payment multiplied by the value of the observable o at the time of the payment.
And c1 c2 is the contract which grants all rights and obligations of both c1 and c2 at the same time.
Or c1 c2 is the contract which grants the holder the right to choose at time of acquisition to acquire either c1 or c2.
Cond o c1 c2 is the contract which grants depending on the value of the boolean observable o at time of acquisition either all rights and obligations of c1, if o is true, or c2, if o is false.
When o c is the contract which acquires the contract c at the first time the boolean observable o becomes true. Anytime o c is the contract which grants the holder at every time the boolean observable o is true the right to decide whether he wants to acquire c and release the complete contract Anytime o c or not.
Until o c is the contract which grants the holder the right to choose between keeping his contract or acquiring c and releasing the complete contract. But this right is only granted as long as the boolean observable o is false. When o becomes true the whole contract becomes equivalent to Zero identical.
The language for derivative contracts is typed. But, because it has a completely standard type system, we omit a formal definition. We describe it only informally:
Every observable expression o has a one of three types: discrete, continuous, and boolean. Their value sets are Z, R, and B. All unary operators take arguments of one type and c ::= j j j j j j j j return the same type. All binary and comparison operators take two arguments of the same type. Binary operators return the same type as their arguments and comparison operators always return boolean. C2D and D2C are the only ways to convert or cast observables. Contracts c have no type, the observable arguments of the contract constructors are of type continuous, if not given otherwise in the description of the contract constructors above.
In this section, we’ll give a formal denotational semantics
for our language of contracts, for an overview on denotational
semantics see e.g. [
Semantics of formal language haven been studied for a
long time. The largest fraction of the literature on this topic
probably covers semantics of formally specified logics and
programming languages. Applying these techniques to other
kinds of languages is not new but certainly not widespread. In
the context of contract languages, we are aware of only one
previous article which gave formal denotational semantics for
a contract language: [
We choose to give a denotational semantics, because a denotational semantics provides a straight forward notion of equality, and because it is quite naturally defined for our derivative contracts.
A denotation of unknown observables is a function from time to values, N ! V. Therefore, an environment, i.e. a mapping of names to their denotation, is a function from e : S ! N ! V. An environment represents the values of all unknown observables of a contract for all times. Therefore, the denotational semantics of observable expression is a function:
J K : o ! (S ! N ! V) ! (N ! V) We write J K
o e to denote the semantics of an observable expression o applied to an environment e. With an additional
J K is defined as followsJ3o:Kte. time argument t we write
JConst kKte
JTimeKte J Lift u oKte
JD2C oKte
JC2D oKtte J Lift2 b o1 o2Ke
t JComp m o1 o2Ke
JReduce s o1o2Kte | {dz } = e n t = k = t = = = = = u JoKte JoKte m 8 init(s) = <
JdKte 1 : JdKte 1 s Jo2Kte if t < 0 if Jo1Kte = f alse if Jo1Kte = true init(s) denotes the left neutral element of s.
In the following the notation xb will denote a set of x. We define the domain D of the denotation of contracts as the largest fixed point of the following recursive algebraic data type equation.
p = o 2 pb 2 is the only constructor of this data type, it has two arguments, the first is an element of V, the second is a finite set of application of this constructor. Therefore, this data type coinductively defines the domain of all denotation of contracts. It is a forest of infinite height n-ary trees which are marked with elements of V. The depths of a node of the forest is the time at which the mark of the node is payed to the holder of a contract. E.g. f17 2 0 2 : : : g is the denotation of a contract which grants the holder the right to receive a payment of 17 money units at time 0 and a payment of zero money units at time 1.
The branching of the trees denotes the choices the holder of the contract has.
The empty denotation which consists only of payments of 0 units of money is abbreviated as . It is largest fixpoint of the following equation:
= f0 2 g
We need the following auxiliary functions on D, before we are able to define the denotational semantics.
pb qb = ¦(p + q) 2 (pÒ0 o te pb = ¦(JoKte v) 2
adds two elements of D such that both arguments are combined into one, as if they were both executed. qb0) (p 2 pÒ0) 2 pb; (q 2 qb0) 2 qb© (o te+1 pÒ0) (v0 2 pÒ0) 2 pb© 3We use a curried function application notation which does not use parenthesis
JOneKte JAnd a bKte
JOr a bKte
JScale o cKte JCond c a bKte
J|Whe{dnz b }cKte
| {dz }
J|Unt{idlz b }cKte = = = = = = = = = JoaKtete J[cKJJtebbKKtete § JbKte if JcKte = f alse
JcK2te JdifKteJ+c1Kte = true
JaKte § f0 g if JbKte = f alse
if JbKte = true § Jfc0K2te[JdfKte+1g
0 2 JdKte+1g § JcKte [ f0 2 JdKte+1g te multiplies every payment of an element of D with the current value of an observable expression.
Now, we are able to define the denotation of contracts, which is the following function: c : (S ! N J K ! V ) ! N ! D horizon, because there is no time at which we can guaranty, that the price of a Siemens share has been at least once smaller than the price of a Daimler share.
(Comp < (Unknown ”Siemens”) (Unknown ”Daimler”)) One
When we return to the example of Sec. III-B.2, we can now determine the following: Let x be the price of one Siemens share at time 5 as determined by e, i.e. JUnknown ”Siemens”Ke5 = x, and let c be the referenced example contract, then JcKte = f0 2 f0 2 f0 2 f0 2 f0 2 ( [ f(x 100) 2 g)ggggg
The denotation tells us that this European put option is a contract, which can be described as a sequence of 5 payments of zero amounts of money, followed either by an infinite sequence of zero-valued payments or by a payment of value x 100 followed by an infinite sequence of zero-valued payments.
We define the equality of two contracts a and b, now as follows:
a = b if and only if 8e:JaKe0 = JbKe0
Now, we have a notion of equality which is not tied to the syntax of contracts or observables, instead we claim it is tied to the intended meaning, we associate with a contract. Yet, we have a mathematical definition of this equality notion.
Most contracts in real life have a maximal life time. The same is true for derivative contracts in finance. We are going to define a notion of a horizon, which will be the earliest time after which nothing interesting may happen.
The smallest time t for which the following equation holds is called the horizon of a contract c. 8t0:t0 > t =) 8e:9pbi2f1:::ng:JcKte0 = f0 2 pÒ1; : : : ; 0 2 pcng
Note: Such a horizon t doesn’t have to exist for every contract c, while most practical contracts do have a defined horizon. The following contract does not have a defined V. APPLICATIONS, FUTURE WORK AND CONCLUSIONS
As we said in Sec. III-A, we wanted to design a language
which can be used to do option pricing, but which is not tied
to one approach. So far, we have implemented option pricing
for a subset with help of Qian Liang and Stefanie Mu¨ ller based
on [
Our language and denotational semantics could also be used to apply abstract interpretation or some specialized variants of if JbKte = f alseit to derivative contracts. That could allow to compute worst if JbKte = true or best case scenarios. Or it could allow to determine whether there is horizon, at which times decision have to be made by if JbKte = f alsethe holder, and much more. if JbKte = true The semantics itself allows to develop a calculus of contracts, which allows to transform contracts in order to simplify other analysises for example.
We have designed a language to express financial
derivatives, which is more general than the language of [