Actus Specification
1 Overview
This blueprint is a machine-checked re-authoring of the ACTUS Technical Specification — the algorithmic standard for representing financial contracts by their cash flows. It reproduces the standard’s normative content (notations, utility functions, observers, and the per-contract schedule, state-initialisation, state-transition and payoff tables) and links every definition to a Lean 4 formalization, so that the document is at once the specification and its proof of internal consistency.
It covers all eighteen contract types of the standard (§5). Every stateful contract — the lending family (PAM, LAM, NAM, ANN, CLM) together with the exotic amortizer LAX, the plain-vanilla swap SWPPV and the non-maturity deposit UMP — is modeled twice: relationally (the inductive Step, the readable spec) and functionally (computable state-transition and payoff functions), with the two proven to agree. The remaining types — positions, derivatives, composite swaps (SWAPS), and credit enhancement — are direct cash-flow builders over the shared schedule-generation engine.
The whole development is generic over the amount type and instantiated twice: at Float for the executable engine — validated against the ACTUS reference test suite, where it reproduces all \(236\) gated reference contracts (\(3155\) cash flows) exactly — and at the real numbers \(\mathbb {R}\) for the quantitative metatheorems of §6. The order/field structure those bounds need exists over \(\mathbb {R}\) but not over Float (where \(\mathtt{NaN}\) even breaks \(a \le a\)), so they are genuine theorems over \(\mathbb {R}\) rather than empirical checks.
Provenance. The normative formulas and tables are derived from the ACTUS Technical Specification, © 2018–present ACTUS Financial Research Foundation, distributed under the Creative Commons Attribution–ShareAlike 4.0 licence; this re-authoring is a derivative work under the same licence.
2 Notations
2.1 Contract attributes
Contract attributes are the legal contractual terms that define a contract’s exchange of cash flows; they are catalogued in the ACTUS data dictionary and referenced here by their dictionary short names in typewriter font, e.g. \(\texttt{IED}\) for the initial exchange date. Vector-valued attributes are indexed with a subscript: the \(i\)-th element of \(\texttt{ARPRANX}\) is \(\texttt{ARPRANX}_i\).
2.2 The \(\varnothing \)-operator
The symbol \(\varnothing \) marks a quantity as undefined: an optional attribute that carries no value, or a schedule that contains no times (\(\vec{t}^{IP}=\varnothing \) is the empty schedule). In the Lean development this is the Option type; an absent term is none.
2.3 \(t_0\)-time and state variables
\(t_0\) denotes the contract’s status date \(\texttt{SD}\) — the time as of which its terms and implied state are represented; the contractual logic determines events and states for all \(t{\gt}t_0\). State variables describe the contract state at a time \(t\); they are written capitalised and bold and indexed by time, e.g. \(\mathbf{Nt}_{t}\) is the outstanding notional principal at \(t\). The Lean counterpart is a State record carrying Nt, Ipnr, Ipac, Feac, Nsc, Isc, Sd, etc.
2.4 Contract events, STF and POF
A contract event \(e_t^k\) is a scheduled or unscheduled occurrence at time \(t\) of type \(k\), carrying an event time and a payoff \(c\in \mathbb {R}\), retrieved by \(\tau (\cdot )\) and \(f(\cdot )\) respectively. Two functions act on an event: the state-transition function \(\mathrm{STF}\_ k\_ CT()\) maps the pre-event state to the post-event state, and the payoff function \(\mathrm{POF}\_ k\_ CT()\) yields the cash flow \(f(e_t^k)\). Both are specific to an event type \(k\) and a contract type \(CT\). In Lean these are the per-contract stf and pof functions; the relational Step is the graph of stf.
Plain/primed state in a transition.
The per-contract tables of Section 5 use a light convention in place of the standard’s \(t^-/t^+\) time decorations: a plain state symbol denotes its pre-event value (written \(\mathbf{\cdot }\), the standard’s \(\mathbf{\cdot }_{t^-}\)) and a primed symbol its post-event value (\(\mathbf{\cdot }’\), the standard’s \(\mathbf{\cdot }_{t^+}\)). An assignment such as \(\mathbf{Nt}’=\mathbf{Nt}-\dots \) then reads “new notional \(=\) old notional \(-\dots \)”; a primed symbol may also appear on the right-hand side when an update depends on a value already revised earlier in the same event. For the interest-bearing contracts we further abbreviate the interest accrued on the outstanding notional since the last state date by
the year fraction from the last state date \(\mathbf{Sd}\) to the event time \(t\) times the nominal rate \(\mathbf{Ipnr}\) times the notional \(\mathbf{Nt}\); this term recurs in almost every transition below.
2.5 Event sequence and contract lifetime
Events occurring at the same time are ordered by a fixed event-sequence indicator, so that their STFs and POFs compose deterministically. A contract’s lifetime runs from \(\texttt{SD}\) to \(\min (\texttt{MD},\texttt{AMD},PR^*,\texttt{STD},\texttt{TD},t^{max})\), where \(PR^*\) is the principal-redemption event that drives \(\mathbf{Nt}_{}\) to \(0\); terms that do not apply to a given contract are taken as \(+\infty \), and \(t^{max}\) optionally bounds the analysis horizon for contracts without a natural end (e.g. STK).
3 Utility functions
The standard is built on a small layer of utility functions shared by every contract. The development is generic over the amount type \(\alpha \) (an ordered field for the metatheorems, Float for the engine).
The schedule function maps an anchor \(s\), a cycle \(c\) and an end date \(T\) to the cyclic sequence
with \(t_i{\lt}t_{i+1}\). Cycles have the form \(NPS\) (\(N\) an integer, \(P\in \{ D,W,M,Q,H,Y\} \) a period unit, \(S\in \{ +,-\} \) a stub rule). An optional boolean \(B\) in \(S(s,c,T,B)\) controls whether the end date \(T\) belongs to the schedule, and the EOMC/BDC conventions (below) may shift the resulting times, so the sequence need not be equidistant.
Array schedules generalise \(S\) to vector inputs \(\vec{s}=(s_0,\dots ,s_m)\), \(\vec{c}=(c_0,\dots ,c_m)\):
coinciding with \(S\) for \(m=1\). Used by LAX (§5.3).
The end-of-month convention EOMC fixes whether cyclic times anchored on a short month-end fall on the same day or the month-end; the business-day convention BDC shifts a time off a non-business day (following/preceding, modified or not, calculate-before or -after the shift); and the business-day calendar \(B:t\mapsto \{ \text{true,false}\} \), selected by CLDR, decides which days are business days (NoHoliday, MondayToFriday, …).
The year-fraction interface \(Y:s,t,\texttt{DCC}\mapsto \mathbb {R}\) gives the fraction of a year between two times under a day-count convention DCC (Actual/360, Actual/365, 30E/360, Actual/Actual ISDA, Business/252). Per-annum rates are accrued by multiplying with \(Y\).
The contract-role sign \(R:\texttt{CNTRL}\to \{ -1,+1\} \) maps a contract role to \(+1\) for a claim (asset) or \(-1\) for an obligation, fixing the direction of every role-sensitive cash flow and state (a positive flow runs from CPID to CRID). E.g. \(\texttt{RPA}\mapsto +1\), \(\texttt{RPL}\mapsto -1\), \(\texttt{GUA}\mapsto -1\), \(\texttt{OBL}\mapsto +1\). We abbreviate \(R(\texttt{CNTRL})\).
The annuity amount sizes the constant ANN instalment so the notional is fully repaid by maturity:
with \(a\) the accrued interest at \(s\), \(r\) the rate, and \(t_1,\dots ,t_m\) the future PR-schedule times of the annuity (§5.5).
The canonical payoff of a contract aggregates all future event payoffs under frozen risk-factor conditions, \(F(x,t)=\sum _{c\in C}c\). When a contract settles in a currency CURS other than its denomination CUR, payoffs are scaled by the settlement FX rate
which appears as the leading factor of every payoff function below.
4 Composition and observers
Combined contracts derive their payoff from child contracts (underlyings) referenced through the attribute CTST, a list of contract references each carrying an object, a type and a role. We write \(\texttt{CTST}_{role}^{type}\) to query a referenced child (omitting the index of the first match), e.g. \(\texttt{CTST}_{FirstLeg}^{Contract}\) for a swap’s first leg or \(\texttt{CTST}_{Underlying}^{Contract}\) for an option’s underlying.
The risk-factor observer is the interface through which a contract reads its uncertain environment. In rate mode it returns a market state, \(O^{rf}:i,t\mapsto \mathbb {R}\), and in event mode it returns observed unscheduled events, \(O^{ev}:i,k,t\mapsto \{ e_t^k,\dots \} \) — e.g. \(O^{rf}(\texttt{RRMO},t)\) for a reset reference rate, or \(O^{ev}(\texttt{CID},\texttt{PP},t)\) for observed prepayments. The interface fixes structure only; implementations encode whatever assumption a forward-looking analysis requires.
The child-contract observer lets a parent read its children: future events \(U^{ev}:i,t,a\mapsto \{ e_v^k,\dots \} \), a child state variable \(U^{sv}:i,t,x,a\mapsto \mathbb {R}\), or a child attribute \(U^{ca}:i,x\mapsto y\) — the basis for evaluating swaps, options and credit enhancement over their underlyings.
5 Contract types
Each contract type is specified by three normative tables — its contract schedule (which events occur and when), its state-variable initialisation (the state at \(t_0\)), and its state-transition and payoff functions (the effect of each event) — reproduced below and linked to the Lean stf/pof/Step definitions that formalize them.
5.1 PAM: Principal at Maturity
PAM is the archetypal ACTUS contract and the building block of the whole maturity family. The entire principal (notional) is advanced at the initial exchange date IED and returned in a single bullet repayment at maturity MD; in between, interest accrues continuously and is paid out on the interest-payment schedule IP. No principal is amortized during the term, so the outstanding notional \(\mathbf{Nt}_{}\) stays constant between IED and MD — which makes PAM the natural model for fixed-term bonds, bullet loans and term deposits.
The contract state carries the outstanding notional \(\mathbf{Nt}_{}\), the nominal rate \(\mathbf{Ipnr}_{}\), accrued interest \(\mathbf{Ipac}_{}\) and fees \(\mathbf{Feac}_{}\), and the notional/interest scaling indices \(\mathbf{Nsc}_{}\)/\(\mathbf{Isc}_{}\). Optional features layer on through their own events: rate resets (RR/RRF, optionally clamped to the life window \([\texttt{RRLF},\texttt{RRLC}]\)), index scaling (SC), periodic fees (FP), prepayment penalties (PY), unscheduled prepayment (PP) and early termination (TD). Because every other lending contract (LAM, NAM, ANN, CLM) is specified as PAM plus a redemption rule, the PAM state-transition and payoff functions below are reused throughout the family.
The PAM state-transition function \(\mathrm{STF}\_ k\_ PAM()\), one branch per event type, together with the payoff function \(\mathrm{POF}\_ k\_ PAM()\), as given by the table below.
|
PAM |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
\(\mathbf{Md}_{t_0} = \texttt{MD}\) |
||
|
\(\mathbf{Nt}_{}\) |
\(\mathbf{Nt}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if} \quad \texttt{IED} {\gt} t_0 \\ R(\texttt{CNTRL})\times \texttt{NT} & \text{else} \end{array}\right.\) |
||
|
\(\mathbf{Ipnr}_{}\) |
\(\mathbf{Ipnr}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if} \quad \texttt{IED} {\gt} t_0 \\ \texttt{IPNR} & \text{else} \end{array}\right.\) |
||
|
\(\mathbf{Ipac}_{}\) |
\(\mathbf{Ipac}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if} \quad \texttt{IPNR}=\varnothing \\ \texttt{IPAC} & \text{else if} \quad \texttt{IPAC} \neq \varnothing \\ Y(t^-,t_0)\times \mathbf{Nt}_{t_0}\times \mathbf{Ipnr}_{t_0} & \text{else} \end{array}\right.\) with \(t^- = \sup t \in \vec{t}^{IP}\mid t{\lt}t_0\) |
||
|
\(\mathbf{Feac}_{}\) |
\(\mathbf{Feac}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if} \quad \texttt{FER}=\varnothing \\ \texttt{FEAC} & \text{else if} \quad \texttt{FEAC} \neq \varnothing \\ Y(t^{FP-},t_0)\times \mathbf{Nt}_{t_0}\times \texttt{FER} & \text{else if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t_0)}{Y(t^{FP-},t^{FP+})}\times \texttt{FER} & \text{else} \end{array}\right.\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
||
|
\(\mathbf{Nsc}_{}\) |
\(\mathbf{Nsc}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{SCIXSD} & \text{if} \quad \texttt{SCEF}=\text{'[x]N[x]'} \\ 1.0 & \text{else} \end{array}\right.\) |
||
|
\(\mathbf{Isc}_{}\) |
\(\mathbf{Isc}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{SCIXSD} & \text{if} \quad \texttt{SCEF}=\text{'I[x][x]'} \\ 1.0 & \text{else} \end{array}\right.\) |
||
|
\(\mathbf{Prf}_{}\) |
\(\mathbf{Prf}_{t_0} = \texttt{PRF}\) |
||
|
\(\mathbf{Sd}_{}\) |
\(\mathbf{Sd}_{t_0} = t_0\) |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
\(\vec{t}^{AD} = \left(t_0,t_1,...,t_n\right)\) With \(t_i,i=1,2,...\) a custom input |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + \Delta \mathbf{Ipac}\\ \mathbf{Sd}’ & = t \end{array}\) |
|
IED |
\(t^{IED} = \texttt{IED}\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(-1)(\texttt{NT}+\texttt{PDIED})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & =R(\texttt{CNTRL})\texttt{NT} \\ \mathbf{Ipnr}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if} \quad \texttt{IPNR}=\varnothing \\ \texttt{IPNR} & \text{else} \end{array}\right. \\ \mathbf{Ipac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{IPAC} & \text{if} \quad \texttt{IPAC} \neq \varnothing \\ y\mathbf{Nt}’\cdot \mathbf{Ipnr}’ & \text{if} \quad \texttt{IPANX} \neq \varnothing \land \texttt{IPANX}{\lt}t \\ 0.0 & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) with \(y=Y(\texttt{IPANX},t)\) |
|
MD |
\(t^{MD} = \mathbf{Md}_{t_0}\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)(\mathbf{Nsc}\cdot \mathbf{Nt}+\mathbf{Isc}\cdot \mathbf{Ipac}+\mathbf{Feac})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = 0.0 \\ \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Feac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
PP |
\(\vec{t}^{PP} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{PPEF}=\text{'N'} \\ (\vec{u},\vec{v}) & \text{else} \end{array}\right.\) where \(\begin{array}{@{}r@{}l@{\quad }l@{}} \vec{u} & = S(s,\texttt{OPCL},T^{MD}) \\ \vec{v} & = O^{ev}(\texttt{CID},\texttt{PP},t) \end{array}\) with \(s = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{OPANX}=\varnothing \land \texttt{OPCL}=\varnothing \\ \texttt{IED}+\texttt{OPCL} & \text{else if} \quad \texttt{OPANX} = \varnothing \\ \texttt{OPANX} & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)f(O^{ev}(\texttt{CID},\texttt{PP},t))\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + \Delta \mathbf{Ipac}\\ \mathbf{Nt}’ & = \mathbf{Nt} - f(O^{ev}(\texttt{CID},\texttt{PP},t)) \\ \mathbf{Sd}’ & = t \end{array}\) |
|
PY |
\(\vec{t}^{PY} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{PYTP}=\text{'O'} \\ \vec{t}^{PP} & \text{else} \end{array}\right.\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}}& X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})\texttt{PYRT} & \text{if} \ \texttt{PYTP}=\text{'A'}\\ & c\, \texttt{PYRT} & \text{if} \ \texttt{PYTP}=\text{'N'}\\ & c\max (0,\mathbf{Ipnr}-O^{rf}(\texttt{RRMO},t)) & \text{if} \ \texttt{PYTP}=\text{'I'} \end{array}\) with \(c=X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})Y(\mathbf{Sd},t)\mathbf{Nt}\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + \Delta \mathbf{Ipac}\\ \mathbf{Sd}’ & = t \end{array}\) |
|
FP |
\(\vec{t}^{FP} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{FER}=\varnothing \lor \texttt{FER}=0 \\ S(s,\texttt{FECL},T^{MD}) & \text{else} \end{array}\right.\) with \(s = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{FEANX}=\varnothing \land \texttt{FECL}=\varnothing \\ \texttt{IED}+\texttt{FECL} & \text{else if} \quad \texttt{FEANX} = \varnothing \\ \texttt{FEANX} & \text{else} \end{array}\right.\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}}& R(\texttt{CNTRL})c & \text{if} \ \texttt{FEB}=\text{'A'}\\ & cY(\mathbf{Sd},t)\mathbf{Nt}+\mathbf{Feac} & \text{if} \ \texttt{FEB}=\text{'N'} \end{array}\) with \(c=X_{\texttt{CUR}}^{\texttt{CURS}}(t)\texttt{FER}\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + \Delta \mathbf{Ipac}\\ \mathbf{Feac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
PRD |
\(t^{PRD}= \texttt{PRD}\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(-1)(\texttt{PPRD} + \mathbf{Ipac} + \Delta \mathbf{Ipac})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + \Delta \mathbf{Ipac}\\ \mathbf{Sd}’ & = t \end{array}\) |
|
TD |
\(t^{TD}= \texttt{TD}\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(\texttt{PTD} + \mathbf{Ipac} + \Delta \mathbf{Ipac})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = 0.0 \\ \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Feac}’ & = 0.0 \\ \mathbf{Ipnr}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
IP |
\(\vec{t}^{IP} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{IPNR}=\varnothing \\ S(s,\texttt{IPCL},T^{MD}) & \text{else} \end{array}\right.\) with \(s = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{IPANX}=\varnothing \land \texttt{IPCL}=\varnothing \\ \texttt{IPCED} & \text{else if}\quad \texttt{IPCED}\neq \varnothing \\ \texttt{IED}+\texttt{IPCL} & \text{else if} \quad \texttt{IPANX} = \varnothing \\ \texttt{IPANX} & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)\mathbf{Isc}\cdot (\mathbf{Ipac} + \Delta \mathbf{Ipac})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
IPCI |
\(\vec{t}^{IPCI} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{IPCED}=\varnothing \\ S(s,\texttt{IPCL},\texttt{IPCED}) & \text{else} \end{array}\right.\) with \(s = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{IPANX}=\varnothing \land \texttt{IPCL}=\varnothing \\ \texttt{IED}+\texttt{IPCL} & \text{else if} \quad \texttt{IPANX} = \varnothing \\ \texttt{IPANX} & \text{else} \end{array}\right.\) |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = \mathbf{Nt} + \mathbf{Ipac} + \Delta \mathbf{Ipac}\\ \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
RR |
\(\vec{t}^{RR} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{RRANX}=\varnothing \land \texttt{RRCL}=\varnothing \\ \vec{t} \setminus t^{RRY} & \text{else if} \texttt{RRNXT} \neq \varnothing \\ \vec{t} & \text{else} \end{array}\right.\) where \(\vec{t}=S(s,\texttt{RRCL},T^{MD})\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} s & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{IED}+\texttt{RRCL} & \text{if} \quad \texttt{RRANX} = \varnothing \\ \texttt{RRANX} & \text{else} \end{array}\right. \\ t^{RRY} & = \inf t \in \vec{t}\mid t{\gt}\texttt{SD} \end{array}\) |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + \Delta \mathbf{Ipac}\\ \mathbf{Ipnr}’ & = \min (\max (\mathbf{Ipnr}+\Delta r,\texttt{RRLF}),\texttt{RRLC}) \\ \mathbf{Sd}’ & = t \end{array}\) with \(\Delta r = \min (\max (O^{rf}(\texttt{RRMO},t)\texttt{RRMLT}+\texttt{RRSP} - \mathbf{Ipnr},\texttt{RRPF}),\texttt{RRPC})\) |
|
RRF |
\(t^{RRF} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{RRANX}=\varnothing \land \texttt{RRCL}=\varnothing \\ \inf t \in \vec{t}\mid t{\gt}\texttt{SD} & \text{else} \end{array}\right.\) where \(\vec{t}=S(s,\texttt{RRCL},T^{MD})\) with \(s = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{IED}+\texttt{RRCL} & \text{if} \quad \texttt{RRANX} = \varnothing \\ \texttt{RRANX} & \text{else} \end{array}\right.\) |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + \Delta \mathbf{Ipac}\\ \mathbf{Ipnr}’ & = \texttt{RRNXT} \\ \mathbf{Sd}’ & = t \end{array}\) |
|
SC |
\(\vec{t}^{SC} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{SCEF}=\text{'000'} \\ S(s,\texttt{SCCL},T^{MD}) & \text{else} \end{array}\right.\) with \(s = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{SCANX}=\varnothing \land \texttt{SCCL}=\varnothing \\ \texttt{IED}+\texttt{SCCL} & \text{else if} \quad \texttt{SCANX} = \varnothing \\ \texttt{SCANX} & \text{else} \end{array}\right.\) |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + \Delta \mathbf{Ipac}\\ \mathbf{Nsc}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Nsc} & \text{if} \ \texttt{SCEF} = [x]0[x] \\ \frac{O^{rf}(\texttt{SCMO},t) - \texttt{SCIED}}{\texttt{SCIED}} & \text{else} \end{array}\right. \\ \mathbf{Isc}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Isc} & \text{if} \ \texttt{SCEF} = 0[x][x] \\ \frac{O^{rf}(\texttt{SCMO},t) - \texttt{SCIED}}{\texttt{SCIED}} & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) |
|
CE |
\(\vec{t}^{CE} = t(e^{k}) \mid \mathbf{Prf} \neq \mathbf{Prf}’, \forall k\) |
0.0 |
\(\mathrm{STF}\_ AD\_ PAM()\) |
The relational one-step transition; each constructor’s target is the functional next-state stf of the table above, so the relation is exactly the graph of stf (Theorem 21).
5.2 LAM: Linear Amortizer
A linear amortizer repays principal in equal redemptions on the principal-redemption schedule PR, so the outstanding notional steps down by a fixed amount each period and reaches zero exactly at maturity. Interest is charged on the declining balance, so the interest portion of each instalment shrinks over time while the principal portion stays constant — the classic constant-amortization loan.
LAM, NAM and ANN share PAM’s machinery and differ only in how the redemption is sized: LAM fixes the principal portion (PRNXT); NAM fixes the total payment and lets principal absorb whatever is left after interest; ANN fixes the total payment through the annuity formula. The LAM tables below therefore record only what differs from PAM — chiefly the PR redemption and the interest-calculation-base bookkeeping (IPCB) that tracks the balance on which interest is charged.
The amortizing contracts, defined as deltas over PAM: a linear principal redemption (LAM), interest-first redemption (NAM), and constant-instalment annuity with rate-reset re-amortization (ANN).
|
LAM |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
\(\mathbf{Md}_{t_0}=\left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{MD} & \text{if}\quad \texttt{MD}\neq \varnothing \\ t^-+ceil(\frac{\texttt{NT}}{\texttt{PRNXT}})\texttt{PRCL} \end{array}\right.\) where \(t^- = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{PRANX} & \text{if}\quad \texttt{PRANX}\neq \varnothing \land \texttt{PRANX}\geq t_0 \\ \texttt{IED}+\texttt{PRCL} & \text{else if}\quad \texttt{IED}+\texttt{PRCL}\geq t_0 \\ \sup t \in \vec{t}^{PR}\mid t{\lt}t_0 & \text{else} \end{array}\right.\) |
||
|
\(\mathbf{Nt}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipnr}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Feac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Nsc}_{}\) |
Same as PAM |
||
|
\(\mathbf{Isc}_{}\) |
Same as PAM |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
\(\mathbf{Prnxt}_{}\) |
\(\mathbf{Prnxt}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{PRNXT} & \text{if}\quad \texttt{PRNXT}\neq \varnothing \\ \texttt{NT}(ceil(\frac{Y(s,T^{MD})}{Y(s,s+\texttt{PRCL})}))^{-1} & \text{else} \end{array}\right.\) with \(s = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{PRANX} & \text{if}\quad \texttt{PRANX}\neq \varnothing \land \texttt{PRANX}{\gt}t_0\\ \texttt{IED}+\texttt{PRCL} & \text{else if}\quad \texttt{PRANX} = \varnothing \land \texttt{IED}+\texttt{PRCL}{\gt}t_0 \\ t^- & \text{else} \end{array}\right.\) and where \(t^- = \sup t \in \vec{t}^{PR}\mid t{\lt}t_0\) |
||
|
\(\mathbf{Ipcb}_{}\) |
\(\mathbf{Ipcb}_{t_0}= \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if}\quad t_0{\lt}\texttt{IED} \\ R(\texttt{CNTRL})\texttt{NT} & \text{else if}\quad \texttt{IPCB}=\text{'NT'} \\ R(\texttt{CNTRL})\texttt{IPCBA} & \text{else} \end{array}\right.\) |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
|
IED |
Same as PAM |
\(\mathrm{POF}\_ IED\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & =R(\texttt{CNTRL})\texttt{NT} \\ \mathbf{Ipnr}’ & = \texttt{IPNR} \\ \mathbf{Ipac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{IPAC} & \text{if} \quad \texttt{IPAC} \neq \varnothing \\ y\mathbf{Nt}’\cdot \mathbf{Ipnr}’ & \text{if} \quad \texttt{IPANX} \neq \varnothing \land \texttt{IPANX}{\lt}t \\ 0.0 & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \\ \mathbf{Ipcb}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} R(\texttt{CNTRL})\texttt{NT} & \text{if}\quad \texttt{IPCB}=\text{'NT'} \\ R(\texttt{CNTRL})\texttt{IPCBA} & \text{else} \end{array}\right. \end{array}\) |
|
PR |
\(t^{PR} = S(s,\texttt{PRCL},T^{MD},F)\) with \(s = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{PRANX}=\varnothing \land \texttt{PRCL}=\varnothing \\ \texttt{IED}+\texttt{PRCL} & \text{else if} \quad \texttt{PRANX} = \varnothing \\ \texttt{PRANX} & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})\mathbf{Nsc}\cdot \mathbf{Prnxt}\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = \mathbf{Nt}-R(\texttt{CNTRL})\mathbf{Prnxt} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Ipcb}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Ipcb} & \text{if}\quad \texttt{IPCB}\neq \text{'NT'} \\ \mathbf{Nt}’ & \text{else} \end{array}\right.\\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
MD |
\(t^{MD} = \mathbf{Md}_{t_0}\) |
\(\mathrm{POF}\_ MD\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = 0.0 \\ \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Feac}’ & = 0.0 \\ \mathbf{Ipcb}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
PP |
Same as PAM |
\(\mathrm{POF}\_ PP\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Nt}’ & = \mathbf{Nt} - f(O^{ev}(\texttt{CID},\texttt{PP},t)) \\ \mathbf{Ipcb}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Ipcb} & \text{if}\quad \texttt{IPCB}\neq \text{'NT'} \\ \mathbf{Nt}’ & \text{else} \end{array}\right.\\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
PY |
Same as PAM |
\(\mathrm{POF}\_ PY\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
FP |
Same as PAM |
\(\mathrm{POF}\_ FP\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
PRD |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(-1)(\texttt{PPRD} + \mathbf{Ipac} +\) \(\qquad \qquad Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
TD |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(\texttt{PTD} + \mathbf{Ipac} +\) \(\qquad \qquad Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb})\) |
\(\mathrm{STF}\_ TD\_ PAM()\) |
|
IP |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)\mathbf{Isc}\cdot (\mathbf{Ipac} +\) \(\qquad \qquad Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb})\) |
\(\mathrm{STF}\_ IP\_ PAM()\) |
|
IPCI |
Same as PAM |
\(\mathrm{POF}\_ IPCI\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = \mathbf{Nt} + \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb}\\ \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Ipcb}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Ipcb} & \text{if}\quad \texttt{IPCB}\neq \text{'NT'} \\ \mathbf{Nt}’ & \text{else} \end{array}\right.\\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
IPCB |
\(\vec{t}^{IPCB} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{IPCB}\neq \text{'NTL'} \\ S(s,\texttt{IPCBCL},T^{MD}) & \text{else} \end{array}\right.\) with \(s = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{IPCBANX}=\varnothing \land \texttt{IPCBCL}=\varnothing \\ \texttt{IED}+\texttt{IPCBCL} & \text{else if} \quad \texttt{IPCBANX} = \varnothing \\ \texttt{IPCBANX} & \text{else} \end{array}\right.\) |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipcb}’ & = \mathbf{Nt} \\ \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
RR |
Same as PAM |
\(\mathrm{POF}\_ RR\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Ipnr}’ & = \min (\max (\mathbf{Ipnr}+\Delta r,\texttt{RRLF}),\texttt{RRLC}) \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} \Delta r & = \min (\max (O^{rf}(\texttt{RRMO},t)\texttt{RRMLT}+\texttt{RRSP} - \mathbf{Ipnr},\texttt{RRPF}),\texttt{RRPC}) \\ t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
RRF |
Same as PAM |
\(\mathrm{POF}\_ RRF\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Ipnr}’ & = \texttt{RRNXT} \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
SC |
Same as PAM |
\(\mathrm{POF}\_ SC\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Nsc}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Nsc} & \text{if} \quad \texttt{SCEF} = [x]0[x] \\ \frac{O^{rf}(\texttt{SCMO},t) - \texttt{SCIED}}{\texttt{SCIED}} & \text{else} \end{array}\right. \\ \mathbf{Isc}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Isc} & \text{if} \quad \texttt{SCEF} = 0[x][x] \\ \frac{O^{rf}(\texttt{SCMO},t) - \texttt{SCIED}}{\texttt{SCIED}} & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
5.3 LAX: Exotic Linear Amortizer
The exotic amortizer generalizes LAM to non-uniform schedules. Principal can be both drawn down (PI, principal increase) and redeemed (PR) on piecewise array schedules (§3): the term is partitioned into segments, each with its own anchor, cycle, rate and redemption amount. This captures structured loans with grace periods, step-ups, balloon segments and draw phases that a single cyclic schedule cannot express.
Within each segment the dynamics follow LAM; the array schedule concatenates the per-segment cyclic schedules. LAX carries the same dual model as the lending family: its own state-transition and payoff functions LAX.stf/LAX.pof (generalised with a per-event payload — the array redemption amount, or the reset rate), together with a relational LAX.Step proven to be their graph. The executable builder folds stf/pof over the array-derived event list, so the relation certifies the engine.
LAX (exotic amortizer) redeems or draws principal on piecewise array schedules; UMP (§5.7) is a non-maturity deposit whose interest capitalizes, settling at the agreed price plus accrued interest on termination. Both carry the relational Step and functional stf/pof models (proven to agree), alongside their executable builders.
|
LAX |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
\(\mathbf{Md}_{t_0}=\left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{MD} & \text{if}\quad \texttt{MD}\neq \varnothing \\ \inf t{\gt}t_0 \mid N(t)=0 & \text{else} \end{array}\right.\) with \(N(t) = \texttt{NT} + \sum _{i=1}^{n(t)} (-1)^k \texttt{ARPRNXT}_i \mid s_i \mid \) where \(\begin{array}{@{}r@{}l@{\quad }l@{}} n(t) & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \sup k\in \mathbb {N}\mid \texttt{ARPRANX}_k{\lt}t & \text{if}\quad t{\lt}max(\texttt{ARPRANX}) \\ \mid \texttt{ARPRANX}\mid & \text{else} \end{array}\right. \\ k & = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0 & \text{if}\quad \texttt{ARINCDEC}_i=\text{'INC'}\\ 1 & \text{else} \end{array}\right. \\ s_i & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \{ \texttt{ARPRANX}_i \} & \text{if}\quad \texttt{ARPRCL} = \varnothing \\ S(\texttt{ARPRANX}_i,\vec{C}_i,T_i) & \text{else} \end{array}\right. \\ T_i & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{ARPRANX}_{i+1} & \text{if}\quad i{\lt}\mid \texttt{ARPRANX}\mid \\ t & \text{else} \end{array}\right. \\ \vec{C} & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{ARRRCL} & \text{if} \quad \mid \texttt{ARRRCL}\mid = \mid \texttt{ARRRANX}\mid \\ \{ c_1, c_2, ..., c_n \} & \text{else} \end{array}\right. \end{array}\) |
||
|
\(\mathbf{Nt}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipnr}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Feac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Nsc}_{}\) |
Same as PAM |
||
|
\(\mathbf{Isc}_{}\) |
Same as PAM |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
\(\mathbf{Prnxt}_{}\) |
\(\mathbf{Prnxt}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if}\quad t_0\geq \texttt{ARPRANX}_1 \\ \texttt{ARPRNXT}_i & \text{else} \end{array}\right.\) where \(i = \sup k\in \mathbb {N}\mid \texttt{ARPRANX}_k{\lt}t_0\) |
||
|
\(\mathbf{Ipcb}_{}\) |
Same as LAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
|
IED |
Same as PAM |
\(\mathrm{POF}\_ IED\_ PAM()\) |
\(\mathrm{STF}\_ IED\_ LAM()\) |
|
PR |
\(\vec{t}^{PR} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \{ t_1, t_2, ..., t_i, ... \} & \text{if}\quad \texttt{ARPRCL}=\varnothing \\ s_1 \cup s_2 \cup ... \cup s_i \cup ... & \text{else} \end{array}\right.\) with \(s_i=S(\texttt{ARPRANX}_i,\vec{C}_i,\texttt{ARPRANX}_{i+1})\), \(i\in \{ 1,2,...,\mid \texttt{ARINCDEC}\mid \} \mid \texttt{ARINCDEC}_i = \text{'DEC'}\) with \(\vec{C} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{ARPRCL} & \text{if} \quad \mid \texttt{ARPRCL}\mid = \mid \texttt{ARPRANX}\mid \\ \{ c_1, c_2, ..., c_n \} & \text{else} \end{array}\right.\) where \(n=\mid \texttt{ARPRANX}\mid , c_k=\texttt{ARPRCL}_1\forall k\) |
\(\mathrm{POF}\_ PR\_ LAM()\) |
\(\mathrm{STF}\_ PR\_ LAM()\) |
|
MD |
Same as PAM |
\(\mathrm{POF}\_ MD\_ PAM()\) |
\(\mathrm{STF}\_ MD\_ LAM()\) |
|
PI |
\(\vec{t}^{PI} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \{ t_1, t_2, ..., t_i, ... \} & \text{if}\quad \texttt{ARPRCL}=\varnothing \\ s_1 \cup s_2 \cup ... \cup s_i \cup ... & \text{else} \end{array}\right.\) with \(s_i=S(\texttt{ARPRANX}_i,\vec{C}_i,\texttt{ARPRANX}_{i+1})\), \(i\in \{ 1,2,...,\mid \texttt{ARINCDEC}\mid \} \mid \texttt{ARINCDEC}_i = \text{'INC'}\) with \(\vec{C} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{ARPRCL} & \text{if} \quad \mid \texttt{ARPRCL}\mid = \mid \texttt{ARPRANX}\mid \\ \{ c_1, c_2, ..., c_n \} & \text{else} \end{array}\right.\) where \(n=\mid \texttt{ARPRANX}\mid , c_k=\texttt{ARPRCL}_1\forall k\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(-1)\mathbf{Nsc}\cdot \mathbf{Prnxt}\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = \mathbf{Nt}+R(\texttt{CNTRL})\mathbf{Prnxt} \\ \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Ipcb}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Ipcb} & \text{if}\quad \texttt{IPCB}\neq \text{'NT'} \\ \mathbf{Nt}’ & \text{else} \end{array}\right.\\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
PRF |
\(\vec{t}^{PRF} = \texttt{ARPRANX}\) |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Prnxt}’ & = \texttt{ARPRNXT}_i \\ \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Ipcb}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Ipcb} & \text{if}\quad \texttt{IPCB}\neq \text{'NT'} \\ \mathbf{Nt}’ & \text{else} \end{array}\right.\\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} i & = \sup k\in \mathbb {N}\mid \texttt{ARPRANX}_k=t \\ t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
PP |
Same as PAM |
\(\mathrm{POF}\_ PP\_ PAM()\) |
\(\mathrm{STF}\_ PP\_ LAM()\) |
|
PY |
Same as PAM |
\(\mathrm{POF}\_ PY\_ PAM()\) |
\(\mathrm{STF}\_ PY\_ LAM()\) |
|
FP |
Same as PAM |
\(\mathrm{POF}\_ FP\_ PAM()\) |
\(\mathrm{STF}\_ FP\_ LAM()\) |
|
PRD |
Same as PAM |
\(\mathrm{POF}\_ PRD\_ LAM()\) |
\(\mathrm{STF}\_ PRD\_ LAM()\) |
|
TD |
Same as PAM |
\(\mathrm{POF}\_ TD\_ LAM()\) |
\(\mathrm{STF}\_ TD\_ PAM()\) |
|
IP |
\(\vec{t}^{IP} = \vec{S}(\texttt{ARIPANX},\texttt{ARIPCL},\mathbf{Md}_{t_0})\) |
\(\mathrm{POF}\_ IP\_ LAM()\) |
\(\mathrm{STF}\_ IP\_ PAM()\) |
|
IPCI |
Same as PAM |
\(\mathrm{POF}\_ IPCI\_ PAM()\) |
\(\mathrm{STF}\_ IPCI\_ LAM()\) |
|
IPCB |
Same as LAM |
\(\mathrm{POF}\_ IPCB\_ LAM()\) |
\(\mathrm{STF}\_ IPCB\_ LAM()\) |
|
RR |
\(\vec{t}^{RR} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \{ t_1, t_2, ..., t_i, ... \} & \text{if}\quad \texttt{ARRRCL}=\varnothing \\ s_1 \cup s_2 \cup ... \cup s_i \cup ... & \text{else} \end{array}\right.\) with \(s_i=S(\texttt{ARRRANX}_i,\vec{C}_i,\texttt{ARRRANX}_{i+1})\), \(i\in \{ 1,2,...,\mid \texttt{ARFIXVAR}\mid \} \mid \texttt{ARFIXVAR}_i = \text{'V'}\) with \(\vec{C} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{ARRRCL} & \text{if} \quad \mid \texttt{ARRRCL}\mid = \mid \texttt{ARRRANX}\mid \\ \{ c_1, c_2, ..., c_n \} & \text{else} \end{array}\right.\) where \(n=\mid \texttt{ARRRANX}\mid , c_k=\texttt{ARRRCL}_1\forall k\) |
\(\mathrm{POF}\_ RR\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Ipnr}’ & = \min (\max (\mathbf{Ipnr}+\Delta r,\texttt{RRLF}),\texttt{RRLC}) \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} \Delta r & = \min (\max (O^{rf}(\texttt{RRMO},t)\texttt{RRMLT}+\texttt{ARRATE}_i - \mathbf{Ipnr},\texttt{RRPF}),\texttt{RRPC}) \\ i & = \sup k\in \mathbb {N}\mid \texttt{ARPRANX}_k=t \\ t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
RRF |
\(\vec{t}^{RRF} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \{ t_1, t_2, ..., t_i, ... \} & \text{if}\quad \texttt{ARRRCL}=\varnothing \\ s_1 \cup s_2 \cup ... \cup s_i \cup ... & \text{else} \end{array}\right.\) with \(s_i=S(\texttt{ARRRANX}_i,\vec{C}_i,\texttt{ARRRANX}_{i+1})\), \(i\in \{ 1,2,...,\mid \texttt{ARFIXVAR}\mid \} \mid \texttt{ARFIXVAR}_i = \text{'F'}\) with \(\vec{C} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{ARRRCL} & \text{if} \quad \mid \texttt{ARRRCL}\mid = \mid \texttt{ARRRANX}\mid \\ \{ c_1, c_2, ..., c_n \} & \text{else} \end{array}\right.\) where \(n=\mid \texttt{ARRRANX}\mid , c_k=\texttt{ARRRCL}_1\forall k\) |
\(\mathrm{POF}\_ RRF\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Ipnr}’ & = \texttt{ARRATE}_i \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} i & = \sup k\in \mathbb {N}\mid \texttt{ARRRANX}_k=t \\ t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
SC |
Same as PAM |
\(\mathrm{POF}\_ SC\_ PAM()\) |
\(\mathrm{STF}\_ SC\_ LAM()\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
5.4 NAM: Negative Amortizer
In a negative amortizer the borrower pays a fixed total instalment (PRNXT) each period, out of which interest is served first and only the remainder reduces principal. When the instalment exceeds the interest due the loan amortizes normally; when interest exceeds the instalment the shortfall is capitalized and the outstanding notional actually grows — hence “negative” amortization.
NAM is PAM with a PR event whose redemption equals the fixed payment net of accrued interest, with the interest-calculation base updated accordingly. It is the model for payment-capped and graduated-payment mortgages, where the scheduled payment is held constant even when it fails to cover current interest.
|
NAM |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
\(\mathbf{Md}_{t_0}=\left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{MD} & \text{if}\quad \texttt{MD}\neq \varnothing \\ t^-+n\texttt{PRCL} & \text{else} \end{array}\right.\) with \(n=ceil(\frac{\texttt{NT}}{\texttt{PRNXT}-\texttt{NT}Y(t^-,t^-+\texttt{PRCL})\texttt{IPNR}})\) where \(t^- = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{PRANX} & \text{if}\quad \texttt{PRANX}\neq \varnothing \land \texttt{PRANX}\geq t_0 \\ \texttt{IED}+\texttt{PRCL} & \text{else if}\quad \texttt{IED}+\texttt{PRCL}\geq t_0 \\ \sup t \in t^{PR}\mid t{\lt}t_0 & \text{else} \end{array}\right.\) |
||
|
\(\mathbf{Nt}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipnr}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Feac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Nsc}_{}\) |
Same as PAM |
||
|
\(\mathbf{Isc}_{}\) |
Same as PAM |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
\(\mathbf{Prnxt}_{}\) |
\(\mathbf{Prnxt}_{t_0} = R(\texttt{CNTRL})\texttt{PRNXT}\) |
||
|
\(\mathbf{Ipcb}_{}\) |
Same as LAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
|
IED |
Same as PAM |
\(\mathrm{POF}\_ IED\_ PAM()\) |
\(\mathrm{STF}\_ IED\_ LAM()\) |
|
PR |
Same as LAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)\mathbf{Nsc}\cdot (\mathbf{Prnxt}-\mathbf{Ipac}-\) \(\qquad \qquad Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = \mathbf{Nt}-(\mathbf{Prnxt}-\mathbf{Ipac}’) \\ \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Ipcb}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Ipcb} & \text{if}\quad \texttt{IPCB}\neq \text{'NT'} \\ \mathbf{Nt}’ & \text{else} \end{array}\right.\\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
MD |
Same as PAM |
\(\mathrm{POF}\_ MD\_ PAM()\) |
\(\mathrm{STF}\_ MD\_ LAM()\) |
|
PP |
Same as PAM |
\(\mathrm{POF}\_ PP\_ PAM()\) |
\(\mathrm{STF}\_ PP\_ LAM()\) |
|
PY |
Same as PAM |
\(\mathrm{POF}\_ PY\_ PAM()\) |
\(\mathrm{STF}\_ PY\_ LAM()\) |
|
FP |
Same as PAM |
\(\mathrm{POF}\_ FP\_ PAM()\) |
\(\mathrm{STF}\_ FP\_ LAM()\) |
|
PRD |
Same as PAM |
\(\mathrm{POF}\_ PRD\_ LAM()\) |
\(\mathrm{STF}\_ PRD\_ LAM()\) |
|
TD |
Same as PAM |
\(\mathrm{POF}\_ TD\_ LAM()\) |
\(\mathrm{STF}\_ TD\_ PAM()\) |
|
IP |
\(\vec{t}^{IP} = (\vec{u},\vec{v})\) where \(\begin{array}{@{}r@{}l@{\quad }l@{}} \vec{u} & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{IPANX}=\varnothing \land \texttt{IPCL}=\varnothing \\ \varnothing & \text{if}\quad \texttt{IPCED}\neq \varnothing \land \texttt{IPCED}\geq \texttt{T}\\ S(r,\texttt{IPCL},T) & \text{else} \end{array}\right. \\ \vec{v} & = S(s,\texttt{PRCL},T^{MD}) \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} r & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{IPCED} & \text{if}\quad \texttt{IPCED}\neq \varnothing \\ \texttt{IPANX} & \text{else if}\quad \texttt{IPANX}\neq \varnothing \\ \texttt{IED}+\texttt{IPCL} & \text{else if}\quad \texttt{IPCL}\neq \varnothing \\ \varnothing & \text{else} \end{array}\right. \\ T & = s-\texttt{PRCL} \\ s & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{IED}+\texttt{PRCL} & \text{if} \quad \texttt{PRANX} = \varnothing \\ \texttt{PRANX} & \text{else} \end{array}\right. \end{array}\) |
\(\mathrm{POF}\_ IP\_ LAM()\) |
\(\mathrm{STF}\_ IP\_ PAM()\) |
|
IPCI |
Same as PAM |
\(\mathrm{POF}\_ IPCI\_ PAM()\) |
\(\mathrm{STF}\_ IPCI\_ LAM()\) |
|
IPCB |
Same as LAM |
\(\mathrm{POF}\_ IPCB\_ LAM()\) |
\(\mathrm{STF}\_ IPCB\_ LAM()\) |
|
RR |
Same as PAM |
\(\mathrm{POF}\_ RR\_ PAM()\) |
\(\mathrm{STF}\_ RR\_ LAM()\) |
|
RRF |
Same as PAM |
\(\mathrm{POF}\_ RRF\_ PAM()\) |
\(\mathrm{STF}\_ RRF\_ LAM()\) |
|
SC |
Same as PAM |
\(\mathrm{POF}\_ SC\_ PAM()\) |
\(\mathrm{STF}\_ SC\_ LAM()\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
5.5 ANN: Annuity
An annuity pays a constant total instalment over its life — the annuity amount \(A\) of §3 — sized so that the level payments exactly retire the loan by maturity. Early instalments are mostly interest and later ones mostly principal, but the total is fixed, which is what makes annuities the standard structure for consumer credit and mortgage lending.
Because the instalment depends on the prevailing rate, a rate reset (RR) triggers a re-amortization: the annuity amount is recomputed from the current balance, the new rate and the remaining redemption schedule so the contract still amortizes to zero by MD. Apart from this re-sizing, ANN reuses PAM’s rate, interest and fee logic — which is why the rate-bound metatheorem (24) carries over to ANN for free.
|
ANN |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
Same as NAM |
||
|
\(\mathbf{Nt}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipnr}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Feac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Nsc}_{}\) |
Same as PAM |
||
|
\(\mathbf{Isc}_{}\) |
Same as PAM |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
\(\mathbf{Prnxt}_{}\) |
\(\mathbf{Prnxt}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} R(\texttt{CNTRL})\texttt{PRNXT} & \text{if}\quad \texttt{PRNXT}\neq \varnothing \\ (\texttt{NT}+\mathbf{Ipac}_{t_0})\frac{todo}{todo} & \text{else} \end{array}\right.\) where \(n=|\vec{t}|\) with \(|a|\) indicating the cardinality of set \(a\) |
||
|
\(\mathbf{Ipcb}_{}\) |
Same as LAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
|
IED |
Same as PAM |
\(\mathrm{POF}\_ IED\_ PAM()\) |
\(\mathrm{STF}\_ IED\_ LAM()\) |
|
PR |
Same as LAM |
\(\mathrm{POF}\_ PR\_ NAM()\) |
\(\mathrm{STF}\_ PR\_ NAM()\) |
|
MD |
Same as PAM |
\(\mathrm{POF}\_ MD\_ PAM()\) |
\(\mathrm{STF}\_ MD\_ LAM()\) |
|
PP |
Same as PAM |
\(\mathrm{POF}\_ PP\_ PAM()\) |
\(\mathrm{STF}\_ PP\_ LAM()\) |
|
PY |
Same as PAM |
\(\mathrm{POF}\_ PY\_ PAM()\) |
\(\mathrm{STF}\_ PY\_ LAM()\) |
|
FP |
Same as PAM |
\(\mathrm{POF}\_ FP\_ PAM()\) |
\(\mathrm{STF}\_ FP\_ LAM()\) |
|
PRD |
Same as PAM |
\(\mathrm{POF}\_ PRD\_ LAM()\) |
\(\mathrm{STF}\_ PRD\_ LAM()\) |
|
TD |
Same as PAM |
\(\mathrm{POF}\_ TD\_ LAM()\) |
\(\mathrm{STF}\_ TD\_ PAM()\) |
|
IP |
Same as NAM |
\(\mathrm{POF}\_ IP\_ LAM()\) |
\(\mathrm{STF}\_ IP\_ PAM()\) |
|
IPCI |
Same as PAM |
\(\mathrm{POF}\_ IPCI\_ PAM()\) |
\(\mathrm{STF}\_ IPCI\_ LAM()\) |
|
IPCB |
Same as LAM |
\(\mathrm{POF}\_ IPCB\_ LAM()\) |
\(\mathrm{STF}\_ IPCB\_ LAM()\) |
|
RR |
Same as PAM |
\(\mathrm{POF}\_ RR\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Ipnr}’ & = \min (\max (\mathbf{Ipnr}+\Delta r,\texttt{RRLF}),\texttt{RRLC}) \\ \mathbf{Prnxt}’ & = A(t,\mathbf{Md}’,\mathbf{Nt}’,\mathbf{Ipac}’,\mathbf{Ipnr}’) \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} \Delta r & = \min (\max (O^{rf}(\texttt{RRMO},t)\texttt{RRMLT}+\texttt{RRSP} - \mathbf{Ipnr},\texttt{RRPF}),\texttt{RRPC}) \\ t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
RRF |
Same as PAM |
\(\mathrm{POF}\_ RRF\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac} + Y(\mathbf{Sd},t)\mathbf{Ipnr}\cdot \mathbf{Ipcb} \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Ipnr}’ & = \texttt{RRNXT} \\ \mathbf{Prnxt}’ & = A(t,\mathbf{Md}’,\mathbf{Nt}’,\mathbf{Ipac}’,\mathbf{Ipnr}’) \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
SC |
Same as PAM |
\(\mathrm{POF}\_ SC\_ PAM()\) |
\(\mathrm{STF}\_ SC\_ LAM()\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
5.6 CLM: Call Money
Call money is a short-term, open loan that either party may “call” (terminate) at will, subject to a notice period. It has no contractual maturity: interest is not paid out but capitalizes into the notional through IPCI, so the balance compounds until the loan is called.
Termination is driven by an observed exercise event (\(\texttt{XD}=\sup \tau (O^{ev}(\texttt{CID},))\)); after the notice period the grown notional is settled in a single payment (STD). Apart from the open maturity and the capitalization of interest, CLM follows PAM, so it reuses PAM’s state transitions directly.
Call money: PAM state transitions with interest capitalizing until maturity. The open “call has no fixed maturity — it closes on an observed exercise (\(\texttt{XD}=\sup \tau (O^{ev}(\texttt{CID},))\)), settling the grown notional after the exercise-notice period.
|
CLM |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
\(\mathbf{Md}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{MD} & \text{if}\quad \texttt{MD}\neq \varnothing \\ s & \text{else if}\quad O^{ev}(\texttt{CID},t_0)\neq \{ \} \\ t^{max}& \text{else} \end{array}\right.\) where \(s=\sup t\in \tau (O^{ev}(\texttt{CID},t_0))\) |
||
|
\(\mathbf{Nt}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipnr}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Feac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
|
IED |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(-1)\texttt{NT}\) |
\(\mathrm{STF}\_ IED\_ PAM()\) |
|
PR |
Same as PAM |
\(\mathrm{POF}\_ PR\_ PAM()\) |
\(\mathrm{STF}\_ PR\_ PAM()\) |
|
FP |
Same as PAM |
\(\mathrm{POF}\_ FP\_ PAM()\) |
\(\mathrm{STF}\_ FP\_ PAM()\) |
|
IP |
\(t^{IP}=\mathbf{Md}_{t_0}\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)(\mathbf{Ipac}+\Delta \mathbf{Ipac})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
IPCI |
\(\vec{t}^{IPCI} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{IPNR}=\varnothing \\ S(s,\texttt{IPCL},\mathbf{Md}_{t_0}) & \text{else} \end{array}\right.\) where \(s=\left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{IPANX} & \text{if}\quad \texttt{IPANX}\neq \varnothing \\ \texttt{IED}+\texttt{IPCL} & \text{else} \end{array}\right.\) |
\(\mathrm{POF}\_ IPCI\_ PAM()\) |
\(\mathrm{STF}\_ IPCI\_ PAM()\) |
|
RR |
Same as PAM |
\(\mathrm{POF}\_ RR\_ PAM()\) |
\(\mathrm{STF}\_ RR\_ PAM()\) |
|
RRF |
Same as PAM |
\(\mathrm{POF}\_ RRF\_ PAM()\) |
\(\mathrm{STF}\_ RRF\_ PAM()\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
5.7 UMP: Undefined Maturity Profile
The undefined-maturity profile models non-maturity deposits such as savings and current accounts: a principal balance that may change over time, interest that capitalizes rather than being paid out, and no scheduled maturity. The holder may add to or withdraw from the balance, and on termination the account settles at its agreed value plus accrued interest.
Like CLM, UMP has no MD; interest accrues on the running balance and is capitalized into it (IPCI), the deposit settling at PTD plus the accrued interest on termination. UMP carries the dual relational/functional model (UMP.Step, UMP.stf/pof); it is documented jointly with LAX as 14.
|
UMP |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
\(\mathbf{Md}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} s & \text{if}\quad O^{ev}(\texttt{CID},t_0)\neq \{ \} \\ t^{max}& \text{else} \end{array}\right.\) where \(s=\sup t, t\in \tau (O^{ev}(\texttt{CID},i,t_0))\) \(i\in \{ \texttt{PR},\texttt{PI}\} \) |
||
|
\(\mathbf{Nt}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipnr}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Feac}_{}\) |
Same as PAM |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
|
IED |
Same as PAM |
\(\mathrm{POF}\_ IED\_ CLM()\) |
\(\mathrm{STF}\_ IED\_ PAM()\) |
|
PR |
\(\vec{t}^{PR}=O^{ev}(\texttt{CID},i,t_0)\) with \(i\in \{ \texttt{PR},\texttt{PI}\} \) |
\(f(e_t^{PR})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = \mathbf{Ipac}+\Delta \mathbf{Ipac}\\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^-,t)}{Y(t^-,t^+)}\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Nt}’ & = \mathbf{Nt}-f(e_t^{PR}) \\ \mathbf{Sd}’ & = t \end{array}\) |
|
FP |
Same as PAM |
\(\mathrm{POF}\_ FP\_ PAM()\) |
\(\mathrm{STF}\_ FP\_ PAM()\) |
|
IPCI |
\(\vec{t}^{IPCI} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{IPNR}=\varnothing \\ S(s,\texttt{IPCL},\mathbf{Md}_{t_0}) & \text{else} \end{array}\right.\) where \(s=\left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{IPANX} & \text{if}\quad \texttt{IPANX}\neq \varnothing \\ \texttt{IED}+\texttt{IPCL} & \text{else} \end{array}\right.\) |
\(\mathrm{POF}\_ IPCI\_ PAM()\) |
\(\mathrm{STF}\_ IPCI\_ PAM()\) |
|
RR |
Same as PAM |
\(\mathrm{POF}\_ RR\_ PAM()\) |
\(\mathrm{STF}\_ RR\_ PAM()\) |
|
RRF |
Same as PAM |
\(\mathrm{POF}\_ RRF\_ PAM()\) |
\(\mathrm{STF}\_ RRF\_ PAM()\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ PAM()\) |
5.8 CSH: Cash
Cash is the simplest contract: a pure holding of money, with no schedule, no interest and no maturity. Its only state is the notional, and its value at any time is just that balance carried with the contract-role sign. CSH exists so that cash positions can sit alongside other instruments in a portfolio and be analyzed uniformly; it generates no scheduled cash flow of its own, which is why its tables below are essentially empty.
|
CSH |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Nt}_{}\) |
\(\mathbf{Nt}_{t_0}=R(\texttt{CNTRL})\texttt{NT}\) |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathbf{Sd}’=t\) |
5.9 STK: Stock
A stock contract models an equity position. It is acquired at the purchase date PRD for the price observed then and disposed of at the termination date TD for the price observed at termination, collecting any dividends (DV) in between as observed cash flows. A holding has no natural end, so the analysis horizon \(t^{max}\) bounds an otherwise open position.
STK is a stateless cash-flow builder: it has no accruing state, only the observed purchase, dividend and sale flows, each signed by the position’s long/short role. It shares its definition with the commodity position (16).
|
STK |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathbf{Sd}’=t\) |
|
PRD |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(-1) \texttt{PPRD}\) |
\(\mathbf{Sd}’=t\) |
|
TD |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})\texttt{PTD}\) |
\(\mathbf{Sd}’=t\) |
|
DV\(^{(fix)}\) |
\(t^{DV^{(fix)}} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{DVNP}=\varnothing \\ \texttt{DVANX} & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})\texttt{DVNP}\) |
\(\mathbf{Sd}’=t\) |
|
DV |
\(\vec{t}^{DV} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{DVANX}=\varnothing \land \texttt{DVCL}=\varnothing \\ S(s,\texttt{DVCL},t^{max}) & \text{else} \end{array}\right.\) where \(s=\left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{DVANX} & \text{if}\quad \texttt{DVNP}=\varnothing \\ \texttt{DVANX}+\texttt{DVCL} & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})O^{rf}(concat(\text{\texttt{CID},"-DV"}),t)\) with \(concat(x,y,z)\) indicates the string concatenation function |
\(\mathbf{Sd}’=t\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ STK()\) |
5.10 COM: Commodity
A commodity position is an equity-style holding without income: it is bought at PRD and sold at TD at the prices observed on those dates, with no intervening dividends. It models physical-commodity or simple spot holdings and, like STK, is a stateless builder over observed prices. Formalized with STK as 16.
|
COM |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Sd}_{}\) |
Same as STK |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ STK()\) |
|
PRD |
Same as STK |
\(\mathrm{POF}\_ PRD\_ STK()\) |
\(\mathrm{STF}\_ PRD\_ STK()\) |
|
TD |
Same as STK |
\(\mathrm{POF}\_ PRD\_ STK()\) |
\(\mathrm{STF}\_ PRD\_ STK()\) |
5.11 FXOUT: Foreign Exchange Outright
An FX outright is an agreement to exchange two fixed notionals in different currencies on a single future settlement date at a pre-agreed rate. One leg delivers NT units of the base currency and the other delivers the counter-currency amount; settlement may be physical (both legs exchanged) or in net cash.
The payoff is therefore the signed difference of the two delivery legs, converted at the settlement-currency rate. The conservation metatheorem (36) records that the two legs net exactly to the par difference \(R\cdot (\texttt{NT}_1-\texttt{NT}_2)\) at unit FX. FXOUT is one of the cash-settled derivatives formalized as 17.
|
FXOUT |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
\(\mathbf{Md}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{MD} & \text{if}\quad \texttt{STD}=\varnothing \\ \texttt{STD} & \text{else} \end{array}\right.\) |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ STK()\) |
|
PRD |
Same as PAM |
\(\mathrm{POF}\_ PRD\_ STK()\) |
\(\mathrm{STF}\_ PRD\_ STK()\) |
|
TD |
Same as PAM |
\(\mathrm{POF}\_ TD\_ STK()\) |
\(\mathrm{STF}\_ TD\_ STK()\) |
|
STD |
\(t^{STD} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{DS}=\text{'D'} \\ \mathbf{Md}_{t_0} & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(\texttt{NT}-O^{rf}(i,\mathbf{Md}_{t})\texttt{NT2})\) where \(i=concat(\text{\texttt{CUR2},"/",\texttt{CUR}})\) and \(concat(x,y,z)\) indicates the string concatenation function |
\(\mathbf{Sd}’=t\) |
|
STD\(^{(1)}\) |
\(t^{STD} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{DS}=\text{'S'} \\ \mathbf{Md}_{t_0} & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})\texttt{NT}\) |
\(\mathbf{Sd}’=t\) |
|
STD\(^{(2)}\) |
\(t^{STD} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{DS}=\text{'S'} \\ \mathbf{Md}_{t_0} & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(-1)\texttt{NT2}\) |
\(\mathbf{Sd}’=t\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ CD\_ STK()\) |
5.12 SWPPV: Plain Vanilla Interest Rate Swap
A plain-vanilla interest-rate swap exchanges a fixed-rate and a floating-rate interest stream on a common notional over a sequence of periods. On each payment date the fixed leg pays \(N\cdot \texttt{fix}\cdot Y\) and the floating leg pays \(N\cdot \texttt{flt}\cdot Y\) for the period year-fraction \(Y\); the contract may settle the two legs gross (both flows) or net (their difference).
The net settlement is exactly \(R\cdot N\cdot (\texttt{fix}-\texttt{flt})\cdot Y\), which the formalization proves equals the difference of the two gross legs (36). SWPPV is given the dual model (SWPPV.Step, SWPPV.stf/pof): a period emits the two legs IPFX/IPFL (the floating leg advances the period boundary \(\mathbf{Sd}_{}\); a rate reset RR only repricings the floating rate), and the relation is proven to be the graph of stf. SWPPV and the composite SWAPS are formalized as 18.
SWPPV pays a fixed and a floating interest leg per period (with the relational Step and functional stf/pof models, proven to agree); SWAPS (§5.13) is a composite of two child legs run by the ordinary engine and combined gross or net.
|
SWPPV |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
Same as PAM |
||
|
\(\mathbf{Nt}_{}\) |
Same as PAM |
||
|
\(\mathbf{Ipnr}_{}\) |
\(\mathbf{Ipnr}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if} \quad \texttt{IED} {\gt} t_0 \\ \texttt{IPNR2} & \text{else} \end{array}\right.\) |
||
|
\(\mathbf{Ipac}_{}\) |
\(\mathbf{Ipac}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{IPAC} & \text{if} \quad \texttt{IPAC} \neq \varnothing \\ Y(t^-,t_0)\mathbf{Nt}_{t_0}(\texttt{IPNR}-\mathbf{Ipnr}_{t_0}) & \text{else} \end{array}\right.\) with \(t^- = \sup {t}, t \in t^{IP}, t{\lt}t_0\) |
||
|
\(\mathbf{Ipac1}_{}\) |
\(\mathbf{Ipac1}_{t_0} = Y(t^-,t_0)\mathbf{Nt}_{t_0}\texttt{IPNR}\) with \(t^- = \sup {t}, t \in t^{IP}, t{\lt}t_0\) |
||
|
\(\mathbf{Ipac2}_{}\) |
\(\mathbf{Ipac2}_{t_0} = Y(t^-,t_0)\mathbf{Nt}_{t_0}\mathbf{Ipnr}_{t_0}\) with \(t^- = \sup {t}, t \in t^{IP}, t{\lt}t_0\) |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = Y(\mathbf{Sd},t)\mathbf{Nt}_{t_0}(\texttt{IPNR}-\mathbf{Ipnr}_{t_0}) \\ \mathbf{Ipac1}’ & = Y(\mathbf{Sd},t)\mathbf{Nt}_{t_0}\texttt{IPNR} \\ \mathbf{Ipac2}’ & = Y(\mathbf{Sd},t)\mathbf{Nt}_{t_0}\mathbf{Ipnr}_{t_0} \\ \mathbf{Sd}’ & = t \end{array}\) |
|
PRD |
Same as PAM |
\(\mathrm{POF}\_ PRD\_ STK()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = Y(\mathbf{Sd},t)\mathbf{Nt}_{t_0}(\texttt{IPNR}-\mathbf{Ipnr}_{t_0}) \\ \mathbf{Ipac1}’ & = Y(\mathbf{Sd},t)\mathbf{Nt}_{t_0}\texttt{IPNR} \\ \mathbf{Ipac2}’ & = Y(\mathbf{Sd},t)\mathbf{Nt}_{t_0}\mathbf{Ipnr}_{t_0} \\ \mathbf{Sd}’ & = t \end{array}\) |
|
TD |
Same as PAM |
\(\mathrm{POF}\_ TD\_ STK()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = 0.0\\ \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Ipac1}’ & = 0.0 \\ \mathbf{Ipac2}’ & = 0.0 \\ \mathbf{Ipnr}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
IED |
Same as PAM |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = R(\texttt{CNTRL})\texttt{NT}\\ \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Ipac1}’ & = 0.0 \\ \mathbf{Ipac2}’ & = 0.0 \\ \mathbf{Ipnr}’ & = \texttt{IPNR2} \\ \mathbf{Sd}’ & = t \end{array}\) |
|
PR |
Same as PAM |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = 0.0\\ \mathbf{Ipnr}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
IP |
\(\vec{t}^{IP} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{DS}=\text{'D'} \\ \mathbf{Md}_{t_0} & \text{else if} \texttt{IPCL}=\varnothing \\ S(s,\texttt{IPCL},\mathbf{Md}_{t_0}) & \text{else} \end{array}\right.\) where \(s=\left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{IPANX} & \text{if}\quad \texttt{IPANX}\neq \varnothing \\ \texttt{IED}+\texttt{IPCL} & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(\mathbf{Ipac}+Y(\mathbf{Sd},t)(\texttt{IPNR}-\mathbf{Ipnr})\mathbf{Nt})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
IP\(^{(fix)}\) |
\(\vec{t}^{IP^{(fix)}} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{DS}=\text{'S'} \\ \mathbf{Md}_{t_0} & \text{else if} \texttt{IPCL}=\varnothing \\ S(s,\texttt{IPCL},\mathbf{Md}_{t_0}) & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(\mathbf{Ipac1}+Y(\mathbf{Sd},t)\texttt{IPNR}\mathbf{Nt})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac1}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
IP\(^{(var)}\) |
\(\vec{t}^{IP^{(var)}} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{DS}=\text{'S'} \\ \mathbf{Md}_{t_0} & \text{else if} \texttt{IPCL}=\varnothing \\ S(s,\texttt{IPCL},\mathbf{Md}_{t_0}) & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})(\mathbf{Ipac2}-\Delta \mathbf{Ipac})\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac2}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
RR |
\(\vec{t}^{RR}=S(s,\texttt{RRCL},\mathbf{Md}_{t_0})\) where \(s=\left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{RRANX} & \text{if}\quad \texttt{RRANX}\neq \varnothing \\ \texttt{IED}+\texttt{RRCL} & \text{else} \end{array}\right.\) |
\(\mathrm{POF}\_ RR\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = Y(\mathbf{Sd},t)\mathbf{Nt}_{t_0}(\texttt{IPNR}-\mathbf{Ipnr}_{t_0}) \\ \mathbf{Ipac1}’ & = Y(\mathbf{Sd},t)\mathbf{Nt}_{t_0}\texttt{IPNR} \\ \mathbf{Ipac2}’ & = Y(\mathbf{Sd},t)\mathbf{Nt}_{t_0}\mathbf{Ipnr}_{t_0} \\ \mathbf{Ipnr}’ & = \texttt{RRMLT}O^{rf}(\texttt{RRMO},t)+\texttt{RRSP} \\ \mathbf{Sd}’ & = t \end{array}\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ SWPPV()\) |
5.13 SWAPS: Swap
The general swap is a composite contract: it references two child contracts — its two legs — runs each through the ordinary execution engine, and then combines their cash flows. The legs may be any ACTUS contracts (for instance a fixed-rate and a floating-rate PAM or ANN), and the swap settles them either gross (passing both legs’ flows through) or net (offsetting same-date flows).
This compositional definition is what lets ACTUS express swaptions, asset swaps and other structured exchanges as hierarchies of simpler contracts (§4). SWAPS is formalized with SWPPV as 18.
|
SWAPS |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
\(\mathbf{Md}_{t_0}=\max (U^{sv}(\texttt{CTST}_{FirstLeg}^{Contract},t_0,\mathbf{Tmd}_{}), U^{sv}(\texttt{CTST}_{SecondLeg}^{Contract},t_0,\mathbf{Tmd}_{}))\) |
||
|
\(\mathbf{Ipac}_{}\) |
\(\mathbf{Ipac}_{t_0} = U^{sv}(\texttt{CTST}_{FirstLeg}^{Contract},t_0,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(1)}\} ) + U^{sv}(\texttt{CTST}_{SecondLeg}^{Contract},t_0,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(2)}\} )\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} r^{(1)} & = \left\{ \begin{array}{@{}l@{\quad }l@{}} RPA & \text{if}\quad \texttt{CNTRL}=RFL \\ RPL & \text{else} \end{array}\right. \\ r^{(2)} & = \left\{ \begin{array}{@{}l@{\quad }l@{}} RPL & \text{if}\quad \texttt{CNTRL}=RFL \\ RPA & \text{else} \end{array}\right. \end{array}\) |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = U^{sv}(\texttt{CTST}_{FirstLeg}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(1)}\} ) \\ & + U^{sv}(\texttt{CTST}_{SecondLeg}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(2)}\} ) \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^-,t)}{Y(t^-,t^+)}\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) |
|
PRD |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t) ( (-1)\texttt{PPRD}\) \(\qquad + U^{sv}(\texttt{CTST}_{FirstLeg}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(1)}\} )\) \(\qquad + U^{sv}(\texttt{CTST}_{SecondLeg}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(2)}\} ))\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = U^{sv}(\texttt{CTST}_{FirstLeg}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(1)}\} ) \\ & + U^{sv}(\texttt{CTST}_{SecondLeg}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(2)}\} ) \\ \mathbf{Sd}’ & = t \end{array}\) |
|
TD |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t) (\texttt{PTD}\) \(\qquad + U^{sv}(\texttt{CTST}_{FirstLeg}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(1)}\} )\) \(\qquad + U^{sv}(\texttt{CTST}_{SecondLeg}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(2)}\} ))\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
\(k\) |
\(\{ e_t^k\} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \{ e_t^{k,1}\} \cup \{ e_s^{l,2}\} & \text{if}\quad \texttt{DS}=\text{'D'} \\ \{ e_t^{k,1}\} + \{ e_s^{l,2}\} & \text{else} \end{array}\right.\) with \(\{ e_t^{k,1}\} +\{ e_s^{l,2}\} = U \cup V\) and \(\begin{array}{@{}r@{}l@{\quad }l@{}} U & = \{ e_t^{k,1}\} \triangle \{ e_s^{l,2}\} \\ V & = \{ x_\tau ^m+y_\tau ^m\} \end{array}\) where for any two events \(x_t^k\in \{ e_t^{k,1}\} \), \(y_s^l\in \{ e_s^{l,2}\} \) we have \(x_t^k=y_s^l \iff t=s \land k=l\), \(\triangle \) is the distinct union-operator, and \(x_t^k+y_s^l=z_\tau ^m\) with \(\tau =t=s\), \(m=k=l\in \{ \text{IED,IP,PR}\} \) indicates that any two congruent events of type IED, IP, or PR are merged into a new aggregate event (see payoff and state transition function below). with \(\begin{array}{@{}r@{}l@{\quad }l@{}} \{ e_t^{k,1}\} & = U^{ev}(\texttt{CTST}_{FirstLeg}^{Contract},t_0 \mid \{ \texttt{CNTRL}=r^{(1)}\} ) \\ \{ e_s^{l,2}\} & = U^{ev}(\texttt{CTST}_{SecondLeg}^{Contract},t_0 \mid \{ \texttt{CNTRL}=r^{(2)}\} ) \\ r^{(1)} & = \left\{ \begin{array}{@{}l@{\quad }l@{}} RPA & \text{if}\quad \texttt{CNTRL}=RFL \\ RPL & \text{else} \end{array}\right. \\ r^{(2)} & = \left\{ \begin{array}{@{}l@{\quad }l@{}} RPL & \text{if}\quad \texttt{CNTRL}=RFL \\ RPA & \text{else} \end{array}\right. \end{array}\) |
||
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ SWAPS()\) |
|
\(z_\tau ^m\) |
\(f(x_\tau ^m)+f(y_\tau ^m)\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = U^{sv}(\texttt{CTST}_{FirstLeg}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(1)}\} ) \\ & + U^{sv}(SecondLeg,t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(2)}\} ) \\ \mathbf{Sd}’ & = t \end{array}\) |
|
5.14 CAPFL: Cap–Floor
A cap (floor) is a rate option layered on a variable-rate underlying: it pays the holder whenever the underlying’s reset rate rises above the cap (falls below the floor), compensating the rate excess on the underlying’s notional. It is the standard hedge against adverse rate moves on a floating-rate loan.
CAPFL is defined over a child contract: at each of the underlying’s reset dates it observes the would-be reset rate \(r\) and pays \(\max (r-\texttt{cap},0)\) or \(\max (\texttt{floor}-r,0)\) on the period’s notional and year-fraction. The intrinsic-value metatheorem (35) proves these payoffs are always non-negative. Formalized with the derivatives as 17.
|
CAPFL |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
\(\mathbf{Md}_{t_0}=\max (U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t_0,\mathbf{Tmd}_{} \mid \{ \texttt{CNTRL}=RPA\} ),\) \(\qquad U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t_0,\mathbf{Tmd}_{} \mid \{ \texttt{CNTRL}=RPA,\texttt{RRLC}=\texttt{RRLC},\texttt{RRLF}=\texttt{RRLF}\} ))\) |
||
|
\(\mathbf{Ipac}_{}\) |
\(\mathbf{Ipac}_{t_0} = R(\texttt{CNTRL})abs(\) \(\qquad U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t_0,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=r^{(1)}\} )\) \(\qquad - U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t_0,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=RPA,\texttt{RRLC}=\texttt{RRLC},\texttt{RRLF}=\texttt{RRLF}\} ))\) |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = R(\texttt{CNTRL})abs(U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=RPA\} ) \\ & - U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=RPA, \\ & \qquad \texttt{RRLC}=\texttt{RRLC},\texttt{RRLF}=\texttt{RRLF}\} )) \\ \mathbf{Sd}’ & = t \end{array}\) |
|
PRD |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t) ( (-1)\texttt{PPRD} + R(\texttt{CNTRL})abs(\) \(\qquad U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=RPA\} ) - \) \(\qquad U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=RPA,\) \(\qquad \qquad \texttt{RRLC}=\texttt{RRLC},\texttt{RRLF}=\texttt{RRLF}\} )))\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = R(\texttt{CNTRL})abs(U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=RPA\} ) \\ & - U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=RPA, \\ & \qquad \texttt{RRLC}=\texttt{RRLC},\texttt{RRLF}=\texttt{RRLF}\} )) \\ \mathbf{Sd}’ & = t \end{array}\) |
|
TD |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t) (\texttt{PTD}\) + R(CNTRL)abs( \(\qquad U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=RPA\} ) - \) \(\qquad U^{sv}(\texttt{CTST}_{Underlying}^{Contract},t,\mathbf{Ipac}_{} \mid \{ \texttt{CNTRL}=RPA,\) \(\qquad \qquad \texttt{RRLC}=\texttt{RRLC},\texttt{RRLF}=\texttt{RRLF}\} )))\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
\(k\) |
\(\{ e_t^k\} = \{ x_t^k+y_s^l\} \) for all events \(x_t^k\in U^{ev}(\texttt{CTST}_{Underlying}^{Contract},t_0 \mid \{ \texttt{CNTRL}=RPA\} )\), \(y_s^l\in U^{ev}(\texttt{CTST}_{Underlying}^{Contract},t_0 \mid \{ \texttt{CNTRL}=RPA,\texttt{RRLC}=\texttt{RRLC},\texttt{RRLF}=\texttt{RRLF}\} )\) with \(t=s \land k=l=IP\). That is, any two congruent events of the child-contract schedule, evaluated once without \(\texttt{RRLC},\texttt{RRLF}\) defined and once with the attributes defined, which are of type IP are merged into a new aggregate event (see payoff and state transition function below). |
||
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ CAPFL()\) |
|
\(z_\tau ^m\) |
\(R(\texttt{CNTRL})abs(f(x_\tau ^m)-f(y_\tau ^m))\) where \(abs(u)\) defines that the absolute value of \(u\) is taken. |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Ipac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
5.15 OPTNS: Option
An option is a European call or put on an underlying instrument, exercised at a single maturity. At exercise it cash-settles at its intrinsic value — \(\max (S-K,0)\) for a call, \(\max (K-S,0)\) for a put — where \(S\) is the observed underlying price and \(K\) the strike; before maturity it carries only its premium.
Like CAPFL it is defined over a child contract through the child-contract observer (§4). The formalization proves the intrinsic value is non-negative and that a call is in the money exactly when \(S{\gt}K\) (35). Formalized with the derivatives as 17.
|
OPTNS |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Xd}_{}\) |
\(\mathbf{Xd}_{t_0} = \texttt{XD}\) |
||
|
\(\mathbf{Xa}_{}\) |
\(\mathbf{Xa}_{t_0} = \texttt{XA}\) |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathbf{Sd}’ = t\) |
|
PRD |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)(-1)\texttt{PPRD}\) |
\(\mathrm{STF}\_ PRD\_ STK()\) |
|
TD |
Same as PAM |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)\texttt{PTD}\) |
\(\mathrm{STF}\_ TD\_ STK()\) |
|
MD |
\(t^{MD} = \texttt{MD}\) |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Xd}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Xd} & \text{if}\quad \mathbf{Xd} \neq \varnothing \\ \varnothing & \text{ else if}\quad x=0.0 \\ t & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} x & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \max (S_t-\texttt{OPS1},0) & \text{if}\quad \texttt{OPTP}=\text{'C'} \\ \max (\texttt{OPS1}-S_t,0) & \text{else if}\quad \texttt{OPTP}=\text{'P'} \\ \max (S_t-\texttt{OPS1},0) & \text{else} \\ \qquad + \max (\texttt{OPS2}-S_t,0) & \end{array}\right. \\ S_t & = O^{rf}(U^{ca}(\texttt{CTST}_{Underlying}^{Contract},MOC),t) \end{array}\) |
|
XD |
\(t^{XD} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Xd}_{t_0} & \text{if}\quad \mathbf{Xd}_{t_0} \neq \varnothing \\ \inf \tau (e^{XD}) & \text{else if}\quad \tau (e^{XD}) \neq \varnothing \wedge \texttt{OPXT} \neq ’E’\\ \varnothing & \text{else} \end{array}\right.\) with \(e^{XD} = e\in O^{ev}(i,\texttt{XD},t_0) | \tau (e) \leq \mathbf{Md}_{t_0}\) and \(i = \texttt{CTST}_{CoveredContract}^{Contract}(i)\) |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Xa}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \max (S_t-\texttt{OPS1},0) & \text{if}\quad \texttt{OPTP}=\text{'C'} \\ \max (\texttt{OPS1}-S_t,0) & \text{else if}\quad \texttt{OPTP}=\text{'P'} \\ \max (S_t-\texttt{OPS1},0) & \text{else} \\ \qquad + \max (\texttt{OPS2}-S_t,0) & \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) with \(S_t=O^{rf}(U^{ca}(\texttt{CTST}_{Underlying}^{Contract},MOC),t)\) |
|
STD |
\(t^{STD} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad \texttt{XD}=\varnothing \\ \texttt{XD} + \texttt{STD} & \text{else} \end{array}\right.\) |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})\mathbf{Xa}\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Xa}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ OPTNS()\) |
5.16 FUTUR: Future
A future is a linear forward on an underlying: at settlement it pays the difference between the observed underlying price \(S\) and the agreed contract (futures) price \(F\), that is \(S-F\), scaled by the contract size. Unlike an option it is symmetric — the holder gains or loses linearly with the underlying — so its payoff may take either sign.
FUTUR is the simplest of the derivative builders defined over a child underlying, and is formalized with them as 17.
|
FUTUR |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Xd}_{}\) |
Same as OPTNS |
||
|
\(\mathbf{Xa}_{}\) |
Same as OPTNS |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ OPTNS()\) |
|
PRD |
Same as PAM |
\(\mathrm{POF}\_ PRD\_ OPTNS()\) |
\(\mathrm{STF}\_ PRD\_ STK()\) |
|
TD |
Same as PAM |
\(\mathrm{POF}\_ TD\_ OPTNS()\) |
\(\mathrm{STF}\_ TD\_ STK()\) |
|
MD |
Same as OPTNS |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Xd}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if}\quad x=0.0 \\ t & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} x & = S_t-\texttt{PFUT} \\ S_t & = O^{rf}(U^{ca}(\texttt{CTST}_{Underlying}^{Contract},MOC),t) \end{array}\) |
|
XD |
Same as OPTNS |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Xa}’ & = S_t-\texttt{PFUT} \\ \mathbf{Sd}’ & = t \end{array}\) with \(S_t=O^{rf}(U^{ca}(\texttt{CTST}_{Underlying}^{Contract},MOC),t)\) |
|
STD |
Same as OPTNS |
\(\mathrm{POF}\_ STD\_ OPTNS()\) |
\(\mathrm{STF}\_ STD\_ OPTNS()\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ FUTUR()\) |
5.17 CEG: Credit Enhancement Guarantee
A credit-enhancement guarantee is a third-party promise to cover the losses of one or more covered contracts. The guarantor receives a premium at inception and, if a covered contract suffers an observed credit event, pays out the covered exposure — the sum of the covered contracts’ outstanding notionals plus, for a guarantee, their accrued interest.
CEG is a composed contract: it references its covered contracts through CTST (§4) and reads their state through the child-contract observer to size the exposure at the moment of default. The payout therefore carries the guarantor’s role sign and is bounded below by zero (37). CEG and the collateral variant CEC are formalized as 19.
Divergence from the reference data. Here the formalization is the arbiter. The executable engine reproduces every gated reference contract exactly, but one CEG reference case (guarantee14) carries a reference value that disagrees with the CEG payoff specified below — the engine computes the value this specification prescribes. We record it as a known discrepancy in the reference suite rather than a defect of the specification.
CEG (guarantee) and CEC (collateral, §5.18) over covered contracts: a premium at purchase, and on a covered contract’s observed credit event the covered exposure settles — capped at the observed collateral value for CEC.
|
CEG |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
\(\mathbf{Md}_{t_0}=\left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{MD} & \text{if}\quad \texttt{MD}\neq \varnothing \\ \max (\tau (\{ e_t^k\} )) & \text{else} \end{array}\right.\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} \{ e_t^k\} & = \{ e_t^{k,1}\} \cup \{ e_t^{k,2}\} \cup ...\cup \{ e_t^{k,n}\} \\ \{ e_t^{k,i}\} & = U^{ev}(\texttt{CTST}_{CoveredContract}^{Contract}(i),t_0 \mid \{ \\ \} ) n & = \mid \texttt{CTST}_{CoveredContract}^{Contract} \mid \end{array}\) |
||
|
\(\mathbf{Nt}_{}\) |
\(\mathbf{Nt}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if}\quad t_0\geq \mathbf{Md}_{t_0} \\ \texttt{CECV}R(\texttt{CNTRL})\texttt{NT} & \text{else if}\quad \texttt{NT}\neq \varnothing \\ \texttt{CECV}R(\texttt{CNTRL})\sum _{i=1}^{\mid I\mid } n_i & \text{else} \end{array}\right.\) with \(n_i=\left\{ \begin{array}{@{}l@{\quad }l@{}} U^{sv}(I(i),t_0,\mathbf{Nt}_{} \mid \{ x\} ) & \text{if}\quad \texttt{CEGE}=NO \\ U^{sv}(I(i),t_0,\mathbf{Nt}_{} \mid \{ x\} ) & \text{else if}\quad \texttt{CEGE}=NI \\ \quad + U^{sv}(I(i),t_0,\mathbf{Ipac}_{} \mid \{ x\} ) & \\ O^{rf}(U^{ca}(I(i),MOC),t_0) & \text{else} \end{array}\right.\) where \(I=\texttt{CTST}_{CoveredContract}^{Contract}\) |
||
|
\(\mathbf{Feac}_{}\) |
\(\mathbf{Feac}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if} \quad \texttt{FER}=\varnothing \\ \texttt{FEAC} & \text{else if} \quad \texttt{FEAC} \neq \varnothing \\ \mathbf{Nt}_{t_0}Y(t^-,t_0)\texttt{FER} & \text{else if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t_0)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right.\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
||
|
\(\mathbf{Xd}_{}\) |
Same as OPTNS |
||
|
\(\mathbf{Xa}_{}\) |
Same as OPTNS |
||
|
\(\mathbf{Prf}_{}\) |
Same as PAM |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) |
|
PRD |
Same as PAM |
\(\mathrm{POF}\_ PRD\_ STK()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Nt} & \text{if}\quad \texttt{NT}\neq \varnothing \\ \texttt{CECV}\sum _{i=1}^{\mid I\mid } n_i & \text{else} \end{array}\right. \\ \mathbf{Feac}’ & = \mathbf{Feac}_{t_0} \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} n_i & = \left\{ \begin{array}{@{}l@{\quad }l@{}} U^{sv}(I(i),t,\mathbf{Nt}_{} \mid \{ \} ) & \text{if}\quad \texttt{CEGE}=NO \\ U^{sv}(I(i),t,\mathbf{Nt}_{} \mid \{ \} ) & \text{else if}\quad \texttt{CEGE}=NI \\ \quad + U^{sv}(I(i),t,\mathbf{Ipac}_{} \mid \{ \} ) & \\ O^{rf}(U^{ca}(I(i),MOC),t) & \text{else} \end{array}\right. \\ t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) where \(I=\texttt{CTST}_{CoveredContract}^{Contract}\) |
|
TD |
Same as PAM |
||
|
FP |
\(\vec{t}^{FP} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{FER}=\varnothing \lor \texttt{FER}=0 \\ S(s,\texttt{FECL},T) & \text{else} \end{array}\right.\) with \(s = \left\{ \begin{array}{@{}l@{\quad }l@{}} \varnothing & \text{if} \quad \texttt{FEANX}=\varnothing \land \texttt{FECL}=\varnothing \\ \texttt{PRD}+\texttt{FECL} & \text{else if} \quad \texttt{FEANX} = \varnothing \\ \texttt{FEANX} & \text{else} \end{array}\right.\) \(T = \left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{MD} & \text{if}\quad t^{XD} = \varnothing \\ t^{XD} & \text{else} \end{array}\right.\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}}& X_{\texttt{CUR}}^{\texttt{CURS}}(t)R(\texttt{CNTRL})\texttt{FER} & \text{if} \quad \texttt{FEB}=A \\ & X_{\texttt{CUR}}^{\texttt{CURS}}(t)\left(\mathbf{Feac} + \mathbf{Nt}Y(t^-,t)\texttt{FER}\right) & \text{else} \end{array}\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Nt} & \text{if}\quad \texttt{NT}\neq \varnothing \\ \texttt{CECV}\sum _{i=1}^{\mid I\mid } n_i & \text{else} \end{array}\right. \\ \mathbf{Feac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} n_i & = \left\{ \begin{array}{@{}l@{\quad }l@{}} U^{sv}(I(i),t,\mathbf{Nt}_{} \mid \{ \} ) & \text{if}\quad \texttt{CEGE}=NO \\ U^{sv}(I(i),t,\mathbf{Nt}_{} \mid \{ \} ) & \text{else if}\quad \texttt{CEGE}=NI \\ \quad + U^{sv}(I(i),t,\mathbf{Ipac}_{} \mid \{ \} ) & \\ O^{rf}(U^{ca}(I(i),MOC),t) & \text{else} \end{array}\right. \\ t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) where \(I=\texttt{CTST}_{CoveredContract}^{Contract}\) |
|
MD |
\(t^{MD}=\left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Md}_{t_0} & \text{if}\quad t^{XD}=\varnothing \\ \varnothing & \text{else} \end{array}\right.\) |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
XD |
\(t^{XD} = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Xd}_{t_0} & \text{if}\quad \mathbf{Xd}_{t_0} \neq \varnothing \\ \inf \tau (e^{CE}) & \text{else if}\quad \tau (e^{CE}) \neq \varnothing \\ \varnothing & \text{else} \end{array}\right.\) with \(e^{CE} = e\in O^{ev}(i,\texttt{CE},t_0) | \mathbf{Prf}_{\tau (e)^+}==\texttt{CET}\wedge \) \( \tau (e) \leq \mathbf{Md}_{t_0}\) and \(i = \texttt{CTST}_{CoveredContract}^{Contract}(i)\) |
\(\mathrm{POF}\_ XD\_ OPTNS()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Nt} & \text{else if}\quad \texttt{NT}\neq \varnothing \\ \texttt{CECV}\sum _{i=1}^{\mid I\mid } n_i & \text{else} \end{array}\right. \\ \mathbf{Feac}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} \mathbf{Feac} + Y(\mathbf{Sd},t)\mathbf{Nt}\texttt{FER} & \text{if} \quad \texttt{FEB}=\text{'N'} \\ \frac{Y(t^{FP-},t)}{Y(t^{FP-},t^{FP+})}R(\texttt{CNTRL})\texttt{FER} & \text{else} \end{array}\right. \\ \mathbf{Xa}’ & = \texttt{CECV}\mathbf{Nt} \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} n_i & = \left\{ \begin{array}{@{}l@{\quad }l@{}} U^{sv}(I(i),t,\mathbf{Nt}_{} \mid \{ \} ) & \text{if}\quad \texttt{CEGE}=NO \\ U^{sv}(I(i),t,\mathbf{Nt}_{} \mid \{ \} ) & \text{else if}\quad \texttt{CEGE}=NI \\ \quad + U^{sv}(I(i),t,\mathbf{Ipac}_{} \mid \{ \} ) & \\ O^{rf}(U^{ca}(I(i),MOC),t) & \text{else} \end{array}\right. \\ t^{FP-} & = \sup t \in \vec{t}^{FP}\mid t{\lt}t_0 \\ t^{FP+} & = \inf t \in \vec{t}^{FP}\mid t{\gt}t_0 \end{array}\) where \(I=\texttt{CTST}_{CoveredContract}^{Contract}\) |
|
STD |
Same as OPTNS |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)\left(\mathbf{Xa}+\mathbf{Feac}\right)\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = 0.0 \\ \mathbf{Feac}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
CE |
Same as PAM |
\(\mathrm{POF}\_ CE\_ PAM()\) |
\(\mathrm{STF}\_ AD\_ CEG()\) |
5.18 CEC: Credit Enhancement Collateral
Credit-enhancement collateral is a guarantee backed by posted assets rather than a counterparty’s promise: on a covered credit event the protection pays the covered exposure, but capped at the observed value of the collateral. The payout is thus \(\min (\text{coverage}\cdot \text{exposure},\ \text{collateral value})\) — it can never exceed either the covered claim or the collateral on hand.
This cap is exactly the bound proved in 37. CEC is formalized with CEG as 19.
|
CEC |
|||
|
State Variables |
|||
|
Variable |
Initialization per \(t_0\) |
||
|
\(\mathbf{Md}_{}\) |
\(\mathbf{Md}_{t_0}=\left\{ \begin{array}{@{}l@{\quad }l@{}} \texttt{MD} & \text{if}\quad \texttt{MD}\neq \varnothing \\ \max (\tau (\{ e_t^k\} )) & \text{else} \end{array}\right.\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} \{ e_t^k\} & = \{ e_t^{k,1}\} \cup \{ e_t^{k,2}\} \cup ...\cup \{ e_t^{k,n}\} \\ \{ e_t^{k,i}\} & = U^{ev}(\texttt{CTST}_{CoveredContract}^{Contract}(i),t_0 \mid \{ \\ \} ) n & = \mid \texttt{CTST}_{CoveredContract}^{Contract} \mid \end{array}\) |
||
|
\(\mathbf{Nt}_{}\) |
\(\mathbf{Nt}_{t_0} = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if}\quad t_0\geq \mathbf{Md}_{t_0} \\ \min \left(\sum _{j=1}^{\mid J\mid } v_j, \texttt{CECV}\sum _{i=1}^{\mid I\mid } n_i\right) & \text{else} \end{array}\right.\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} n_i & = \left\{ \begin{array}{@{}l@{\quad }l@{}} U^{sv}(I(i),t_0,\mathbf{Nt}_{} \mid \{ \} ) & \text{if}\quad \texttt{CEGE}=NO \\ U^{sv}(I(i),t_0,\mathbf{Nt}_{} \mid \{ \} ) & \text{else if}\quad \texttt{CEGE}=NI \\ \quad + U^{sv}(I(i),t_0,\mathbf{Ipac}_{} \mid \{ \} ) & \\ O^{rf}(U^{ca}(I(i),MOC),t_0) & \text{else} \end{array}\right. \\ v_j & = O^{rf}(U^{ca}(J(j),MOC),t_0) \\ I & = \texttt{CTST}_{CoveredContract}^{Contract} \\ J & = \texttt{CTST}_{CoveringContract}^{Contract}\end{array}\) |
||
|
\(\mathbf{Sd}_{}\) |
Same as PAM |
||
|
Events |
|||
|
Event |
Schedule |
Payoff Function |
State Transition |
|
AD |
Same as PAM |
\(\mathrm{POF}\_ AD\_ PAM()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = \left\{ \begin{array}{@{}l@{\quad }l@{}} 0.0 & \text{if}\quad t\geq \mathbf{Md}_{t_0} \\ \min \left(\sum _{j=1}^{\mid J\mid } v_j, \texttt{CECV}\sum _{i=1}^{\mid I\mid } n_i\right) & \text{else} \end{array}\right. \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} n_i & = \left\{ \begin{array}{@{}l@{\quad }l@{}} U^{sv}(I(i),t_0,\mathbf{Nt}_{} \mid \{ \} ) & \text{if}\quad \texttt{CEGE}=NO \\ U^{sv}(I(i),t_0,\mathbf{Nt}_{} \mid \{ \} ) & \text{else if}\quad \texttt{CEGE}=NI \\ \quad + U^{sv}(I(i),t_0,\mathbf{Ipac}_{} \mid \{ \} ) & \\ O^{rf}(U^{ca}(I(i),MOC),t_0) & \text{else} \end{array}\right. \\ v_j & = O^{rf}(U^{ca}(J(j),MOC),t_0) \\ I & = \texttt{CTST}_{CoveredContract}^{Contract} \\ J & = \texttt{CTST}_{CoveringContract}^{Contract}\end{array}\) |
|
XD |
Same as CEG |
\(\mathrm{POF}\_ XD\_ OPTNS()\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = \min \left(\sum _{j=1}^{\mid J\mid } v_j, \texttt{CECV}\sum _{i=1}^{\mid I\mid } n_i\right) \\ \mathbf{Sd}’ & = t \end{array}\) with \(\begin{array}{@{}r@{}l@{\quad }l@{}} n_i & = \left\{ \begin{array}{@{}l@{\quad }l@{}} U^{sv}(I(i),t_0,\mathbf{Nt}_{} \mid \{ \} ) & \text{if}\quad \texttt{CEGE}=NO \\ U^{sv}(I(i),t_0,\mathbf{Nt}_{} \mid \{ \} ) & \text{else if}\quad \texttt{CEGE}=NI \\ \quad + U^{sv}(I(i),t_0,\mathbf{Ipac}_{} \mid \{ \} ) & \\ O^{rf}(U^{ca}(I(i),MOC),t_0) & \text{else} \end{array}\right. \\ v_j & = O^{rf}(U^{ca}(J(j),MOC),t_0) \\ I & = \texttt{CTST}_{CoveredContract}^{Contract} \\ J & = \texttt{CTST}_{CoveringContract}^{Contract}\end{array}\) |
|
STD |
Same as CEG |
\(X_{\texttt{CUR}}^{\texttt{CURS}}(t)\mathbf{Nt}\) |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
|
MD |
Same as CEG |
0.0 |
\(\begin{array}{@{}r@{}l@{\quad }l@{}} \mathbf{Nt}’ & = 0.0 \\ \mathbf{Sd}’ & = t \end{array}\) |
5.19 Schedule generation and execution
genSchedule builds the full event Schedule (IED, IP/IPCI, PR, RR/RRF, FP, SC, MD, …) for a stateful contract from its dictionary terms, following the Contract-Schedule tables above; runSchedule then folds the contract’s stf/pof over it. This is the type-agnostic core shared by every contract family.
6 Metatheorems
The formalization adds guarantees the original specification never states: the relational and functional models agree, status dates advance monotonically, maturity zeroes the notional, and — over \(\mathbb {R}\) — a battery of quantitative bounds and conservation laws hold of every execution.
For each of the eight stateful contracts (PAM, LAM, NAM, ANN, CLM and LAX, SWPPV, UMP) every relational step lands on the functional next-state for some event and time; conversely every admissible event/time yields a step. Each relation is exactly the graph of its stf.
Along any execution trace the status date is non-decreasing: each step requires \(\mathtt{Sd} \le t\) and sets \(\mathtt{Sd} := t\).
The maturity event zeroes the notional principal (and accrued interest and fees); termination additionally zeroes the interest rate.
6.1 Quantitative bounds and conservation (over \(\mathbb {R}\))
After a rate reset the nominal rate lies within the life floor/cap window \([\mathtt{RRLF}, \mathtt{RRLC}]\) (whenever both are present and well-ordered). Holds for PAM, for ANN (by reuse of PAM’s rate logic), and for SWPPV’s floating-rate reset. With every cap/floor absent the reset instead returns the raw repricing target \(O^{rf}(\mathtt{RRMO},t)\cdot \mathtt{RRMLT}+\mathtt{RRSP}\) (pam_rr_uncapped).
A principal redemption never overshoots: with a sign-normalised nonnegative state the post-redemption notional stays in \([0, \mathtt{Nt}]\), and the redeemed amount never exceeds the outstanding notional in magnitude (\(|\, \mathrm{redeemed}\, | \le |\mathtt{Nt}|\)).
With a strictly positive notional and instalment a redemption strictly decreases the notional (guaranteed progress); once the instalment reaches the outstanding notional the step drives it to exactly \(0\) (clean repayment).
The IPCI event moves accrued interest into the notional and resets accrued interest to \(0\): value is relocated, not created. (This one holds definitionally at any amount type.)
PRTrace is the sub-relation of the LAM execution trace consisting of zero or more admissible principal-redemption (PR) steps — the regime in which the notional should be conserved (events like IED/IPCI reset or grow it).
Along an entire principal-redemption trace the notional stays in \([0, \mathtt{Nt}_0]\) and never increases in magnitude — the single-step non-overshoot lifted to whole executions by induction over the trace. Every PRTrace is moreover a genuine LAM execution trace, so this is a statement about real runs.
IPCITrace is the chain of zero or more admissible interest capitalizations (IPCI) of a UMP deposit; ipciFactor accumulates the multiplicative growth factor \(\prod _i (1 + \mathtt{rate}\cdot Y_i)\) along it.
Along a capitalization trace the notional grows multiplicatively to \(\mathtt{Nt}' = \mathtt{Nt}_0 \cdot \prod _i (1 + \mathtt{rate}\cdot Y_i)\); the nominal rate is invariant under IPCI (justifying the single \(\mathtt{rate}\)), and with a non-negative rate and year fraction each capitalization never shrinks the deposit.
LAXPRTrace is the chain of zero or more admissible LAX principal redemptions (PR) with non-negative instalments.
On the long side (\(\mathrm{sign} \ge 0\)) a LAX redemption with a non-negative instalment never increases the notional, so along an entire redemption trace \(\mathtt{Nt}' \le \mathtt{Nt}_0\) (monotone repayment). Unlike LAM’s capped redeemed this is a one-sided bound, since STF_PR_LAX subtracts the raw instalment. Every such trace is a genuine LAX execution.
A swap exchanges interest, not principal: no SWPPV event moves the notional, and only a rate reset (RR) changes the floating rate. Status dates are non-decreasing along any execution (even though the fixed leg and reset leave \(\mathbf{Sd}_{}\) untouched and only the floating leg advances it).
6.2 Payoff bounds for the derivative and credit families (over \(\mathbb {R}\))
The cap/floor rate-excess kernel \(\max (r - \mathtt{cap}, 0) + \max (\mathtt{floor} - r, 0)\) and the European call/put intrinsics \(\max (S - K, 0)\), \(\max (K - S, 0)\) are all \(\ge 0\), so a long cap, floor, or option never settles negative; a call is in the money exactly when the underlying exceeds the strike.
An FX outright’s two delivery legs net to the par difference \(R \cdot (\mathtt{Nt_1} - \mathtt{Nt_2})\) at unit FX; a swap’s per-period fixed and floating legs net to \(R \cdot N \cdot (\mathtt{fix} - \mathtt{flt}) \cdot Y\) — exactly what the net-settlement fold computes from the two gross legs. For SWPPV this is now proven on the actual stf/pof state machine (swppv_pof_net), and at par (\(\mathtt{fix}=\mathtt{flt}\)) the netted period flow is zero.
A collateral payout \(\min (\mathtt{coverage}\cdot \mathtt{exposure}, \mathtt{value})\) never exceeds either the posted collateral value or the covered claim; the covered exposure, a sum of per-leg magnitudes, is non-negative, so the payout carries the contract-role sign.
7 Data Dictionary
The tables below reproduce the ACTUS Data Dictionary (ACTUS Financial Research Foundation, v1.4, CC-BY-SA-4.0), the normative glossary of the standard. They explain every contract-term, state-variable and contract-type acronym used throughout this document; the lifecycle event types (IED, IP, PR, …) are not part of the dictionary and so are not listed here. Acronyms in typewriter font elsewhere in the blueprint link to their entry below.
7.1 Contract Terms
|
Acronym |
Name |
Description |
|
Amortization Date |
This Date is used to calculate the annuity amounts for ANN and ANX NGX CT’s. Needs only to be set in case where the contract balloon at MD and MD is less than AD. |
|
|
Array Fixed Variable |
For array-type rate reset schedules, this attributes defines the meaning of ARRATE. |
|
|
Array Increase Decrease |
Indicates whether a certain PRNXT element in ARPRNX increases the principal (NT) or decreases it. Applies only for ANX, NAX, LAX Maturity CTs. For all other Maturity CTs the first principal payment is always in the opposite direction of all other (following) payments. |
|
|
Array Cycle Anchor Date Of Interest Payment |
Same like IPANX but as array |
|
|
Array Cycle Of Interest Payment |
Same like IPCL but as array |
|
|
Array Cycle Anchor Date Of Principal Redemption |
Same like PRANX but as array |
|
|
Array Cycle Of Principal Redemption |
Same like PRCL but as array |
|
|
Array Next Principal Redemption Payment |
Same like PRNXT but as array |
|
|
Array Rate |
For array-type rate reset schedules, this attribute represents either an interest rate (corresponding to IPNR) or a spread (corresponding to RRSP). Which case applies depends on the attribute ARFIXVAR: if ARFIXVAR=FIX then it represents the new IPNR and if ARFIXVAR=VAR then the applicable RRSP. |
|
|
Array Cycle Anchor Date Of Rate Reset |
Same like RRANX but as array |
|
|
Array Cycle Of Rate Reset |
Same like RRCL but as array |
|
|
Boundary Crossed Flag |
Initializes the value of Boundary Crossed Flag state variable at statusDate |
|
|
Business Day Convention |
BDC’s are linked to a calendar. Calendars have working and non-working days. A BDC value other than N means that cash flows cannot fall on non-working days, they must be shifted to the next business day (following) or the previous on (preceding). These two simple rules get refined twofold: - Following modified (preceding): Same like following (preceding), however if a cash flow gets shifted into a new month, then it is shifted to preceding (following) business day. - Shift/calculate (SC) and calculate/shift (CS). Accrual, principal, and possibly other calculations are affected by this choice. In the case of SC first the dates are shifted and after the shift cash flows are calculated. In the case of CS it is the other way round. Attention: Does not affect non-cyclical dates such as PRD, MD, TD, IPCED since they can be set to the correct date directly. |
|
|
Boundary Direction |
Boundary direction specifies the direction of motion in the underlying asset’s price which will be considered a valid crossing of the boundary and trigger the boundary effect changing which, if any, of the boundary legs is active. |
|
|
Boundary Effect |
This term specifies which leg - if any- becomes the active subcontract when the underlying asset’s price crosses the specified boundary value in the specified direction triggerring a boundary crossing event. |
|
|
Boundary Leg Initially Active |
Specifies which leg - if any - is the active contract in effect when the boundary controlled switch contract starts. |
|
|
Boundary Monitoring Anchor Date |
The first Boundary monitoring event occurs on this date |
|
|
Boundary Monitoring Cycle |
The frequency with which boundary monitoring events occur. It defines how often the system checks to test whether the market value of the underlying asset has crossed the boundary in the specified direction triggerring a boundary crossing event. |
|
|
Boundary Monitoring End Date |
Boundary monitoring ends on this date |
|
|
Boundary Value |
Boundary value in a barrier options contract, when reached, triggers the boundary effect specified e.g. Knock-In or Knock-out |
|
|
Contract Deal Date |
This date signifies the origination of the contract where an agreement between the customer and the bank has been settled. From this date on, the institution will have a (market) risk position for financial contracts. This is even the case when IED is in future. |
|
|
Coverage Of Credit Enhancement |
Defines which percentage of the exposure is covered |
|
|
Guaranteed Exposure |
Defines which value of the exposure is covered: - NO: Nominal Value - NI: Nominal plus Interest - MV: Market Value |
|
|
Credit Event Type Covered |
The type of credit events covered e.g. in credit enhancement or credit default swap contracts. Only the defined credit event types may trigger the protection. |
|
|
Contract Identifier |
Unique identifier of a contract. If the system is used on a single firm level, an internal unique ID can be generated. If used on a national or globally level, a globally unique ID is required. |
|
|
Credit Line Amount |
If defined, gives the total amount that can be drawn from a credit line. The remaining amount that can still be drawn is given by CLA-NT. For ANN, NAM, the credit line can only be drawn prior to PRANX-1PRCL. For CRL, the remaining amount that can still be drawn is given by CLA-Sum(NT of attached contracts). |
|
|
Calendar |
Calendar defines the non-working days which affect the dates of contract events (CDE’s) in combination with EOMC and BDC. Custom calendars can be added as additional enum options. |
|
|
Contract Role |
CNTRL defines which position the CRID ( the creator of the contract record ) takes in a contract. For example, whether the contract is an asset or liability, a long or short position for the CRID. Most contracts are simple on or off balance sheet positions which are assets, liabilities. Such contracts can also play a secondary role as a collateral. The attribute is highly significant since it determines the direction of all cash flows. The exact meaning is given with each CT in the ACTUS High Level Specification document. |
|
|
Counterparty Identifier |
CPID identifies the counterparty to the CRID in this contract. CPID is ideally the official LEI which can be a firm, a government body, even a single person etc. However, this can also refer to a annonymous group in which case this information is not to be disclosed. CPID may also refer to a group taking a joint risk or more generally, CPID is the main counterparty, against which the contract has been settled. |
|
|
Creator Identifier |
This identifies the legal entity creating the contract record. The counterparty of the contract is tracked in CPID. CRID is ideally the official LEI which can be a firm, a government body, even a single person etc. However, this can also refer to a annonymous group in which case this information is not to be disclosed. CRID may also refer to a group taking a joint risk. |
|
|
Contract Type |
The ContractType is the most important information. It defines the cash flow generating pattern of a contract. The ContractType information in combination with a given state of the risk factors will produce a deterministic sequence of cash flows which are the basis of any financial analysis. |
|
|
Contract Structure |
A structure identifying individual or sets of underlying contracts. E.g. for FUTUR, this structure identifies the single underlying contract, for SWAPS, the FirstLeg and SecondLeg are identified, or for CEG, CEC the structure identifies Covered and Covering contracts. |
|
|
Currency |
The currency of the cash flows. |
|
|
Currency 2 |
The currency of the cash flows of the second leg (if not defined, main currency applies) |
|
|
Settlement Currency |
The currency in which cash flows are settled. This currency can be different from the currency (CUR) in which cash flows or the contract, respectively, is denominated in which case the respective FX-rate applies at settlement time. If no settlement currency is defined the cash flows are settled in the currency in which they are denominated. |
|
|
Delinquency Period |
If real payment happens after scheduled payment date plus DLP, then the counterparty is in technical default. This means that the creditor legally has the right to declare default of the debtor. |
|
|
Delinquency Rate |
Rate at which Delinquency Payments accrue on NT (in addition to the interest rate) during the DelinquencyPeriod |
|
|
Delivery Settlement |
Indicates whether the contract is settled in cash or physical delivery. In case of physical delivery, the underlying contract and associated (future) cash flows are effectively exchanged. In case of cash settlement, the current market value of the underlying contract determines the cash flow exchanged. |
|
|
Cycle Anchor Date Of Dividend |
Date from which the dividend payment date schedule is calculated according to the cycle length. The first dividend payment event takes place on this anchor. |
|
|
Cycle Of Dividend |
Defines in combination with DVANX the payment points of dividends. The dividend payment schedule will start at DVANX and end at MaximumProjectionPeriod (cf. sheet Modeling Parameters). |
|
|
Ex Dividend Date |
In case contract is traded between DVEX and next DV payment date (i.e. PRD>DVEX & PRD<next DV payment date), then the old holder of the contract (previous to the trade) receives the next DV payment. In other words, the next DV payment is cancelled for the new (after the trade) holder of the contract. |
|
|
Next Dividend Payment Amount |
Defines the next dividend payment (amount) whereas the date of dividend payment is defined through the DVANX/DVCL pair. If DVCL is defined, then this amount will be used as dividend payment for each future dividend payment date. |
|
|
End Of Month Convention |
When computing schedules a special problem arises if an anchor date is at the end of a month and a cycle of monthly or quarterly is applied (yearly in the case of leap years only). How do we have to interpret an anchor date April 30 plus 1M cycles? In case where EOM is selected, it will jump to the 31st of May, then June 30, July 31 and so on. If SM is selected, it will jump to the 30st always with of course an exception in February. This logic applies for all months having 30 or less days and an anchor date at the last day. Month with 31 days will at any rate jump to the last of the month if anchor date is on the last day. |
|
|
Fee Accrued |
Accrued fees as per SD |
|
|
Cycle Anchor Date Of Fee |
Date from which the fee payment date schedule is calculated according to the cycle length. The first fee payment event takes place on this anchor. |
|
|
Fee Basis |
Basis, on which Fee is calculated. For FEB=’A’, FER is interpreted as an absolute amount to be paid at every FP event and for FEB=’N’, FER represents a rate at which FP amounts accrue on the basis of the contract’s NT. |
|
|
Cycle Of Fee |
Defines in combination with FEANX the payment points of fees |
|
|
Fee Rate |
Rate of Fee which is a percentage of the underlying or FER is an absolute amount. For all contracts where FEB does not apply (cf. business rules), FER is interpreted as an absolute amount. |
|
|
Grace Period |
If real payment happens after scheduled payment date plus GRP, then the payment is in delay. |
|
|
Initial Exchange Date |
Date of the initial cash flow for Maturity and Non-Maturity CT’s. It also coincides with the beginning of interest accrual calculation. |
|
|
Accrued Interest |
Accrued interest as per SD. In case of NULL, this value will be recalculated using IPANX, IPCL and IPNR information. Can be used to represent irregular next IP payments. |
|
|
Cycle Anchor Date Of Interest Payment |
Date from which the interest payment date schedule is calculated according to the cycle length. The first interest payment event takes place on this anchor. |
|
|
Interest Calculation Base |
This is important for amortizing instruments. The basis of interest calculation is normally the notional outstanding amount as per SD. This is considered the fair basis and in many countries the only legal basis. If NULL or NTSD is selected, this is the case. Alternative bases (normally in order to favor the lending institution) are found. In the extreme case the original balance (PCDD=NT+PDCDD) never gets adjusted. In this case PCDD must be chosen. An intermediate case exist wherre balances do get adjusted, however with lags. In this case NTL mut be selected and anchor dates and cycles must be set. |
|
|
Interest Calculation Base Amount |
This is the amount used for the calculation of interest. Calculation base per SD. |
|
|
Cycle Anchor Date Of Interest Calculation Base |
Date from which the interest calculation base date schedule is calculated according to the cycle length. The first interest calculation base event takes place on this anchor. |
|
|
Cycle Of Interest Calculation Base |
Concerning the format see PRCL. Defines the subsequent adjustment points to NT of the interest payment calculation base. |
|
|
Capitalization End Date |
If IPCED is set, then interest is not paid or received but added to the balance (NT) until IPCED. If IPCED does not coincide with an IP cycle, one additional interest payment gets calculated at IPCED and capitalized. Thereafter normal interest payments occur. |
|
|
Cycle Of Interest Payment |
Cycle according to which the interest payment date schedule will be calculated. In case IPCL is not set, then there will only be an interest payment event at MD (and possibly at IPANX if set). The interval will be adjusted yet by EOMC and BDC. |
|
|
Day Count Convention |
Method defining how days are counted between two dates. This finally defines the year fraction in accrual calculations. |
|
|
Nominal Interest Rate |
The nominal interest rate which will be used to calculate accruals and the next interest payment at the next IP date. NT multiplied with IPNR is the base for the interest payment calculation. The relevant time period is a function of IPDC. If the contract is variable (RRANX set) this field is periodically updated per SD. In the case of plan vanilla interest rate swaps (IRSPV) this defines the rate of fixed leg. |
|
|
Nominal Interest Rate 2 |
The nominal interest rate which will be used to calculate accruals and the next interest payment at the next IP date on the second leg (the one not mentioned in CNTRL) of a plain vanilla swap. The relevant time period is a function of IPDC. It is periodically updated per SD. |
|
|
Cycle Point Of Interest Payment |
Usually, interest is paid at the end of each IPCL which corresponds to a IPPNT value of E which is also the default. If interest payment occurs at the beginning of the cycle, the value is B. |
|
|
Maturity Date |
Marks the contractual end of the lifecycle of a CT. Generally, date of the last cash flows. This includes normally a principal and an interest payment. Some Maturity CTs as perpetuals (PBN) do not have such a date. For variable amortizing contracts of the ANN CT, this date might be less than the scheduled end of the contract (which is deduced from the periodic payment amount PRNXT). In this case it balloons. |
|
|
Market Object Code |
Is pointing to the market value at SD (MarketObject). Unique codes for market objects must be used. |
|
|
Maximum Penalty Free Disbursement |
Defines the notional amount which can be withdrawn before XDN without penalty |
|
|
Cycle Anchor Date Of Margining |
Date from which the margin call date schedule is calculated according to the cycle length. The first margin call event takes place on this anchor. |
|
|
Cycle Of Margining |
Defines together with MRANX the points where margins can be called. |
|
|
Clearing House |
Indicates wheter CRID takes a clearing house function or not. In other word, whether CRID receive margins (MRIM, MRVM). |
|
|
Initial Margin |
Margin to cover losses which may be incurred as a result of market fluctuations. Upon contract closing or maturity, the MRIM is reimbursed. |
|
|
Maintenance Margin Lower Bound |
Defines the lower bound of the Maintenance Margin. If MRVM falls below MRMML, then capital must be added to reach the original MRIM. |
|
|
Maintenance Margin Upper Bound |
Defines the upper bound of the Maintenance Margin. If MRVM falls above MRMMU, then capital is refunded to reach the original MRIM. |
|
|
Variation Margin |
MRVM reflects the accrued but not yet paid margin as per SD. Open traded positions are revalued by the exchange at the end of every trading day using mark-to-market valuation. Often clearing members do not credit or debit their clients daily with MRVM, but rather use a Maintenance Margin. If the balance falls outside MRMML (and MRMMU), then capital must be added (is refunded) to reach the original margin amount MRIM. We can also say that MVO+MRVM is equal to the reference value as per last margin update. |
|
|
Market Value Observed |
Value as observed in the market at SD per unit. Incase of fixed income instruments it is a fraction. |
|
|
Non Performing Date |
The date of the (uncovered) payment event responsible for the current value of the Contract Performance attribute. |
|
|
Notional Principal |
Current nominal value of the contract. For debt instrument this is the current remaining notional outstanding. NT is generally the basis on which interest payments are calculated. If IPCBS is set, IPCBS may introduce a different basis for interest payment calculation. |
|
|
Notional Principal 2 |
Notional amount of the second currency to be exchanged in an FXOUT CT. |
|
|
Cycle Anchor Date Of Optionality |
Used for Basic Maturities (such as PAM, RGM, ANN, NGM and their Step-up versions) and American and Bermudan style options. - Basic Maturities: Within the group of these Maturities, it indicates the possibility of prepayments. Prepayment features are controlled by Behavior. - American and Bermudan style Options: Begin of exercise period. |
|
|
Cycle Of Optionality |
Cycle according to which the option exercise date schedule will be calculated. OPCL can be NULL for American Options or Prepayment Optionality in which case the optionality period starts at OPANX and ends at OPXED (for american options) or MD (in case of prepayment optionality). The interval will be adjusted yet by EOMC and BDC. |
|
|
Option Strike 1 |
Strike price of the option. Whether it is a call/put is determined by the attribute OPTP, i.e a call or a put (or a combination of call/put). This attribute is used for price related options such as options on bonds, stocks or FX. Interest rate related options (caps/floos) are handled within th RatReset group. |
|
|
Option Type |
Defines whether the option is a call or put or a combination of it. This field has to be seen in combination with CNTRL where it is defined whether CRID is the buyer or the seller. |
|
|
Option Exercise End Date |
Final exercise date for American and Bermudan options, expiry date for European options. |
|
|
Option Exercise Type |
Defines whether the option is European (exercised at a specific date), American (exercised during a span of time) or Bermudan (exercised at certain points during a span of time). |
|
|
Premium Discount At IED |
Total original premium or discount that has been set at CDD and will be added to the (notional) cash flow at IED (cash flow at IED = NT+PDIED, w.r.t. an RPA CT). Negative value for discount and positive for premium. Note, similar to interest the PDIED portion is part of P&L. |
|
|
Futures Price |
The price the counterparties agreed upon at which the underlying contract (of a FUTUR) is exchanged/settled at STD. Quoting is different for different types of underlyings: Fixed Income = in percentage, all others in nominal terms. |
|
|
Prepayment Effect |
This attribute defines whether or not the right of prepayment exists and if yes, how prepayment affects the remaining principal redemption schedule of the contract |
|
|
Prepayment Period |
If real payment happens before scheduled payment date minus PPP, then it is considered a prepayment. Effect of prepayments are further described in PPEF and related fields. |
|
|
Price At Purchase Date |
Purchase price exchanged at PRD. PPRD represents a clean price (includes premium/discount but not IPAC). |
|
|
Cycle Anchor Date Of Principal Redemption |
Date from which the principal payment date schedule is calculated according to the cycle length. The first principal payment event takes place on this anchor. |
|
|
Cycle Of Principal Redemption |
Cycle according to which the interest payment date schedule will be calculated. In case PRCL is not set, then there will only be one principal payment event at MD (and possibly at PRANX if set). The interval will be adjusted yet by EOMC and BDC. |
|
|
Purchase Date |
If a contract is bought after initiation (for example a bond on the secondary market) this date has to be set. It refers to the date at which the payment (of PPRD) and transfer of the security happens. In other words, PRD - if set - takes the role otherwise IED has from a cash flow perspective. Note, CPID of the CT is not the counterparty of the transaction! |
|
|
Contract Performance |
Indicates the current contract performance status. Different states of the contract range from performing to default. |
|
|
Next Principal Redemption Payment |
Amount of principal that will be paid during the redemption cycle at the next payment date. For amortizing contracts like ANN, NAM, ANX, and NAX this is the total periodic payment amount (sum of interest and principal). |
|
|
Price At Termination Date |
Sellingprice exchanged at PTD PTDrepresents a clean price (includes premium/discount but not IPAC |
|
|
Penalty Rate |
Either the rate or the absolute amount of the prepayment. |
|
|
Penalty Type |
Defines whether prepayment is linked to a penalty and of which kind. |
|
|
Quantity |
This attribute relates either to physical contracts (COM) or underlyings of traded contracts. In case of physical contracts it holds the number of underlying units of the specific good (e.g. number of barrels of oil). In case of well defined traded contracts it holds the number of defined underlying instruments. Example: QT of STK CTs underlying a FUTUR indicates the number of those specific STK CTs which underlie the FUTUR. |
|
|
Cycle Anchor Date Of Rate Reset |
Date from which the rate reset date schedule is calculated according to the cycle length. The first rate reset event takes place on this anchor. |
|
|
Cycle Of Rate Reset |
Cycle according to which the rate reset date schedule will be calculated. In case RRCL is not set, then there will only be one rate reset event at RRANX given RRANX if set. The interval will be adjusted yet by EOMC and BDC. |
|
|
Fixing Period |
Interest rate resets (adjustments) are usually fixed one or two days (usually Business Days) before the new rate applies (defined by the rate reset schedule). This field holds the period between fixing and application of a rate. |
|
|
Life Cap |
For variable rate basic CTs this represents a cap on the interest rate that applies during the entire lifetime of the contract. For CAPFL CTs this represents the cap strike rate. |
|
|
Life Floor |
For variable rate basic CTs this represents a floor on the interest rate that applies during the entire lifetime of the contract. For CAPFL CTs this represents the floor strike rate. |
|
|
Rate Multiplier |
Interest rate multiplier. A typical rate resetting rule is LIBOR plus x basis point where x represents the interest rate spread. However, in some cases like reverse or super floater contracts an additional rate multiplier applies. In this case, the new rate is determined as: IPNR after rate reset = Rate selected from the market object * RRMLT + RRSP. |
|
|
Market Object Code Of Rate Reset |
Is pointing to the interest rate driver (MarketObject) used for rate reset uniquely. Unique codes for market objects must be used. |
|
|
Next Reset Rate |
Holds the new rate that has been fixed already (cf. attribute FixingDays) but not applied. This new rate will be applied at the next rate reset event (after SD and according to the rate reset schedule). Attention, RRNXT must be set to NULL after it is applied! |
|
|
Period Cap |
For variable rate basic CTs this represents the maximum positive rate change per rate reset cycle. |
|
|
Period Floor |
For variable rate basic CTs this represents the maximum negative rate change per rate reset cycle. |
|
|
Cycle Point Of Rate Reset |
Normally rates get reset at the beginning of any resetting cycles. There are contracts where the rate is not set at the beginning but at the end of the cycle and then applied to the previous cycle (post-fixing); in other words the rate applies before it is fixed. Hence, the new rate is not known during the entire cycle where it applies. Therefore, the rate will be applied backwards at the end of the cycle. This happens through a correction of interest accrued. |
|
|
Rate Spread |
Interest rate spread. A typical rate resetting rule is LIBOR plus x basis point where x represents the interest rate spread. The following equation can be taken if RRMLT is not set: IPNR after rate reset = Rate selected from the market object + RRSP. |
|
|
Cycle Anchor Date Of Scaling Index |
Date from which the scaling date schedule is calculated according to the cycle length. The first scaling event takes place on this anchor. |
|
|
Scaling Index At Contract Deal Date |
The value of the Scaling Index as per Contract Deal Date. |
|
|
Cycle Of Scaling Index |
Cycle according to which the scaling date schedule will be calculated. In case SCCL is not set, then there will only be one scaling event at SCANX given SCANX is set. The interval will be adjusted yet by EOMC and BDC. |
|
|
Scaling Effect |
Indicates which payments are scaled. I = Interest payments, N = Nominal payments and M = Maximum deferred interest amount. They can be scaled in any combination. |
|
|
Interest Scaling Multiplier |
The multiplier being applied to interest cash flows |
|
|
Market Object Code Of Scaling Index |
||
|
Notional Scaling Multiplier |
The multiplier being applied to principal cash flows |
|
|
Status Date |
SD holds the date per which all attributes of the record were updated. This is especially important for the highly dynamic attributes like Accruals, Notional, interest rates in variable instruments etc. |
|
|
Seniority |
Refers to the order of repayment in the event of a sale or default of the issuer. |
|
|
Settlement Period |
Defines the period from fixing of a contingent event/obligation (Exercise Date) to settlement of the obligation. |
|
|
Termination Date |
If a contract is sold before MD (for example a bond on the secondary market) this date has to be set. It refers to the date at which the payment (of PTD) and transfer of the security happens. In other words, TD - if set - takes the role otherwise MD has from a cash flow perspective. Note, CPID of the CT is not the counterparty of the transaction! |
|
|
Unit |
The physical unit of the contract. Example: Barrels for an Oil COM CT. |
|
|
Exercise Amount |
The amount fixed at Exercise Date for a contingent event/obligation such as a forward condition, optionality etc. The Exercise Amount is fixed at Exercise Date but not settled yet. |
|
|
Exercise Date |
Date of exercising a contingent event/obligation such as a forward condition, optionality etc. The Exercise date marks the observed timestamp of fixing the contingent event and respective payment obligation not necessarily the timestamp of settling the obligation. |
|
|
X Day Notice |
Used as rolling attribute with the callable CT’s UMP and CLM uniquely. CLM’s and UMP’s will not be settled (MD not set) until the client uses his option to call the contract X_Day_Notice after Current Date. As long as MD or TD is not set, the client postpones his right to call to the future. The cycle is normally defined in number of business days. |
|
|
Option Strike 2 |
Put price in case of call/put. |
7.2 State Variables
|
Acronym |
Name |
Description |
|
Boundary Crossed Flag |
TRUE value indicates that a boundary crossing event has already occurred; boundary monitoring is no longer in effect. |
|
|
Boundary Leg1 Active Flag |
TRUE value indicates that boundaryLeg1 is currently active and generating cashflow events. |
|
|
Boundary Leg2 Active Flag |
TRUE value indicates that boundaryLeg2 is currently active and generating cashflow events. |
|
|
Fee Accrued |
The current value of accrued fees |
|
|
Interest Calculation Base Amount |
The basis at which interest is being accrued. Potentially different from NVL. |
|
|
Accrued Interest |
The current value of accrued interest |
|
|
Accrued Interest 2 |
The current value of accrued interest of the second leg |
|
|
Nominal Interest Rate |
The applicable nominal rate |
|
|
Nominal Interest Rate 2 |
The applicable nominal rate |
|
|
Maturity Date |
The timestamp as per which the contract matures according to the initial terms or as per unscheduled events |
|
|
Non Performing Date |
The date of the (uncovered) payment event responsible for the current value of the Contract Performance state variable. |
|
|
Notional Principal |
The outstanding nominal value |
|
|
Notional Principal 2 |
The outstanding nominal value of the second leg |
|
|
Contract Performance |
Indicates the current Contract Performance status. Different states of the contract range from performing to default. |
|
|
Next Principal Redemption Payment |
The value at which principal is being repaid. This may be including or excluding of interest depending on the Contract Type |
|
|
Interest Scaling Multiplier |
The multiplier being applied to interest cash flows |
|
|
Notional Scaling Multiplier |
The multiplier being applied to principal cash flows |
|
|
Status Date |
The timestamp as per which the state is captured at any point in time |
|
|
Termination Date |
The timestamp of unscheduled termination of a contract |
|
|
Exercise Amount |
The amount fixed for a the contingent event/obligation exercised at Exercise Date |
|
|
Exercise Date |
The timestamp at which a contingent event/obligation is exercised |
7.3 Contract Types
|
Acronym |
Name |
Description |
|
Annuity |
Principal payment fully at IED and interest plus principal repaid periodically in constant amounts till MD. If variable rate, total amount for interest and principal is recalculated to be fully matured at MD. |
|
|
Exotic Annuity |
Exotic version of ANN However step ups with respect to (i) Principal, (ii) Interest rates are possible. Highly flexible to match totally irregular principal payments. Principal can also be paid out in steps. |
|
|
Boundary Controlled Switch |
A boundary controlled switch is a derivative contract with subcontract legs which can be activated (knocked in) or extinguished (knocked out) when the underlying asset price reaches a specified value. The underlying asset may be a stock, index, or exchange-traded fund. Boundary controlled switch contracts with a single boundary are currently defined. |
|
|
Convertible Note |
Bonds with a call or put option. If option is exercised, underlying bond ceases to exist. |
|
|
Warrant |
Bonds with a warrant. If option is exercised, underlying bond continues to exist. |
|
|
Cap Floors |
Interest rate option expressed in a maximum or minimum interest rate. |
|
|
Credit Default Swap |
A payment is triggered if one or more of the ndelying counterparties defaults. |
|
|
Collateral |
Collateral creates a relationship between a collateral an obligee and a debtor, covering the exposure from the debtor with the collateral. |
|
|
Guarantee |
Guarantee creates a relationship between a guarantor, an obligee and a debtor, moving the exposure from the debtor to the guarantor. |
|
|
Call Money |
Loans that are rolled over as long as they are not called. Once called it has to be paid back after the stipulated notice period. |
|
|
Credit Linked Note |
A credit linked note is a security with an embedded CDSWP |
|
|
Commodity |
This is not a financial contract in its propper sense. However it traks movements of commodities such as oil, gas or even houses. Such commodities can serve as underlyings of commodity futures, guarantees or simply asset positions. |
|
|
Cash |
Cash or cash equivalent position |
|
|
EXOTi |
As of current, most of the exotic options which were popular before 2008 are out of favor and factually irrelevant.Which of the exotic options will be implemented will depend on the real relevance in the future. |
|
|
Future |
Keeps track of value changes for any basic CT as underlying (PAM, ANN etc. but also FXOUT, STK, COM). Handles margining calls. |
|
|
Foreign Ex-change Outright |
Two parties agree to exchange two fixed cash flows in different currencies at a certain point in time in future. |
|
|
Linear Amortizer |
Principal payment fully at IED. Principal repaid periodically in constant amounts till MD. Interest gets reduced accordingly. If variable rate, only interest payment is recalculated. Fixed and variable rates. |
|
|
Exotic Linear Amortizer |
Exotic version of LAM. However step ups with respect to (i) Principal, (ii) Interest rates are possible. Highly flexible to match totally irregular principal payments. Principal can also be paid out in steps. |
|
|
Margining |
A Margining contract traces the value changes and the different margin categories like inital and variation margin. |
|
|
Negative Amortizer |
Similar as ANN. However when resetting rate, total amount (interest plus principal) stay constant. MD shifts. Only variable rates. |
|
|
Exotic Negative Amortizer |
Exotic version of NAM However step ups with respect to (i) Principal, (ii) Interest rates are possible. Highly flexible to match totally irregular principal payments. Principal can also be paid out in steps. |
|
|
Option |
Calculates straight option pay-off for any basic CT as underlying (PAM, ANN etc.) but also SWAPS, FXOUT, STK and COM. Single, periodic and continuous strike is supported. |
|
|
Principal at Maturity |
Principal payment fully at Initial Exchange Date (IED) and repaid at Maturity Date (MD). Fixed and variable rates. |
|
|
Perpetual Bonds |
Bonds without any maturity date. Interest is paid into eternity if is not terminated. |
|
|
Repurchase Agreement |
A Repo contract controls and manages the sale and repurchase of assets on the books. |
|
|
Securitization Credit Risk |
Securitiazion contracts where contracs are ranked according to credit default. The lower ranked tranches are hit by the first defaults. Only when the lowest tranches are wiped out, the next higher tranch is hit. |
|
|
Securitization Market Risk |
Securitiazion contracts where all underlying contracts are treated equal. The buyer of a tranche gets a part of the cash-flows. |
|
|
Stock |
Any instrument which is bought at a certain amount (market price normally) and then follows an index. |
|
|
Swap |
Exchange of two basic CT´s (PAM, ANN etc.). Normally one is fixed, the other variable. However all variants possible including different currencies for cross currency swaps, basic swaps or even different principal exchange programs. |
|
|
Plain Vanilla Swap |
Plain vanilla swaps where the underlyings are always two identical PAM´s however with one leg fixed and the other variable. |
|
|
Total Return Swap |
A total return swap is a swap agreement in which one party makes payments based on a set rate, either fixed or variable, while the other party makes payments based on the return of an underlying asset, which includes both the income it generates and any capital gains. |
|
|
Undefined Maturity Profile |
Principal paid in and out at any point in time without prefixed schedule. Interest calculated on outstanding and capitalized periodically. Needs link to a behavioral function describing expected flows. |