philnguyen/size-change-terminating-contract.rkt

## size-change-terminating-contract.rkt
#lang racket/base

(require racket/contract
         racket/set
         racket/match
         redex)

(define-language L
  ;; Syntax
  ;; λ-calculus extended with:
  ;; - `(Fin E)` enforcing that `E` computes a terminating function
  ;; - Named functions to make recursion easy
  [#|Expression  |# E ::= V X (if E E E) (E E ...) (Fin E)]
  [#|Literal     |# V ::= (Fun (X X ...) E) O N]
  [#|Primitive   |# O ::= car cdr sub1 add1 integer? pair? procedure? zero? cons + - *]
  [#|Integer     |# N ::= integer]
  [#|Variable    |# X ::= variable-not-otherwise-mentioned]
  ;; Semantics
  ;; CESK-like machine with:
  ;; - A: The answer
  ;; - K: Intra-precedural continuation
  ;; - M: Continuation mark at coarse procedural level
  ;;      + M maps each clsoure `W` to:
  ;;        * the most recent call's bindings, and
  ;;        * the observed size-change graphs of `W` calling itself in current call chain
  ;;      + the empty map `M` is abused as a flag for "termination not being enforced"
  ;; - Ξ: Continuation store, mapping each kont. address to the caller's
  ;;      continuation and mark
  ;; The concrete semantics does not model value allocation, hence no value-store.
  [#|State       |# S ::= (A K M Ξ)]
  [#|Answer      |# A ::= W (Err any)]
  [#|Local Kont  |# K ::= (Rt α) (if • E E Ρ ∷ K) (W ... • E ... Ρ ∷ K) (Fin • ∷ K)]
  [#|Value       |# W ::= (Clo (X X ...) E Ρ) (Fin W) (cons W W) O N]
  [#|Env.        |# Ρ ::= (side-condition (name Ρ any) (Ρ? (term Ρ)))] ; X → W
  [#|Kont. Store |# Ξ ::= (side-condition (name Ξ any) (Ξ? (term Ξ)))] ; α → K×M
  [#|Kont. Mark  |# M ::= (side-condition (name M any) (M? (term M)))] ; Clo → ℘(x×W) × ℘(G)
  [#|Frames+Mark |# KM ::= (K M)]
  [#|Kont. Addr  |# α ::= integer]
  [#|Change Graph|# G ::= (side-condition (name G any) (G? (term G)))]
  [#|Edge        |# D ::= (X R X)]
  [#|Change      |# ?R ::= ↓ ↧ #f] ; ↓ ⊏ ↧ ⊏ #f
  [#|Descending  |# R ::= ↓ ↧])

(define X? (redex-match? L X))
(define W? (redex-match? L W))
(define D? (redex-match? L D))
(define G? (set/c D?))
(define Ρ? (hash/c X? W? #:flat? #t))
(define Ξ? (hash/c integer? (redex-match? L KM) #:flat? #t))
(define M? (hash/c W? (list/c (hash/c X? W? #:flat? #t) (set/c G?)) #:flat? #t))

(define-term mt ,(hash))

(define-metafunction L
  inj : E -> S
  [(inj E) (↠ E mt (Rt -1) mt mt)])

(define-syntax-rule (viz p) (traces -> (term (inj p))))
(define-syntax-rule (evl p) (apply-reduction-relation* -> (term (inj p))))

(define ->
  (reduction-relation
   L #:domain S
   ;; Standard stuff
   [--> (W (if • E _ Ρ ∷ K) M Ξ)
        (↠ E Ρ K M Ξ)
        if-T
        (where #t (truish? W))]
   [--> (W (if • _ E Ρ ∷ K) M Ξ)
        (↠ E Ρ K M Ξ)
        if-F
        (where #f (truish? W))]
   [--> (W_i-1 (W_1 ... • E_i E_i+1 ... Ρ ∷ K) M Ξ)
        (↠ E_i Ρ (W_1 ... W_i-1 • E_i+1 ... Ρ ∷ K) M Ξ)
        App-Swap]
   [--> (W_n (O W_1 ... • _ ∷ K) M Ξ)
        ((δ O W_1 ... W_n) K M Ξ)
        App-Prim]
   [--> (W_n (W_1 ... • _ ∷ K) M Ξ)
        (↠ E Ρ_1 K_1 M Ξ_1)
        App-Clo
        (where ((Clo (X_f X ..._1) E Ρ) W_x ..._1) (W_1 ... W_n))
        (where (Ρ_1 K_1 Ξ_1) (app-clo W_1 ... W_n K M Ξ))
        (where #f (monitoring? M))]
   [--> (W (Rt α) _ Ξ)
        (W K M Ξ)
        Rt
        (where (K M) (@ Ξ α #f))]
   ;; Relevant stuff, with some duplication in `App-Clo-*` rules
   [--> (W_n (W_1 ... • _ ∷ K) M Ξ)
        (↠ E Ρ_1 K_1 M_1 Ξ_1)
        App-Clo-Decreased
        (where (W_f W_x ..._1) (W_1 ... W_n))
        (where (Clo (X_f X ..._1) E Ρ) W_f)
        (where (Ρ_1 K_1 Ξ_1) (app-clo W_f W_x ... K M Ξ))
        (where #t (monitoring? M))
        (where M_1 (M++ M W_f W_x ...))
        (where #t (size-change-terminating? M_1 W_f))]
   [--> (W_n (W_1 ... • _ ∷ K) M Ξ)
        ((Err (May-Diverge W_f W_x ...)) K M_1 Ξ)
        App-Clo-Killed
        (where (W_f W_x ..._1) (W_1 ... W_n))
        (where (Clo (X_f X ..._1) E Ρ) W_f)
        (where (Ρ_1 K_1 Ξ_1) (app-clo W_f W_x ... K M Ξ))
        (where #t (monitoring? M))
        (where M_1 (M++ M W_f W_x ...))
        (where #f (size-change-terminating? M_1 W_f))]
   [--> (W_n (W_1 ... • _ ∷ K) M Ξ)
        (↠ E Ρ_1 K_1 (M++ M W_f W_x ...) Ξ_1)
        App-Fin
        (where ((Fin W_f) W_x ..._1) (W_1 ... W_n))
        (where (Clo (X_f X ..._1) E Ρ) W_f)
        (where (Ρ_1 K_1 Ξ_1) (app-clo (Clo (X_f X ...) E Ρ) W_x ... K M Ξ))]
   [--> (W (Fin • ∷ K) M Ξ)
        ((fin W) K M Ξ)
        Fin]))

(define-metafunction L
  ;; Fast-forward all "push" reductions to compress state space
  ↠ : E Ρ K M Ξ -> S
  [(↠ E Ρ K M Ξ) (W K_1 M Ξ)
   (where (W K_1) (ev E Ρ K))])

(define-metafunction L
  ev : E Ρ K -> (W K)
  [(ev X Ρ K) ((@ Ρ X) K)]
  [(ev V Ρ K) ((clo V Ρ) K)]
  [(ev (if E E_1 E_2) Ρ K) (ev E Ρ (if • E_1 E_2 Ρ ∷ K))]
  [(ev (E_1 E ...) Ρ K) (ev E_1 Ρ (• E ... Ρ ∷ K))]
  [(ev (Fin E) Ρ K) (ev E Ρ (Fin • ∷ K))])

(define-metafunction L
  ;; Close value
  clo : V Ρ -> W
  [(clo (Fun (X ...) E) Ρ) (Clo (X ...) E Ρ)]
  [(clo V _) V])

(define-metafunction L
  ;; Factor out standard/boring allocations/extensions for applying closures
  app-clo : W W ... K M Ξ -> (Ρ K Ξ)
  [(app-clo (name W_f (Clo (X_f X ..._1) E Ρ)) W ..._1 K M Ξ)
   (Ρ_1 (Rt α) (++ Ξ [α ↦ (K M)]))
   (where Ρ_1 (++ Ρ [X_f ↦ W_f] [X ↦ W] ...))
   (where α ,(hash-count (term Ξ)))])

(define-metafunction L
  ;; Wrap closure in `(Fin _)`
  fin : W -> W
  [(fin (Clo (X ...) E Ρ)) (Fin (Clo (X ...) E Ρ))]
  [(fin W) W])

(define-metafunction L
  truish? : W -> boolean
  [(truish? 0) #f]
  [(truish? _) #t])

;; `↓` is definite descendence
;; `↧` is definite non-ascendence
;; `#f` is conservative "don't know"
(define-metafunction L
  ;; Judge the transition between values based on some well-founded partial order
  cmp : W W -> ?R
  [(cmp W W) ↧]
  [(cmp N_1 N_2) ,(and (> (term N_1) (term N_2) -1) '↓)]
  [(cmp (cons W_1 W_2) W)
   ,(and (ormap values (term ((cmp W_1 W) (cmp W_2 W)))) '↓)]
  [(cmp _ _) #f])

(define-metafunction L
  M++ : M W W ... -> M
  [(M++ M (name W_f (Clo (_ X ..._1) _ _)) W ..._1)
   ,(hash-set (term M) (term W_f)
              (term ((++ mt [X ↦ W] ...)
                     ,(refl-trans (set (list->set (term ([X ↓ X] ...))))))))
   (side-condition (not (hash-has-key? (term M) (term W_f))))]
  [(M++ M (name W_f (Clo (_ X ..._1) _ _)) W ..._1)
   ,(hash-update (term M) (term W_f)
                 (match-lambda
                   [`(,h₀ ,s₀)
                    (define h₁ (term (++ mt [X ↦ W] ...)))
                    (term (,h₁ ,(refl-trans (set-add s₀ (mk-graph h₀ h₁)))))]))])

(define-metafunction L
  monitoring? : M -> boolean
  [(monitoring? M) ,(not (hash-empty? (term M)))])

(define-relation L
  ;; Check if current call-chain of function `W` is making progress
  ;; by not violating the `size-change-terminating` principle
  size-change-terminating? ⊆ M × W
  [(size-change-terminating? M W)
   (where (_ any_graphs) (@ M W))
   ;; Step 2 in Algorithm in section 3.2
   ;; Could simplify some double negations but just matching paper for now
   (side-condition
    (not (for/or ([G (in-set (term any_graphs))])
           (and (equal? G (compose-graph G G))
                (not (for/or ([edge (in-set G)])
                       (match edge
                         [`(,s ↓ ,s) #t]
                         [_ #f])))))))])

(define-metafunction L
  ;; Compose non-ascending transitions
  ∘ : R R ... -> R
  [(∘ _ ... ↓ _ ...) ↓]
  [(∘ _ ...) ↧])

;; Make size-change graph from comparing old and new bindings
(define (mk-graph h₀ h₁)
  (for*/set ([(X₀ W₀) (in-hash h₀)]
             [(X₁ W₁) (in-hash h₁)]
             [R (in-value (term (cmp ,W₀ ,W₁)))] #:when R)
    (term (,X₀ ,R ,X₁))))

;; Compose size-change graphs
(define (compose-graph G₁ G₂)
  (define (compact G)
    (for/fold ([G* G])
              ([edge (in-set G)]
               #:when (match-let ([`(,s ,↝ ,t) edge])
                        (and (equal? ↝ '↧)
                             (set-member? G `(,s ↓ ,t)))))
      (set-remove G* edge)))
  (compact
   (for*/set ([edge₁ (in-set G₁)]
              [edge₂ (in-set G₂)]
              [?edge
               (in-value
                (match-let ([`(,s₁ ,↝₁ ,t₁) edge₁]
                            [`(,s₂ ,↝₂ ,t₂) edge₂])
                  (and (equal? t₁ s₂)
                       (term (,s₁ (,↝₁ . ∘ . ,↝₂) ,t₂)))))]
              #:when ?edge)
     ?edge)))

;; Step 1 in algorithm in section 3.2
(define (refl-trans Gs)
  (define (trans Gs)
    (set-union Gs (for*/set ([G₁ (in-set Gs)]
                             [G₂ (in-set Gs)] #:unless (eq? G₁ G₂))
                    (compose-graph G₁ G₂))))
  (let fix ([Gs Gs])
    (define Gs* (trans Gs))
    (if (equal? Gs* Gs) Gs (fix Gs*))))

(define-metafunction L
  δ : O W ... -> A
  [(δ car (cons W _)) W]
  [(δ cdr (cons _ W)) W]
  [(δ sub1 N) ,(sub1 (term N))]
  [(δ add1 N) ,(add1 (term N))]
  [(δ + N_1 N_2) ,(+ (term N_1) (term N_2))]
  [(δ - N_1 N_2) ,(- (term N_1) (term N_2))]
  [(δ * N_1 N_2) ,(* (term N_1) (term N_2))]
  [(δ integer? N) 1]
  [(δ integer? _) 0]
  [(δ zero? 0) 1]
  [(δ zero? _) 0]
  [(δ pair? (cons _ _)) 1]
  [(δ pair? _) 0]
  [(δ procedure? (Clo _ ...)) 1]
  [(δ procedure? O) 1]
  [(δ procedure? _) 0]
  [(δ cons W_1 W_2) (cons W_1 W_2)]
  [(δ O W ...) (Err (undefined O W ...))])

(define-metafunction L
  ;; Extend map
  ++ : any [any ↦ any] ... -> any
  [(++ any) any]
  [(++ any_m [any_k ↦ any_v] any ...)
   (++ ,(hash-set (term any_m) (term any_k) (term any_v)) any ...)])

(define-metafunction L
  ;; Lookup map, with optional default
  @ : any any any ... -> any
  [(@ any_m any_k) (@ any_m any_k ,(λ () (error '@ "not-found ~a" (term any_k))))]
  [(@ any_m any_k any_default) ,(hash-ref (term any_m) (term any_k) (term any_default))])


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; Macros
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-metafunction L
  -let : ([X E] ...) E -> E
  [(-let ([X E_x] ...) E) ((Fun (LET X ...) E) E_x ...)])

(define-metafunction L
  -cond : [E E] ... [else E] -> E
  [(-cond [else E]) E]
  [(-cond [E_1 E_2] any ...) (if E_1 E_2 (-cond any ...))])

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; Paper examples
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-term ex-1 ; accumulating parameters
  (-let ([r1 (Fun (r1 ls a)
                  (if (pair? ls)
                      (r1 (cdr ls) (cons (car ls) a))
                      a))])
    ((Fin (Fun (rev l) (r1 l 0))) (cons 1 (cons 2 (cons 3 0))))))

(define-term ex-2-a ; indirect recursion, encoded compared to paper
  ; start with `f`
  ((Fin (Fun (fg f? i/a x/b c)
             (if f?
                 (if (zero? i/a) x/b (fg 0 (cdr i/a) x/b i/a))
                 (fg 1 i/a (cons x/b c) 0))))
   1
   (cons 1 (cons 2 0))
   42
   0))
(define-term ex-2-b ; indirect recursion, encoded compared to paper
  ; start with `g`
  ((Fin (Fun (fg f? i/a x/b c)
             (if f?
                 (if (zero? i/a) x/b (fg 0 (cdr i/a) x/b i/a))
                 (fg 1 i/a (cons x/b c) 0))))
   0
   (cons 1 (cons 2 0))
   42
   0))

(define-term ex-3 ; lexically ordered parameters
  ((Fin (Fun (a m n)
             (-cond [(zero? m) (add1 n)]
                    [(zero? n) (a (sub1 m) 1)]
                    [else (a (sub1 m) (a m (sub1 n)))])))
   1 2))

(define-term ex-4 ; permuted parameters
  ((Fin (Fun (p m n r)
             (-cond [r (p m (sub1 r) n)]
                    [n (p r (sub1 n) m)]
                    [else m])))
   3 4 5))

(define-term ex-5 ; permuted and discarded parameters
  ((Fin (Fun (f x y)
             (-cond [(zero? y) x]
                    [(zero? x) (f y (cdr y))]
                    [else (f y (cdr x))])))
   (cons 1 (cons 2 0))
   (cons 3 (cons 4 0))))

(define-term ex-6 ; late starting sequence of descending parameter values
  (-let ([g (Fun (g c d)
                 (if (zero? c) d
                     (g (cdr c) (cons (car c) d))))])
    ((Fin (Fun (f a b) (if (zero? b) (g a 0)
                           (f (cons (car b) a) (cdr b)))))
     (cons 1 (cons 2 0))
     (cons 3 (cons 4 0)))))

(module+ test
  (evl ex-1)
  (evl ex-2-a)
  (evl ex-2-b)
  (evl ex-3)
  (evl ex-4)
  (evl ex-5)
  (evl ex-6))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; Other examples
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-term ex-loop
  ((Fin (Fun (f x y)
             (if (zero? x) 42 (f (sub1 y) (add1 x)))))
   3 3))

(define-term fact-loop
  ((Fin (Fun (fact n)
             (if (zero? n) 1
                 (* n (fact (sub1 n))))))
   -1))

(define-term fact-ok
  ((Fin (Fun (fact n)
             (if (zero? n) 1
                 (* n (fact (sub1 n))))))
   3))

(module+ test
  (evl ex-loop)
  (evl fact-loop)
  (evl fact-ok))
	#lang racket/base

	(require racket/contract
	racket/set
	racket/match
	redex)

	(define-language L
	;; Syntax
	;; λ-calculus extended with:
	;; - `(Fin E)` enforcing that `E` computes a terminating function
	;; - Named functions to make recursion easy
	[#\|Expression \|# E ::= V X (if E E E) (E E ...) (Fin E)]
	[#\|Literal \|# V ::= (Fun (X X ...) E) O N]
	[#\|Primitive \|# O ::= car cdr sub1 add1 integer? pair? procedure? zero? cons + - *]
	[#\|Integer \|# N ::= integer]
	[#\|Variable \|# X ::= variable-not-otherwise-mentioned]
	;; Semantics
	;; CESK-like machine with:
	;; - A: The answer
	;; - K: Intra-precedural continuation
	;; - M: Continuation mark at coarse procedural level
	;; + M maps each clsoure `W` to:
	;; * the most recent call's bindings, and
	;; * the observed size-change graphs of `W` calling itself in current call chain
	;; + the empty map `M` is abused as a flag for "termination not being enforced"
	;; - Ξ: Continuation store, mapping each kont. address to the caller's
	;; continuation and mark
	;; The concrete semantics does not model value allocation, hence no value-store.
	[#\|State \|# S ::= (A K M Ξ)]
	[#\|Answer \|# A ::= W (Err any)]
	[#\|Local Kont \|# K ::= (Rt α) (if • E E Ρ ∷ K) (W ... • E ... Ρ ∷ K) (Fin • ∷ K)]
	[#\|Value \|# W ::= (Clo (X X ...) E Ρ) (Fin W) (cons W W) O N]
	[#\|Env. \|# Ρ ::= (side-condition (name Ρ any) (Ρ? (term Ρ)))] ; X → W
	[#\|Kont. Store \|# Ξ ::= (side-condition (name Ξ any) (Ξ? (term Ξ)))] ; α → K×M
	[#\|Kont. Mark \|# M ::= (side-condition (name M any) (M? (term M)))] ; Clo → ℘(x×W) × ℘(G)
	[#\|Frames+Mark \|# KM ::= (K M)]
	[#\|Kont. Addr \|# α ::= integer]
	[#\|Change Graph\|# G ::= (side-condition (name G any) (G? (term G)))]
	[#\|Edge \|# D ::= (X R X)]
	[#\|Change \|# ?R ::= ↓ ↧ #f] ; ↓ ⊏ ↧ ⊏ #f
	[#\|Descending \|# R ::= ↓ ↧])

	(define X? (redex-match? L X))
	(define W? (redex-match? L W))
	(define D? (redex-match? L D))
	(define G? (set/c D?))
	(define Ρ? (hash/c X? W? #:flat? #t))
	(define Ξ? (hash/c integer? (redex-match? L KM) #:flat? #t))
	(define M? (hash/c W? (list/c (hash/c X? W? #:flat? #t) (set/c G?)) #:flat? #t))

	(define-term mt ,(hash))

	(define-metafunction L
	inj : E -> S
	[(inj E) (↠ E mt (Rt -1) mt mt)])

	(define-syntax-rule (viz p) (traces -> (term (inj p))))
	(define-syntax-rule (evl p) (apply-reduction-relation* -> (term (inj p))))

	(define ->
	(reduction-relation
	L #:domain S
	;; Standard stuff
	[--> (W (if • E _ Ρ ∷ K) M Ξ)
	(↠ E Ρ K M Ξ)
	if-T
	(where #t (truish? W))]
	[--> (W (if • _ E Ρ ∷ K) M Ξ)
	(↠ E Ρ K M Ξ)
	if-F
	(where #f (truish? W))]
	[--> (W_i-1 (W_1 ... • E_i E_i+1 ... Ρ ∷ K) M Ξ)
	(↠ E_i Ρ (W_1 ... W_i-1 • E_i+1 ... Ρ ∷ K) M Ξ)
	App-Swap]
	[--> (W_n (O W_1 ... • _ ∷ K) M Ξ)
	((δ O W_1 ... W_n) K M Ξ)
	App-Prim]
	[--> (W_n (W_1 ... • _ ∷ K) M Ξ)
	(↠ E Ρ_1 K_1 M Ξ_1)
	App-Clo
	(where ((Clo (X_f X ..._1) E Ρ) W_x ..._1) (W_1 ... W_n))
	(where (Ρ_1 K_1 Ξ_1) (app-clo W_1 ... W_n K M Ξ))
	(where #f (monitoring? M))]
	[--> (W (Rt α) _ Ξ)
	(W K M Ξ)
	Rt
	(where (K M) (@ Ξ α #f))]
	;; Relevant stuff, with some duplication in `App-Clo-*` rules
	[--> (W_n (W_1 ... • _ ∷ K) M Ξ)
	(↠ E Ρ_1 K_1 M_1 Ξ_1)
	App-Clo-Decreased
	(where (W_f W_x ..._1) (W_1 ... W_n))
	(where (Clo (X_f X ..._1) E Ρ) W_f)
	(where (Ρ_1 K_1 Ξ_1) (app-clo W_f W_x ... K M Ξ))
	(where #t (monitoring? M))
	(where M_1 (M++ M W_f W_x ...))
	(where #t (size-change-terminating? M_1 W_f))]
	[--> (W_n (W_1 ... • _ ∷ K) M Ξ)
	((Err (May-Diverge W_f W_x ...)) K M_1 Ξ)
	App-Clo-Killed
	(where (W_f W_x ..._1) (W_1 ... W_n))
	(where (Clo (X_f X ..._1) E Ρ) W_f)
	(where (Ρ_1 K_1 Ξ_1) (app-clo W_f W_x ... K M Ξ))
	(where #t (monitoring? M))
	(where M_1 (M++ M W_f W_x ...))
	(where #f (size-change-terminating? M_1 W_f))]
	[--> (W_n (W_1 ... • _ ∷ K) M Ξ)
	(↠ E Ρ_1 K_1 (M++ M W_f W_x ...) Ξ_1)
	App-Fin
	(where ((Fin W_f) W_x ..._1) (W_1 ... W_n))
	(where (Clo (X_f X ..._1) E Ρ) W_f)
	(where (Ρ_1 K_1 Ξ_1) (app-clo (Clo (X_f X ...) E Ρ) W_x ... K M Ξ))]
	[--> (W (Fin • ∷ K) M Ξ)
	((fin W) K M Ξ)
	Fin]))

	(define-metafunction L
	;; Fast-forward all "push" reductions to compress state space
	↠ : E Ρ K M Ξ -> S
	[(↠ E Ρ K M Ξ) (W K_1 M Ξ)
	(where (W K_1) (ev E Ρ K))])

	(define-metafunction L
	ev : E Ρ K -> (W K)
	[(ev X Ρ K) ((@ Ρ X) K)]
	[(ev V Ρ K) ((clo V Ρ) K)]
	[(ev (if E E_1 E_2) Ρ K) (ev E Ρ (if • E_1 E_2 Ρ ∷ K))]
	[(ev (E_1 E ...) Ρ K) (ev E_1 Ρ (• E ... Ρ ∷ K))]
	[(ev (Fin E) Ρ K) (ev E Ρ (Fin • ∷ K))])

	(define-metafunction L
	;; Close value
	clo : V Ρ -> W
	[(clo (Fun (X ...) E) Ρ) (Clo (X ...) E Ρ)]
	[(clo V _) V])

	(define-metafunction L
	;; Factor out standard/boring allocations/extensions for applying closures
	app-clo : W W ... K M Ξ -> (Ρ K Ξ)
	[(app-clo (name W_f (Clo (X_f X ..._1) E Ρ)) W ..._1 K M Ξ)
	(Ρ_1 (Rt α) (++ Ξ [α ↦ (K M)]))
	(where Ρ_1 (++ Ρ [X_f ↦ W_f] [X ↦ W] ...))
	(where α ,(hash-count (term Ξ)))])

	(define-metafunction L
	;; Wrap closure in `(Fin _)`
	fin : W -> W
	[(fin (Clo (X ...) E Ρ)) (Fin (Clo (X ...) E Ρ))]
	[(fin W) W])

	(define-metafunction L
	truish? : W -> boolean
	[(truish? 0) #f]
	[(truish? _) #t])

	;; `↓` is definite descendence
	;; `↧` is definite non-ascendence
	;; `#f` is conservative "don't know"
	(define-metafunction L
	;; Judge the transition between values based on some well-founded partial order
	cmp : W W -> ?R
	[(cmp W W) ↧]
	[(cmp N_1 N_2) ,(and (> (term N_1) (term N_2) -1) '↓)]
	[(cmp (cons W_1 W_2) W)
	,(and (ormap values (term ((cmp W_1 W) (cmp W_2 W)))) '↓)]
	[(cmp _ _) #f])

	(define-metafunction L
	M++ : M W W ... -> M
	[(M++ M (name W_f (Clo (_ X ..._1) _ _)) W ..._1)
	,(hash-set (term M) (term W_f)
	(term ((++ mt [X ↦ W] ...)
	,(refl-trans (set (list->set (term ([X ↓ X] ...))))))))
	(side-condition (not (hash-has-key? (term M) (term W_f))))]
	[(M++ M (name W_f (Clo (_ X ..._1) _ _)) W ..._1)
	,(hash-update (term M) (term W_f)
	(match-lambda
	[`(,h₀ ,s₀)
	(define h₁ (term (++ mt [X ↦ W] ...)))
	(term (,h₁ ,(refl-trans (set-add s₀ (mk-graph h₀ h₁)))))]))])

	(define-metafunction L
	monitoring? : M -> boolean
	[(monitoring? M) ,(not (hash-empty? (term M)))])

	(define-relation L
	;; Check if current call-chain of function `W` is making progress
	;; by not violating the `size-change-terminating` principle
	size-change-terminating? ⊆ M × W
	[(size-change-terminating? M W)
	(where (_ any_graphs) (@ M W))
	;; Step 2 in Algorithm in section 3.2
	;; Could simplify some double negations but just matching paper for now
	(side-condition
	(not (for/or ([G (in-set (term any_graphs))])
	(and (equal? G (compose-graph G G))
	(not (for/or ([edge (in-set G)])
	(match edge
	[`(,s ↓ ,s) #t]
	[_ #f])))))))])

	(define-metafunction L
	;; Compose non-ascending transitions
	∘ : R R ... -> R
	[(∘ _ ... ↓ _ ...) ↓]
	[(∘ _ ...) ↧])

	;; Make size-change graph from comparing old and new bindings
	(define (mk-graph h₀ h₁)
	(for*/set ([(X₀ W₀) (in-hash h₀)]
	[(X₁ W₁) (in-hash h₁)]
	[R (in-value (term (cmp ,W₀ ,W₁)))] #:when R)
	(term (,X₀ ,R ,X₁))))

	;; Compose size-change graphs
	(define (compose-graph G₁ G₂)
	(define (compact G)
	(for/fold ([G* G])
	([edge (in-set G)]
	#:when (match-let ([`(,s ,↝ ,t) edge])
	(and (equal? ↝ '↧)
	(set-member? G `(,s ↓ ,t)))))
	(set-remove G* edge)))
	(compact
	(for*/set ([edge₁ (in-set G₁)]
	[edge₂ (in-set G₂)]
	[?edge
	(in-value
	(match-let ([`(,s₁ ,↝₁ ,t₁) edge₁]
	[`(,s₂ ,↝₂ ,t₂) edge₂])
	(and (equal? t₁ s₂)
	(term (,s₁ (,↝₁ . ∘ . ,↝₂) ,t₂)))))]
	#:when ?edge)
	?edge)))

	;; Step 1 in algorithm in section 3.2
	(define (refl-trans Gs)
	(define (trans Gs)
	(set-union Gs (for*/set ([G₁ (in-set Gs)]
	[G₂ (in-set Gs)] #:unless (eq? G₁ G₂))
	(compose-graph G₁ G₂))))
	(let fix ([Gs Gs])
	(define Gs* (trans Gs))
	(if (equal? Gs* Gs) Gs (fix Gs*))))

	(define-metafunction L
	δ : O W ... -> A
	[(δ car (cons W _)) W]
	[(δ cdr (cons _ W)) W]
	[(δ sub1 N) ,(sub1 (term N))]
	[(δ add1 N) ,(add1 (term N))]
	[(δ + N_1 N_2) ,(+ (term N_1) (term N_2))]
	[(δ - N_1 N_2) ,(- (term N_1) (term N_2))]
	[(δ * N_1 N_2) ,(* (term N_1) (term N_2))]
	[(δ integer? N) 1]
	[(δ integer? _) 0]
	[(δ zero? 0) 1]
	[(δ zero? _) 0]
	[(δ pair? (cons _ _)) 1]
	[(δ pair? _) 0]
	[(δ procedure? (Clo _ ...)) 1]
	[(δ procedure? O) 1]
	[(δ procedure? _) 0]
	[(δ cons W_1 W_2) (cons W_1 W_2)]
	[(δ O W ...) (Err (undefined O W ...))])

	(define-metafunction L
	;; Extend map
	++ : any [any ↦ any] ... -> any
	[(++ any) any]
	[(++ any_m [any_k ↦ any_v] any ...)
	(++ ,(hash-set (term any_m) (term any_k) (term any_v)) any ...)])

	(define-metafunction L
	;; Lookup map, with optional default
	@ : any any any ... -> any
	[(@ any_m any_k) (@ any_m any_k ,(λ () (error '@ "not-found ~a" (term any_k))))]
	[(@ any_m any_k any_default) ,(hash-ref (term any_m) (term any_k) (term any_default))])


	;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
	;;;;; Macros
	;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

	(define-metafunction L
	-let : ([X E] ...) E -> E
	[(-let ([X E_x] ...) E) ((Fun (LET X ...) E) E_x ...)])

	(define-metafunction L
	-cond : [E E] ... [else E] -> E
	[(-cond [else E]) E]
	[(-cond [E_1 E_2] any ...) (if E_1 E_2 (-cond any ...))])

	;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
	;;;;; Paper examples
	;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

	(define-term ex-1 ; accumulating parameters
	(-let ([r1 (Fun (r1 ls a)
	(if (pair? ls)
	(r1 (cdr ls) (cons (car ls) a))
	a))])
	((Fin (Fun (rev l) (r1 l 0))) (cons 1 (cons 2 (cons 3 0))))))

	(define-term ex-2-a ; indirect recursion, encoded compared to paper
	; start with `f`
	((Fin (Fun (fg f? i/a x/b c)
	(if f?
	(if (zero? i/a) x/b (fg 0 (cdr i/a) x/b i/a))
	(fg 1 i/a (cons x/b c) 0))))
	1
	(cons 1 (cons 2 0))
	42
	0))
	(define-term ex-2-b ; indirect recursion, encoded compared to paper
	; start with `g`
	((Fin (Fun (fg f? i/a x/b c)
	(if f?
	(if (zero? i/a) x/b (fg 0 (cdr i/a) x/b i/a))
	(fg 1 i/a (cons x/b c) 0))))
	0
	(cons 1 (cons 2 0))
	42
	0))

	(define-term ex-3 ; lexically ordered parameters
	((Fin (Fun (a m n)
	(-cond [(zero? m) (add1 n)]
	[(zero? n) (a (sub1 m) 1)]
	[else (a (sub1 m) (a m (sub1 n)))])))
	1 2))

	(define-term ex-4 ; permuted parameters
	((Fin (Fun (p m n r)
	(-cond [r (p m (sub1 r) n)]
	[n (p r (sub1 n) m)]
	[else m])))
	3 4 5))

	(define-term ex-5 ; permuted and discarded parameters
	((Fin (Fun (f x y)
	(-cond [(zero? y) x]
	[(zero? x) (f y (cdr y))]
	[else (f y (cdr x))])))
	(cons 1 (cons 2 0))
	(cons 3 (cons 4 0))))

	(define-term ex-6 ; late starting sequence of descending parameter values
	(-let ([g (Fun (g c d)
	(if (zero? c) d
	(g (cdr c) (cons (car c) d))))])
	((Fin (Fun (f a b) (if (zero? b) (g a 0)
	(f (cons (car b) a) (cdr b)))))
	(cons 1 (cons 2 0))
	(cons 3 (cons 4 0)))))

	(module+ test
	(evl ex-1)
	(evl ex-2-a)
	(evl ex-2-b)
	(evl ex-3)
	(evl ex-4)
	(evl ex-5)
	(evl ex-6))


	;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
	;;;;; Other examples
	;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

	(define-term ex-loop
	((Fin (Fun (f x y)
	(if (zero? x) 42 (f (sub1 y) (add1 x)))))
	3 3))

	(define-term fact-loop
	((Fin (Fun (fact n)
	(if (zero? n) 1
	(* n (fact (sub1 n))))))
	-1))

	(define-term fact-ok
	((Fin (Fun (fact n)
	(if (zero? n) 1
	(* n (fact (sub1 n))))))
	3))

	(module+ test
	(evl ex-loop)
	(evl fact-loop)
	(evl fact-ok))