notes.txt

Some thoughts
-------------

type mngt_contract =
      {start: date,
       initial: contract,
       date: date,
       current: contract,
       events: event list}    //   (start, initial)   ---events---> (date, current)

datatype event =  Fixing of date * string * value | NewContract of date * Contract.contract | Default of date * string

datatype portfolio = {start   : date,
                      initial : contract,
                      events: event list,
                      current_date: date,
                      current : contract}

===================

Semantics of translating a contract: should affect embedded expressions/observables!

i = If (condition(day) , contract1, contract2)
Transl (I 30 , i ) =!= If (condition ( day + 30 ) , 
                           Transl (I 30, contract1), 
                           Transl (I 30, contract2)

-------------
Preconditions: causality of components

consistent (a : contract) : bool
   (no flow in the present depends on future value of any observable,
    and this is maintained through translated contracts)

This implies the following side conditions:
o Obs of String * int: int should be non-positive
                       if a positive int occurs, an _outer_ Transl must be introduced 
                       to eliminate it*).
o Transl of intE * contract: intE should _evaluate_ _to_ non-negative number

Transl nodes should be pushed to the outside in normalisation
(direction "<=" in the example above). If this yields negative Transl
on the inside, the contract is not consistent.
Question here is, how to check this, as Transl uses intE, not int.

=====================

Ideas how to use this library in the future:

fun normalise (a : contract) = beautiful contract
fun isBarrier (a : contract) = ...pattern match..
fun defocus ( a : contract, days : int ) = contract aggregating "day windows"
    should be called "decreaseLevelOfDetail", or something else?

makes possible to do: 
  testB  a = isBarrier (normalise (defocus ( a , 1week)))

-------------

"beautiful contract" (normal form): established by a special routine.
Should gather constructors in one place, essentially on one
side of If and CheckWithin constructs: Transl should be pushed to the
outside, Scale should be pushed in. All should be inside, but above 
Scale (to see empty leaves?)
In addition, should apply simplifications once constructors are
adjacent: multiply Scales, add Transl, cut them when empty below

======================

simpler uses, immediately possible:

removeParty (p : string, a : contract) = contract without anything involving party p
mergeParties (p1, p2 : string, a : contract) = contract with party p2 identified with p1

more real-world functionality:

defaultParty (party : string, 
             t : time (expected litigation duration), 
             perc : real (percentage), a : contract) = 
      contract a, with all payments received from this party scaled to
      perc % and translated by time t forward, and all payments to this
      party removed.

=======================

How to model (non-rational) choice?

Should be part of the Expr language (chosenBy party : boolE) and 
use the If constructor.

Or else, Choice(p, c1, c2) as a contract constructor?

chosenBy : Party+Label -> boolE

together with If, models non-rational choice.

Semantic implications: none.

Problem of causality: decision needs to be made before implications

chosenBy : Party+Label -> Time -> boolE
                           int
Time denoting relative time when the decision must have been taken
(i.e. must be available in the environment).

Semantically can be seen as a value changing from _|_ to a constant.
Assuming translate operations are all outside of the scoped contracts
which uses a chosenBy, the time should always be non-positive.

Also adding an if in the expression language?

E [[ b: boolE "?" e1:expr a ":" e2:expr a ]] e = if E[[b]]e then E[[e1]]e else E[[e2]]e

This enables choosing values that are not boolean (sizes, prices, ...)
(could also be modeled by "multiplexing" the contracts that use it, though)


=======================

How the contract language differs from the LexiFi contract language

 - Dates are first class, meaning that a residual contract can be
   translated in time a dynamic amount (e.g., based on an
   underlying). American optionality and knock-outs are therefore
   easily expressible, without discretization; we may need a few more
   operators, such as anytime, however.

 - Contracts are truly relative to the present, which is contrary to
   how the LexiFi system works. In the LexiFi system, observables are
   defined separately and are not translated in time by the 'when'
   operator; see "The Fun of Programming" paper, page 114, for
   instance. Also, the paper does not mention whether there is a
   "delay" operator that allows for a contract to refer to a past
   value of an underlying.

 - Concrete contracts are paired with an associated date under which
   the contract should be understood. Using this date, cash flows with
   concrete dates can be computed. The notion of advancing a contract
   is important. Say we have a concrete contract (d,c), that is a
   contract c that should be understood relative to the date d. We
   have (d,c) -adv(1)-> (d+1,c'), where c' is c advanced by one
   day. First notice that expressions in the contract language are
   arithmetic and boolean expressions that may reference underlying
   observable quantities at particular dates, relative to
   now. Formally, we first define the notion of expression time
   adjustment:

   Expression Time Adjustment
    (s,d)/d' = (s,d+d')
    e/d' = e with all underlying references (s,d) in e replaced by (s,d+d')

   Notice that time adjustment e/d is defined only when d is known to
   be a particular integer.

   An expression's value is certain if it does not contain observables.
   In this case, we call the expression "certain" (i.e. if its _value_ is certain)

   Here are some equivalences that hold:

    transl(d1,transl(d2,c)     ==   transl(d1+d2,c)
    transl(d,scale(s,c))       ==   scale(s,transl(d,c))           s certain
    transl(d,scale(s,c))       ==   scale(s/d,transl(d,c))
    scale(s1,scale(s2,c))      ==   scale(s1*s2,c)
    iff(T,c1,c2)               ==   c1
    iff(F,c1,c2)               ==   c2
    transl(d,all cs)           ==   all (map (\c.transl(d,c)) cs)
    transl(d,iff(cond,c1,c2))  ==   iff(cond/d, transl(d,c1), transl(d,c2))
    transl(d,checkWithin (cond, e, c1, c2))  ==  
                             checkWithin (cond/d, e, transl(d,c1), transl(d,c2))
    iff(c,zero,zero)           ==   zero
    transl(d,zero)             ==   zero
    scale(r,zero)              ==   zero
    Both (zero,zero)           ==   zero
    scale(0,c)                 ==   zero
    all cs                     ==   zero if c == zero forall c in cs

   Advancing a contract (throwing away due transfers) can now be
   defined, formally (and partially), as follows:

    fun adv 0 c = c
      | adv n c =         (* notice: n >= 0 *)
        case c of
           scale(s,c) => scale(s/-n, adv n c)
         | transl(d,c) => 
              if certain d then
                  let n' = min n d
                  in transl(d-n', adv (n-n') c)
                  end
              else error "contract advancement not possible"
         | transl(d,c) => 
         | iff(cond,c1,c2) => iff(cond/-n,adv n c1,adv n c2)
         | all cs => all (map (adv n) cs)
         | transfOne(c,p1,p2) => emp
 
   It is not clear whether we can always write up a contract in a
   canonical form that will help us determine whether two contracts
   are bisimilar.

 - A causal contract is, by definition, a contract with the property that during all
   possible executions of the contract, a transfer cannot depend on a
   future fixing.

   Example of a non-causal contract:

      iff(("CarlsbergDKR",2) > 50.0, transfOne(EUR,me,you), emp)

         - Meaning: if the Carlsberg stock is worth more than kr 50 in
           two days, I should transfer one EUR to you today.

In general, causality is now a dynamic property that for some
contracts needs to be checked at runtime (during contract
management). For many contracts, however, the property of causality
can be established statically. We now define a conservative causality
check. Given a non-negative integer b, an expression e is b-causal
(written b |- e), if for all obs(s,i) in e, we have i <= b (and there
is no smaller such b):

     e is a literal
   ----------------- (Lit)      (b non-negative because we use 0 here)
        0 |- e
    
   ------------------------ (Obs)
      max b 0 |- obs(s,b)


       b1 |- e1  b2 |- e2
   -------------------------- (BinOp)
      max b1 b2 |- e1 o e1


       b |- e
   ------------- (UnOp)
      b |- o e

Given b a non-negative integer or inf, b-causality of a contract c
(written b |- c) is defined as follows:
 
                                                           +--------+
Conservative contract causality                            | b |- c |
                                                           +--------+

(Intuitively, b |- c means that c is causal and there are no transfers
before d days have passed.)

                b |- c 
       ---------------------------- (TL)
           b + d |- transl(d,c)


       --------------- (Zero)
        inf |- zero

       ------------------------- (TO)
        0 |- transfOne(C,p1,p2)

        b1 |- e  b2 |- c  b1 <= b2
      ----------------------------- (Sc)
             b2 |- scale(e,c)

         0 |- e  b1 |- c1  b1 |- c2
       ----------------------------- (If)
         min b1 b2 |- iff(e,c1,c2)

              b1 |- c1  b2 |- c2
        ----------------------------- (Both)
           min b1 b2 |- both(c1,c2) 

                 0 |- e  b1 |- c1   b2 |- c1
       ----------------------------------------------- (CW)
        min b1 (d + b2) |- checkWithin (e, d, c1, c2)

(This follows from an algebraic law which "unrolls" the check:
   checkWithin (b, d, c1, c2) == 
               let r i = if i == d then transl(d,c2)
                                   else iff (b/i, transl(i,c1), r (i+1))
               in r 0

   checkWithin (b, d, c1, c2) ==
               iff (b, c1, transl(1, checkWithin(b, d-1, c1, c2)))
   checkWithin (b, 0, c1, c2) == iff(b,c1,c2)

    (*** note: b is assumed only to contain relative observables ***)
 
This recursion could be written as a fixed point...
c1 is translated with i < d during unrolling. 
b is causal at present, but not necessarily in the future.)

Proposition (Conservative Causality Soundness).
If d |- c (for some d) then c is causal. 


Corollary.
If for all observables obs(s,i) in c, we have that i <= 0, then c is
causal.


=======================

Design question:

 Should transl affect the date on which an underlying is referenced?

 - The answer to this question is yes! Otherwise, we would lack good
   compositionality properties.


h([],a) = a
h(c::cs,a)  = h(cs, c + a * 19)

val hashExp:  expr0 -> IntInf.int
val hashContr : contr -> IntInf.int

H(p,a)                     = p * (a + 1)
h(Zero, a)                 = H(2,a)
h(Both(c1,c2), a)          = h(c1,0) + h(c2,0) + a
h(TransfOne(cur,p1,p2), a) = h(cur,h(p1,h(p2,H(3,a)))
h(Iff(e,c1,c2),a)          = h(c1,h(c2,h(e,H(5,a))))
h(Scale(e,c),a)            = h(e,h(c,H(7,a)))
h(Transl(e,c),a)           = h(e,h(c,H(11,a)))

==============================================

Argument against using intE for Transl constructor:

On day 0 observe Carlsberg to define when to receive 
a flow scaling with the IBM stock price (on _that_ day, BAD)

Transl ( obs ("Carlsberg",0) , Scale (obs ("IBM",0),flow(...)))

Desired: 
On day 0 observe Carlsberg to define when to receive 
a flow scaling with the IBM stock price on _1st_ of _January_.

Solution:
 Choose d from today such that addDays today d = Jan 1 2014
Scale (obs ("IBM", d), Transl(obs ("Carlsberg",0), flow (...)))
                        
This normalises to a non-causal thing: the observable "IBM" needs
to be translated using an intE, not an int.

==> replace intE by int in Transl constructor, incl. all changes on top.

===========================
===========================

Formal semantics of contracts:


\mathbb{C} :: Contract -> Environment -> 
              Sequence of Set of CashFlows (for all days in the future)

         where CashFlow = (Amount, currency, party_from, party_to)
               ( see flow function in Contract.sml )
               Environment = (int, string) -/-> Real (partial mapping)

equivalent: adding a date to flow, sorting by date, inserting empty dates.
(we have a prettyprinter for that one)

Reminder: exp/d means all offsets in observables in exp forwarded by d (+d)
We transfer this "/" to environments now:

   e / d =  \(i,s) -> e (i+d,s)

E [[ exp ]] e =..

C [[ Zero ]] e = repeat emptySet

C [[ TransfOne (cur, p1, p2) ]] e = (1,cur,p1,p2): repeat emptySet

C [[ Scale (exp, c1) ]]         e = let cs = C [[ c1 ]] e
                                    in mapmap (\(a,c,f,t) -> (a*E[[exp]]e,c,f,t)) cs

C [[ Both (c1,c2) ]]  e = zipWith flowMerge ( C[[c1]]e) (C[[c2]]e)

C [[ Transl (d,c1) ]] e = replicate d emptySet ++ C [[ c1 ]] (e/d) **

C [[ If ( b, c1, c2) ]] e = if (E [[ b ]] e) then C [[ c1 ]] e else C [[ c2 ]] e
                               ------------- might not exist(?)
                       (partial Env. function leads to partial semantics)
C [[ CheckWithin ( b, d, c1, c2) ]] 
  | d == 0 = C [[ If (b, c1, c2) ]] e
  | d > 0  = if (E [[ b ]] e) then C [[ c1 ]] e 
                              else emptySet : C [[ CheckWithin (b,d-1,c1,c2) ]] e/1

**      example: Transl (2 , Scale (obs "carlsberg" -1, TransfOne (dkk, me, you))
               =semantic= Scale (obs "carlsberg" 1, Tranls(2, TransfOne (dkk, me, you)))
           (pay in 2 days the carlsberg stock I give tomorrow)

Defining causality using the semantics:

(above: - A causal contract is, by definition, a contract with the property that during
 all possible executions of the contract, a transfer cannot depend on a future fixing.)

c "causal" :<=> For all d: if two environments e1 e2 coincide up to point d in time,
                           then the semantics of c under e1 and e2 coincides at point d.

(e1 and e2 "coincide" up to d <- Int :<=> e1 (s,x) == e2(s,x) for all x <= d)

(Semantics of contract c under e1 and e2 "coincide" up to d :<=>
       take d ( C[[c]] e1) == take d ( C[[c]]e2 ))

-------------

Advancing a contract by d days = drop d (C [[c]]e)

Removing a party p from a contract = map (setFilter (not (involves p))) (C[[c]]e)
         where involves p (_,_,p',p'') = p == p' || p == p''

merging parties: ... eliminating flows between them

----------

"defocus" of contracts, by time window i:
  union of d consecutive flow sets, merging as appropriate. Start
  (arbitrary) by full time window..

  This leads to a "i-day semantics", where above we defined the "day semantics".

  What about the observables? (min/max/what?)

more advanced: "defocusParty" from a party's perspective:

  avoid "making contracts look better" by defocusing, move payments I
  make to the beginning while the ones I receive go to the end of the
  window.

what does it mean for a contract to "look better" (and for whom)?

===========

A contract c' is a d-defocus of a contract c iff "when fiddling with
 the environment using d" c' yields the same semantics as defocus(d,c)

"fiddling with the env." defines the semantics of defocus more thoroughly.

--------------------

problem "where to draw the line".

Might be useful to use a "sliding average window" of cash flows,
window size d. However, the sum of all sliding averages is maybe not
equal to the sum of all original cashflows between two resp. parties.
(or is it?)

contracts c1 and c2 are d-similar iff their d-defocus (using this
sliding average) is the same.

==================

Potentially useful defocused views on a contract:

o merging all counterparties to one, analysing the result (defocused,merged)
    example: if the merge ends up being just one vanilla option, hedge
             with an opposite option.


=================

Higher-Order Abstract Syntax for Contracts

Example:
  observe("CB", fn cb0 => 
    transl(10, 
      observe("CB", fn cb =>
        iff(cb > cb0,
            scale(cb - cb0, transfOne(DK, "you", "me")),
            zero))))

===================

More contract equivalences:
(basis for new simplification rules for "If" )

if (b, if (b, c11, c12), c2) == if (b, c11, c2)
   ---    --- same b

if (b, c1, if (b, c21, c22)) == if (b, c1, c22)
   ---        --- same b

Both equations follow immediately from semantics of if (evaluate same b).

if (b, CheckWithin(b,i,c11,c12), c2) == if (b, c11, c2)
   ---            --- same b

Follows from CheckWithin semantics: b is known to be true from the start.

NB This needs a normalisation of boolean expressions for full impact
(equivalent expressions are sufficient, also syntactically unequal).
This is easy for booleans (we only have "not" and "|", must identify
branches of "|" in hash, as done for "Both" constructor). In contrast,
it is very cumbersome to implement for arithmetic expressions (needs
to use distribution laws).

Analogous:

CheckWithin(b,i,If(b,c11,c12), c2) == CheckWithin(b,i,c11,c2)
           ---    ---
CheckWithin(b,i1,CheckWithin(b,i2,c11,c12), c2) == CheckWithin(b,i,c11,c2)
           ---              ---
CheckWithin(b,i1,c1,If(b,c21,c22)) == CheckWithin(b,i1,c1,c22)
           ---        ---

------------------------
Jost + Martin Meeting Jan 15, 2014

Action points:

  - Add concept of managed environment to CONTRACTSIG. Simplify
    simplify - externally, it should work on managed
    environments. Ordinary environments should probably be hidden for
    the user (together with the associated functions that use ordinary
    environments (type env). Doing so allows us to work with relative
    environments internally (for simplicity) and managed environments
    externally.
  DONE

  - Add support for accumulation as an expression:

      e ::= ... | Acc(\v.e,i,a)
 
    Here i is an integer and a is the initial accumulated value. The
    meaning of Acc(f,i,a) is given as f/i(...f/1(f(a))...). Notice
    here that we have extended the notion of promotion to work on
    functions in the obvious way: (\x.e)/i = \x.(e/i).

    This feature allows us to construct a barrier contract that pays a
    EUR at maturity if a boundary has been reached within a period:

      iff(Acc(\x.x !|! (obs("Carlsberg",0) !>! 50.0), y1, B false),
          transl(y1,transfOne(EUR,"me","you")),
          zero)

    This contract can easily be proven to be causal. The feature also
    allows us to define Asian options.

  - We found out that by assuming an observable "Time" : int -> intE,
    we can construct a version of transl that takes an integer
    expression as argument instead of simply an integer:

      fun translE(e,c) =
        checkWithin(obs("Time",0) !=! e, maxInt, c, zero)

    Proving causality for such a construct, may prove to be difficult...

    One cannot simulate a fully dynamic translate with
    checkWithin. There are a number of suptleties that make
    translE(e,c) different:
     - The underlying checkWithin is bounded (in the above by maxInt).
     - In translE(e,c) he expression e is evaluated afresh each
       time step.
     - In translE(e,c) we compare 'e', which should denote relative
       time with obs("Time",0), which should denote absolute time (or
       at least relative to the start time of the "whole" contract,
       otherwise having an observable "Time" makes no sense).

    The semantics of the "Time" observable is non-compositional since
    its value depends on the contexts it appears. This is true for
    observables in general but time should play a different
    role. Maybe its better to have explicit scoping of time by using
    some sort of "clock scope":

      clock cl in ... obs(cl,0) ...

    Here the value of obs(cl,0) is the time relative to the starting
    time of the contract "clock cl in ... obs(cl,0) ..." (no matter
    whether it is nested in a larger contract or not).

    - Comments to JB's comments above by ME:

      The clock can be modelled as follows (from test/contract.sml):

        fun translE(e: intE,c) =
            letc(e !+! obs("Time",0), fn x => checkWithin(obs("Time",0) !=! x, maxInt, c, zero))


 Preparation done in environment definitions. Name is "Time", although
 "days-from-start" might be better. 


  - It may turn out to be useful to be able to extract a specification
    of what underlyings it will make use of for the next N days, say...

  - Other features:
     + compute the horizon for a contract...
    DONE

-------------------------------------------

extracting "trigger values" for contracts, brainstorm:

Interesting expressions are the boolean expr. inside CheckWithin and If.
If is a special case of CheckWithin. (but see ***)

Example: 

         Both (CheckWithin( 6.9 < USD/SEK@0, 10, c1, c2),
               CheckWithin( 6.4 < USD/SEK@0, 10, c3, c4))

can lead to different outcomes: Both c1 c3,  (6.9 breached within 10)
                                Both c2 c3,  (6.4 breached within 10, 6.9 not)
                                Both c2 c4   (none breached within 10)
Trigger values: 6.4, 6.9

A "time window" is associated with each trigger value (its "horizon").

We might (for now) just compute trigger values for given dates. (?) ***

Idea:
  compute trigger values
  generate environments for each "area" between them
                                      6.4            6.9
                  (Example: ___________|______________|_________ )
  simplify the contract for each "area"

Challenge: leaving environment (otherwise) symbolic, to account for Scale
contracts with the same expressions as the ones we fix to get the areas.

More complex cases:

   If ( USD/SEK@1 < USD/SEK@0 * SEK/DKK@1, c1, c2)

this one should become a side condition for each of the areas, or just
be presented to the user.

   If ( 6.9 < USD/SEK@0 * SEK/DKK@1, c1, c2)

unsure about this one... simple "areas" are not possible with it
(unless 2-dimensional ones, hyperplanes).

   If (6.9 < Acc((Var a, a !+! USD/SEK@0, d, R 0), ...)

We cannot do that one!

Further work:

generalise "simplify(0)" to identify a trigger values if its fixing is
not available, then recursively split into the two cases (and remember
the resp. trigger), returning a list of contracts with "trigger
fixings".