CIS352 'S25 -- 3/20/25

03-20.rkt

#lang racket

;; CIS352 -- March 20, 2025

;; For the past few lectures, we've talked about the idea of "in-context" β:
;; the idea that we can "just do all the βs." So for example:
((λ (b) b)
 (((λ (x) x) (λ (a) a))
  ((λ (y) y) (λ (z) z))))

;; The above term has three different β redexes
;; STOP: can you work them out? Along with the result of β reduction for each

;; The idea this class is to try to come up with a systematic strategy for
;; chosing which β redex to reduce.
;;
;; We will begin by making the following observation:
;; - The key decision we have to make is what to do when we hit an application
;; - In Call-by-Value evaluation order, we *force* the reduction of the
;;   argument to be a *value*.
;; - You can't start executing "into" a λ until you finish materializing the
;;   arguments to values.
;;
;; For example:
;; (f (+ 2 3) (/ 1 0))

;; This program calls the function f. But before it does that, it demands
;; the evaluation of (+ 2 3) and (/ 1 0)--which, of course, is an error.

;; The key idea is to notice that for CBV, when we get to a callsite,
;; we want to reduce the function position to a value (lambda),
;; followed by the argument, followed by traversing into the body.
;;
;; In other words, an exression can progress as follows:
;; (e e) -->* ((λ (x) ...) e) -->* ((λ (x) ...) v) --> (do the call)

;; We'll pick up here.