#### 3.15Problem: 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.