ContractSemantics.tex

\documentclass[xcolor=dvipsnames,11pt]{beamer} 

\mode<presentation>
{
\usetheme{Malmoe}
\useinnertheme{rounded}
\usecolortheme{beaver} 
\usecolortheme[named=Mahogany]{structure} 
}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}

\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}

\usepackage{graphicx}

\usepackage{listings}
\usepackage{color}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5
\newcommand{\comment}[2]{{\tiny \color{Orange}{$\spadesuit${\bf #1: }{\sf #2}$\spadesuit$}}}
%\renewcommand{\comment}[2]{}

\newcommand{\jbcomment}[1]{\comment{JB}{#1}}
\newcommand{\pbcomment}[1]{\comment{PB}{#1}}
\newcommand{\mecomment}[1]{\comment{ME}{#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5
\lstloadlanguages{ML,C}
% auto-colorisation with listings, handy for known languages...
\lstdefinestyle{smlstyle}{
      basicstyle=\ttfamily\scriptsize,
      keywordstyle=\color{violet},
      literate={->}{$\rightarrow$}1,
      stringstyle=\color{gray},
      identifierstyle=\color{blue},
      commentstyle=\color{red}\ttfamily,
      mathescape,
      language=ML
}
\lstnewenvironment{mlcode}
   {\lstset{basicstyle=\scriptsize,style=smlstyle,frame=tlrb}}
   {}
\lstnewenvironment{mlcodesmall}
   {\lstset{basicstyle=\tiny,style=smlstyle,frame=tlrb}}
   {}
\lstset{style=smlstyle,keepspaces=true,breaklines=false}\newcommand{\cd}[1]{\lstinline$#1$}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\emph}[1]{\textcolor{structure!90}{#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% change here to change all
\newcommand{\ttt}[1]{\mbox{\cd{#1}}}

% smart constructors
\newcommand{\zero}{\ttt{zero}}
\newcommand{\transfOne}{\ttt{transfOne}}
\newcommand{\scale}{\ttt{scale}}
\newcommand{\transl}{\ttt{transl}}
\newcommand{\both}{\ttt{both}}
\newcommand{\ifff}{\ttt{iff}}
\newcommand{\checkWithin}{\ttt{checkWithin}}

\title{A Small Multi-Party Contract Language}
\author[Bahr,Berthold,Elsman,Henglein]{Patrick Bahr, Jost Berthold, Martin Elsman, Fritz Henglein}

\begin{document}

\frame[plain]{\titlepage}

\begin{frame}[fragile,t]
    \frametitle{Outline}

\begin{itemize}
\item Expressions and contracts
\item Example contracts
\item Contract equivalences and semantics
\item Contract causality
\item Contract utilities
\item Discussion of future work\\
\item Appendix: Contract semantics
\end{itemize}
\end{frame}

\begin{frame}[fragile,t]
    \frametitle{Contract Language Goals}

\textbf{Compositionality}. 
\begin{quote}
Contracts are time-relative, which makes compositionality
straightforward.
\end{quote}

\textbf{Multi-party}.
\begin{quote}
A contract specifies the contractual obligations and opportunities for
multiple parties, which opens up the possibility for specifying
portfolios.
\end{quote}

\textbf{Contract management}.
\begin{quote}
Contracts can be managed; gradually, a contract reduces to the ``empty
contract''.
\end{quote}

\textbf{Contract utilities}.
\begin{quote}
Contracts can be analyzed in a variety of ways...
\end{quote}

\end{frame} 

\begin{frame}[fragile,t]
    \frametitle{Expressions and Intuitive Semantics}

\begin{mlcode}
  type 'a exp                     (* Expressions          *)
  type bexp = bool exp            (* Boolean expressions  *)
  type 'a num 
  type 'a nexp = 'a num exp       (* Numeric expressions  *)
  type rexp = real nexp           (*  real expressions    *)
  type iexp = int nexp            (*  integer expressions *)
 
  val I   : int -> iexp
  val R   : real -> rexp
  val B   : bool -> bexp
  val $\oplus$  : 'a nexp * 'a nexp -> 'a nexp  (* max, +, ... *)
  val obs : string * int -> rexp
\end{mlcode}

\begin{description}
\item[I d] is the integer constant $d$.
\item[R r] is the real (i.e., double) constant $r$.
\item[$e_1$ !-! $e_2$] represents the result of subtracting the results of two subexpression.
\item[obs(s,d)] represents the value of the underlying ``s'' in $d$ days.
\end{description}

\end{frame}

\begin{frame}[fragile,t]
    \frametitle{Contract Constructors and Intuitive Semantics}

\begin{mlcode}
  type cur val EUR : cur val USD : cur    (* currencies *)
  type party = string                     (* parties *)
  type contr                              (* contracts *)
  val zero        : contr             
  val transfOne   : cur * party * party -> contr
  val scale       : rexp * contr -> contr
  val transl      : int * contr -> contr
  val both        : contr * contr -> contr
  val iff         : bexp * contr * contr -> contr
  val checkWithin : bexp * int * contr * contr -> contr
\end{mlcode}

\begin{description}
\item[transfOne] is a cash flow (which happens immediately)
\item[scale] scales a cash flow by an expression (of type \cd{rexp})
\item[transl] postpones a contract into the \emph{future}.

    The \cd{int} argument must be positive!

\item[checkWithin] repeatedly checks a condition (of type \cd{bexp}) for a number of days.
    The \cd{int} arg. must be positive!
\end{description}
\end{frame}

\begin{frame}[fragile,t]\frametitle{Example --- Vanilla Option}

\begin{mlcode}
val equity = "Carlsberg"  (* Carlsberg stock call option *)
val maturity = 12 * 30
val ex4 =
    let val strike = 50.0
        val nominal = 1000.0
        val obs = max(R 0.0, obs(equity,0) !-! R strike)
    in scale(R nominal,
             transl(maturity,
                    scale(obs,transfOne(EUR,"you","me"))))
    end
\end{mlcode}

\textbf{Cash flows in 360 days:}

\begin{scriptsize}
\begin{verbatim}
Cashflows:
2013-12-26 Certain [you->me] EUR (1000.0*max(0.0,(Obs(Carlsberg@0)-50.0)))
\end{verbatim}
\end{scriptsize}
\end{frame}

\begin{frame}[fragile,t]\frametitle{Example --- Barrier Touch Option}
\textbf{Instrument:}
\begin{mlcode}
datatype kind = Up | Down
fun fxTouch buyer seller curSettle amount
                   (cur1,cur2) barrier kind expiry =
  let val rate = fxRate cur1 cur2
      val cond = case kind of
                    Up   => R barrier !<! obs (rate,0)
                  | Down => obs (rate,0) !<! R barrier
      val tr   = transfOne (curSettle, buyer, seller)
  in checkWithin (cond, expiry,
                  scale (R amount, tr),
                  zero)    (* pay only if barrier is hit *)
  end
\end{mlcode}

\textbf{I buy a EUR 1000 1Y EUR/USD barrier touch Up-option:}
\begin{mlcode}
val touch =
 fxTouch "me" "you" EUR 1000.0 (EUR,USD) 1.0 Up y1
\end{mlcode}

\textbf{Contract simplifies to:}
\begin{scriptsize}
\begin{verbatim}
CheckWithin(1.0 < Obs(FX EUR/USD@0), y1, 
            Scale(1000.0,TransfOne(EUR,me,you)), zero)
\end{verbatim}
\end{scriptsize}
\end{frame}

\begin{frame}\frametitle{Basic Contract Equivalences}{\footnotesize

\begin{columns}
\column{0.35\textwidth}
\begin{align*}
    \transl(d,\zero)             &=  \zero\\
    \scale(r,\zero)              &=  \zero\\
    \both(\zero,\zero)           &=  \zero\\
    \scale(0,c)                  &=  \zero\\
\end{align*}

\column{0.65\textwidth}
\begin{align*}
    \ifff(c,\zero,\zero)        &= \zero\\[0.5ex]
    \ifff(T,c_1,c_2)            &=  c_1\\
    \ifff(F,c_1,c_2)            &=  c_2\\[0.5ex]
    \checkWithin(b,0,c_1,c_2)   &= \ifff(b,c_1,c_2) \\
\end{align*}
\end{columns}

\begin{align*}
    \scale(s_1,\scale(s_2,c))    &=  \scale(s_1\cdot s_2,c)\\
    \transl(d_1,\transl(d_2,c)   &=  \transl(d_1+d_2,c)\\[1ex]
    \transl(d,\both(c_1,c_2)     &=  \both(\transl(d,c_1),\transl(d,c_2))\\[1ex]
\end{align*}

}\end{frame}


\begin{frame}[t] \frametitle{Complex Contract Equivalences}

\emph{\textbf{Expression promotion:}}

Expressions involving observables can be \emph{promoted} from a time later to a time earlier:
%
\hfill {\footnotesize $(e \in \ttt{iexp} \cup \ttt{rexp} \cup \ttt{bexp},\ d \in \mathbb{Z})$}

{\footnotesize 
$$ e / d = \left \{
\begin{array}{ll}
obs(s,\emph{d+i}) :& e = \emph{obs(s,i)}\\
e_1/d \oplus e_2/d :& e = e_1 \oplus e_2\\
\ldots
\end{array}
\right .$$
}

An expression is \emph{certain} if it does not depend on observables.
\medskip

\hrule
\medskip

\emph{\textbf{\ldots enables equivalences with \cd{transl}}}

{\footnotesize
\begin{align*}
    \transl(d,\scale(s,c))       &=  \scale(s/d,\transl(d,c))\\
    \transl(d,\scale(s,c))       &=  \scale(s,\transl(d,c))\  \mbox{if } s \mbox{ is certain}\\
%
  \transl(d,\checkWithin (b, e, c_1, c_2))  &=  \\
                             \checkWithin &(b/d, e, \transl(d,c_1), \transl(d,c_2))\\[1ex]
  \transl(d,\ifff(b,c_1,c_2))  &=  \ifff(b/d, \transl(d,c_1), \transl(d,c_2))\\
\end{align*}
}

\end{frame}

\newcommand{\crule}[3]{\frac{#2}{#3}\ \mbox{\scriptsize \it #1}}
\newcommand{\sem}[1]{[\![#1]\!]}
\newcommand{\csem}[3]{\mathcal{C}\sem{#1}#2 & = #3}

\begin{frame}
    \frametitle{Formal Semantics: Sequence of Cash Flow Sets}

The \emph{semantics of an expression} is (partially) defined with
respect to an environment ($\ttt{env}$), containing fixings for
observables and choices:
\vspace*{-2ex}

{\footnotesize
\begin{align*}
  \mathcal{E} & : \ttt{bexp} \times \ttt{env} \rightarrow \ttt{bool}\\
    \mathcal{E} & : \ttt{iexp} \times \ttt{env} \rightarrow \ttt{int}\\
  \mathcal{E} & : \ttt{rexp} \times \ttt{env} \rightarrow \ttt{real}
\end{align*}}
\vspace*{-2ex}

A \emph{cash flow} is a tuple \cd{(amount:real, c:currency, from:party, to:party)}.

\vfill 
The \emph{semantics of a contract} is (partially) defined, with respect
to an environment, as a series of cash flow sets:

$$ \mathcal{C} : \ttt{contr} \times \ttt{env} 
          \rightarrow \mathbb{P}(\ttt{flow})^\mathbb{N}$$

\vfill
See appendix for a full definition of contract semantics.

\end{frame}

\begin{frame}[fragile,t]
    \frametitle{Contract Causality}

 A \emph{causal contract} is a contract with the property that during all
   possible executions of the contract, a cash flow cannot depend on a
   future fixing (of an observable).

\vfill

\emph{Example of a non-causal contract:}

\begin{mlcode}
iff( obs("CarlsbergDKR",2) !>! R 50.0,
                              transfOne(EUR, me, you), zero)
\end{mlcode}
{\footnotesize
\begin{quote}
  If, \emph{on the day after tomorrow}, 
           the Carlsberg stock is worth more than 50~kr.,
           I give you one EUR \emph{today}.
\end{quote}}

\vfill

\emph{Goal}: Define a static contract causality analysis that, for many useful contracts,
guarantees causality (see appendix).
\end{frame}

\begin{frame}
\frametitle{Supported Instruments}
\begin{itemize}
\item Basic swaps, fx-swaps
\item Fx-forwards
\item Vanilla options, fx-options, fx-barrier-touch options, fx-barrier-no-touch options, fx-double-barrier-in/out, fx-single-barrier-in/out
\item Asian options (not yet supported; observable average computation needed)
\item American options (supported using $\ttt{checkWithin}$)
\item Barrier options with fixed maturity (not yet supported)
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Utilities}

\textbf{Available features}:
\begin{itemize}
  \item Applying fixings
  \item Advancing a contract in time
  \item Finding cash flows
  \item Eliminating transfers to and from a particular party
  \item Merging parties
\end{itemize}
\end{frame}


\begin{frame}[fragile,t]
\frametitle{Example Portfolio of Touch Options}

\begin{mlcodesmall}
val touchOptions = all
 [fxTouch   "C" "us" USD  400000.0 (USD,SEK) 6.90 Up   m6
 ,fxTouch   "D" "us" USD  600000.0 (USD,SEK) 6.15 Down m12
 ,fxNoTouch "A" "us" USD 1400000.0 (USD,SEK) 6.70 Up   m6
 ,fxNoTouch "B" "us" USD 1600000.0 (USD,SEK) 6.25 Down m12]

val env = fixings ("FX USD/SEK",today) 
   [6.6,6.7,6.8,6.9,6.8,6.7,6.6,6.5,6.4,6.3,6.2,6.1]

val allTouch = simplify (env,today) allTouch
val () = ppCashflows (today, allTouch)
\end{mlcodesmall}

{\scriptsize
Two touch options will be triggered (barriers up 6.9, down 6.15).

Two no-touch options will be canceled (barriers up 6.7, down 6.25).
}
\vfill
\emph{Result:}
\begin{verbatim}
2014-01-03 Certain [C->us] USD 400000.0
2014-01-11 Certain [D->us] USD 600000.0
\end{verbatim}

\end{frame}

\begin{frame}
\frametitle{Future Work}

\textbf{Next steps}:
\begin{itemize}
  \item Focusing / Defocusing  (e.g., resolution: day-week-month).
  \item Pattern matching to identify standard contracts.
  \item Adding strategies (at another level)
  \item CVA
  \item Finding ``branch-boundaries'' in conditionals.

      \emph{Goal:} generate tree of scenarios with fixings.
\end{itemize}
\end{frame}

\frame{\Huge APPENDIX}
\begin{frame}
    \frametitle{Appendix: Formal Semantics: Contracts}

Expression promotion is generalised to environments: 
{\footnotesize
\begin{center}
$\ttt{env/d}$ promotes all fixings by $d$ days.
\end{center}}

Cash flows ($\ttt{flow}$): \cd{(amount:real, c:currency, from:party, to:party)}.

\vfill

Contract semantics \hfill \framebox{$ \mathcal{C} : \ttt{contr} \times \ttt{env} 
          \rightarrow \mathbb{P}(\ttt{flow})^\mathbb{N}$}

\vspace{-2ex}
{\footnotesize
\begin{align*}
\csem{\zero}{e}{\ttt{repeat}\ \emptyset}\\
\csem{\transfOne(c,p_1,p_2)}{e}{\{(1,c,p_1,p_2)\} :: \ttt{repeat}\ \emptyset }\\
\csem{\both(c_1,c_2)}{e}{\ttt{zipWith flowMerge }\ (\mathcal{C}\sem{c_1}e)\ (\mathcal{C}\sem{c_2}e)}\\
\csem{\scale(s,c)}{e}{\ttt{mapmap}\ (\lambda (a,c,f,t)\mapsto(a\cdot\mathcal{E}\sem{s}e,c,f,t))\ (\mathcal{C}\sem{c}e)}\\
\csem{\transl(d,c)}{e}{\ttt{replicate}\ d \ \emptyset +\!\!\!+\  \mathcal{C}\sem{c}(e/d)}\\
\csem{\checkWithin(b,d,c_1,c_2)}{e}{
\left \{
\begin{array}{rl}
\mathcal{C}\sem{c_1}e & \mbox{iff}\ \mathcal{E}\sem{b}e \\
\mathcal{C}\sem{c_2}e & \mbox{iff}\ d = 0\ \wedge\ !\mathcal{E}\sem{b}e  \\
\emptyset :: L & \mbox{iff}\ d > 0\ \wedge\ !\mathcal{E}\sem{b}e \ \wedge \\
& L = \mathcal{C}\sem{\checkWithin(b,d\!-\!1,c_1,c_2)}(e/1)
\end{array}\right.
}
\end{align*}
}

\end{frame}

\begin{frame}
    \frametitle{Appendix: Expression Causality}

\emph{$b$-causality} $ b \vdash e$ for \emph{expressions}:
{\scriptsize $ (b \in \mathbb{Z}_0^+, \ e \in \ttt{expr0})$}

\begin{columns}
\column{0.1\textwidth}
\emph{Axioms:}
\column{0.35\textwidth}
$$\crule{(Obs)}{}{max(0,i) \vdash \ttt{obs}(s,i)}$$
%\jbcomment{b non-negative to use 0 as lowest value: How about $\forall b\in\mathbb{Z}: b\vdash Literal$}
\column{0.2\textwidth}
$$\crule{(Lit)}{e \mbox{ is a literal}}{0 \vdash e}$$
\end{columns}


\begin{columns}
\column{0.1\textwidth}
\emph{Propagation:}
\column{0.35\textwidth}
$$\crule{(BinOp)}{b_1 \vdash e_1\ \ b_2 \vdash e_2 }{max(b_1,b_2) \vdash e_1 \otimes e_2}$$

\column{0.2\textwidth}
$$\crule{(UnOp)}{b \vdash e}{b \vdash \ominus e}$$
\end{columns}

\medskip
\hrule
\medskip

\emph{Intuition:} $i \vdash e$ indicates the smallest $i$ such that no observable in $e$ is observed \emph{after more than $i$ days}.

\end{frame}

\begin{frame}[t]
    \frametitle{Appendix: Contract Causality}

\emph{$d$-causality} $ d \vdash c$ for contracts:
{\scriptsize $ (d \in \mathbb{Z}_0^+, \ c \in \ttt{contr})$}

\begin{columns}
\column{0.3\textwidth}
\begin{align*}
\crule{(Zero)}{}{\infty \vdash \zero}&\\[1ex]
\crule{(TO)}{}{0 \vdash \transfOne(C,p_1,p_2)}&\\[1ex]
\crule{(TL)}{b \vdash c}{b + d \vdash \transl(d,c)}&\\[1ex]
\end{align*}

\column{0.3\textwidth}
\begin{align*}
&\\[1ex]
&\crule{(Sc)}{b_1 \vdash e\ \ \ b_2\vdash c\ \ \ b_1 \leq b_2 }{b_2 \vdash \scale(e,c)}\\[1ex]
&\crule{(Both)}{b_1 \vdash c_1\ \ \ b_2 \vdash c_2}{min(b_1,b_2) \vdash \both(c_1,c_2)}%\\[1ex]
\end{align*}
\end{columns}
$$ 
\crule{(CW)}{0\vdash e\ \ \ b_1 \vdash c_1\ \ \ b_2 \vdash c_2}{min(b_1,d+b_2) \vdash \checkWithin(e,d,c_1,c_2)}
$$

\medskip
\hrule
\medskip

\emph{Intuition:} $i \vdash c$ means c is causal (\textit{SC} rule) and there are no transfers before $i$ days have passed (\textit{TL} rule and using \textit{min}).

\end{frame}

\begin{frame}[fragile,t]
    \frametitle{Appendix: Contract Horizon}

\emph{$d$ is the horizon} of a contract: $ c \dashv d$:
{\scriptsize $ (c \in \ttt{contr},\ d \in \mathbb{Z}_0^+) $}

\begin{columns}
\column{0.3\textwidth}
\begin{align*}
\crule{(H-Zero)}{}{\zero \dashv 0}&\\[1ex]
\crule{(H-TO)}{}{\transfOne(C,p_1,p_2)\dashv 0}&\\[1ex]
\crule{(H-TL)}{c \dashv i }{\transl(d,c) \dashv (i + d) }&\\[1ex]
\end{align*}

\column{0.3\textwidth}
\begin{align*}
&\\[1ex]
&\crule{(H-Sc)}{b_1 \vdash e\ \ \ c \dashv b_2\ \ \ b_1 \leq b_2 }{\scale(e,c) \dashv b_2 }\\[1ex]
&\crule{(H-Both)}{c_1 \dashv b_1 \ \ \ c_2 \dashv b_2 }{\both(c_1,c_2) \dashv max(b_1,b_2) }\\[1ex]
\end{align*}
\end{columns}
$$ 
\crule{(H-CW)}{0\vdash e\ \ \ c_1 \dashv b_1 \ \ \ c_2 \dashv b_2 }{\checkWithin(e,d,c_1,c_2) \dashv (d + max(b_1,b_2)) }
$$

\medskip
\hrule
\medskip

\emph{Intuition:} $c \dashv i$ means the last transfer may happen after no more than $i$ days (\textit{H-TL} and \textit{max}). c may or may not be causal (\textit{H-SC}).

\end{frame}

\begin{frame}[fragile,t]
    \frametitle{Appendix: Contract Language Implementation}
\emph{Expression Datatype}
\begin{mlcode}
type party = string                       
datatype exp0 = I of int  (* data structure for expressions *)
              | R of real (*  - numeric or boolean *)
              | ...
              | BinOp of string * exp0 * exp0
              | ...
              | Obs of string * int     (* observable *)
              | ChosenBy of party * int (* active choice *)
\end{mlcode}

\emph{Contract Datatype}\footnote{Interface functions are ``smart constructor'' version of the above
constructors.}
\begin{mlcode}
datatype contr =
       Zero
     | TransfOne of cur * party * party
     | Scale of exp0 * contr
     | Transl of int * contr
     | Both of contr * contr
     | If of exp0 * contr * contr
     | CheckWithin of exp0 * int * contr * contr
\end{mlcode}
%datatype contr =
%       Zero
%     | TransfOne of cur * party * party (* immediate cash flow *)
%     | Scale of exp0 * contr            (* scaling by an expr. *)
%     | Transl of int * contr            (* postpone to later *)
%     | Both of contr * contr            (* combine two contracts *)
%     | If of exp0 * contr * contr       (* choice between two contracts *)
%     | CheckWithin of exp0 * int * contr * contr
%               (* monitoring of a condition (expr.) within a duration 
%                  if true within time: first contract, otherwise second *)
%


\end{frame}

\end{document}