lazy.rkt

#lang racket
(require redex)

;; There are many different semantics for Call-By-Need
;; in the literature.  Some are purely syntactic:
;; they model sharing using `let' and have complicated 
;; notions of evaluation contexts (e.g. Ariola and 
;; Felleisen). Others are heap-based natural semantics
;; (e.g. Launchbury).

;; This is a heap-based reduction semantics with
;; explicit substitutions.

;; NB: Jan Midtgaard points out that a substitution-based
;; variant of this semantics appears in: Danvy and Zerny,
;; A Synthetic Operational Account of Call-by-Need Evaluation
;; https://dl.acm.org/citation.cfm?id=2505898

(define-language Λ
  ; Terms
  (M ::= X (M M) (λ X M))
  (X ::= variable-not-otherwise-mentioned)
  ; Evaluation contexts
  (E ::= hole (E C) (force A E))
  ; Closures
  (C ::= (C C) (M R) (force A C))
  ; Environments
  (R ::= ((X A) ...))
  ; Addresses
  (A ::= natural)
  ; Stores
  (Σ ::= ((A S) ...))
  ; Storeables
  (S ::= (delay C) V)
  ; Values
  (V ::= ((λ X M) R)))

; Reduction axioms
(define step
  (reduction-relation 
   Λ #:domain (C Σ)
   (--> ((X R) Σ)
        (V Σ)
        (where V (lookup Σ (lookup R X)))
        var-val)
   (--> ((X R) Σ)
        ((force A C) Σ)
        (where A (lookup R X))
        (where (delay C) (lookup Σ A))        
        var-delay)
   
   (--> ((force A V) Σ)
        (V (:= Σ A V))
        save)
   
   (--> (((M_0 M_1) R) Σ)
        (((M_0 R) (M_1 R)) Σ)
        dist-env)
   
   (--> ((((λ X M) R) C) Σ)
        ((M (ext R X A)) (ext Σ A (delay C)))
        (where A (alloc Σ))
        β)))

; One-step reduction in context

; Looks a bit ugly, but this is just doing:
;     C Σ -> C' Σ'
; -------------------
;  E[C] Σ -> E[C'] Σ'

(define -->_step
  (reduction-relation 
   Λ #:domain (C Σ)
   (--> ((in-hole E C_0) Σ_0)
        ((in-hole E C_1) Σ_1)
        (where (_ ... (any_n (C_1 Σ_1)) _ ...)
               ,(apply-reduction-relation/tag-with-names 
                 step
                 (term (C_0 Σ_0))))
        (computed-name (term any_n)))))

; Lookup in a finite map
(define-metafunction Λ
  lookup : ((any any) ...) any -> any
  [(lookup ((any_x any_y) _ ...) any_x) any_y]
  [(lookup (_ any_b ...) any_x)
   (lookup (any_b ...) any_x)])

; Extend a finite map
(define-metafunction Λ
  ext : ((any any) ...) any any -> ((any any) ...)
  [(ext (any_b ...) any_x any_y)
   ((any_x any_y) any_b ...)])

; Heap update
(define-metafunction Λ
  := : Σ A S -> Σ
  [(:= ((A _) any ...) A S)
   ((A S) any ...)]
  [(:= ((A_0 S_0) any ...) A S)
   ((A_0 S_0) any_0 ...)
   (where (any_0 ...) (:= (any ...) A S))])

; Allocate a fresh address
(define-metafunction Λ
  alloc : Σ -> A
  [(alloc ((any_x any_y) ...))
   ,(add1 (apply max (term (0 any_x ...))))])



; An example that demonstrates sharing in z.
(traces -->_step
        (term ((((λ z (z (z (λ a a)))) 
                 ((λ x x) (λ y y))) ()) ())))