3.15 Problem: Contracts

Design a reduction semantics (standard or regular) for a Lambda language with contracts. Here is the syntax:
(define-language Lambda
  (e ::=
     x (lambda (x) e) (e e)
     n (+ e e)
     (if0 e e e)
     (c · e x x)
     (blame x))
  (n ::= number)
  (c ::= num? even? odd? pos? (c -> c))
  (x ::= variable-not-otherwise-mentioned))
The contract primitives are interpreted as follows:
  • (num? x) checks whether x is a number, not a function

  • (pos? x) checks whether x is a positive number

  • (even? x) checks whether x is an even number

  • (odd? x) checks whether x is an even number

The contract form (c · e x_s x_c) checks contract c on e. If e breaks the contract, the semantics signals a (blame x_s) error; other contract violations signal a (blame x_c) error.

Consider these three examples where the same contracted function works well, is blamed, or blames its context depending on the argument:
(define a-module (term {(even? -> pos?) · (lambda (x) (+ x 1)) server client}))
(define p-good (term [,a-module 2]))
(define p-bad-server (term [,a-module -2]))
(define p-bad-client (term [,a-module 1]))
Work through the examples by hand to find out why the three programs work fine, blame the server, and blame the client for contract violations, respectively.