<commit_before>#lang racket
(require redex)
(require "close.rkt")
(require "common.rkt")

;;
;; 5 Lab Designing Reductions
;;

;; Given:

(define-extended-language Lambda-η Lambda
  (e ::= .... n)
  (n ::= natural)
  (C ::=
     hole
     (e ... C e ...)         ; call-by-name
     (lambda (x_!_ ...) C))
  (v ::=                     ; values
     n
     (lambda (x ...) e)))

(define lambda-η? (redex-match? Lambda-η e))

(define -->β
  (reduction-relation
   Lambda-η
   (--> (in-hole C ((lambda (x_1 ..._n) e) e_1 ..._n)) ; call-by-name
        (in-hole C (subst ([e_1 x_1] ...) e))
        β)))

;; HC add tests:

(define e1 (term ((lambda (x) x) 3)))
(define e2 (term ((lambda (x) x)
                  ((lambda (y) y) 3))))
(define e3 (term ((lambda (a) (c a)) 1)))

(module+ test
  (test--> -->β (term  0                 )     ) ; expect nothing
  (test--> -->β (term  (lambda (x) x)    )     ) ; expect nothing
  (test--> -->β (term ((lambda (x) x) 3) )    3) ; β reduction
  (test--> -->β e1 3)
  ;; with α equivalence there is just one result
  (test--> -->β #:equiv =α/racket
           e2
           (term ((lambda (x) x) 3)))
  ;; without α equivalence there are two results
  (test--> -->β
           e2
           (term ((lambda (x) x) 3))
           (term ((lambda (y) y) 3)))
  ;; do all redexes
  (test-->> -->β
           e2
           3)
  ;; application
  (test--> -->β #:equiv =α/racket
           e3
           (term (c 1)))
  )
  
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Exercise 4.
;; Develop a βη reduction relation for Lambda-η.

(module+ test
  ;; see if new reduction handles existing above
  (test-->> -->β-η
           e2
           3)
  (test--> -->β
           (term (lambda (a b c) (c a b c)))
                   ) ; nothing, does not reduce using -->β
  (test--> -->β-η
           (term (lambda (a b c) (c a b c)))
           (term c)) ; the η reduction
  )

(define -->β-η
  (extend-reduction-relation
   -->β
   Lambda-η
   (--> (in-hole C (lambda (x ..._n) (e e_1 ..._n)))
        (in-hole C e)
        β-η)))

;; --------------------------------------------------
;; Find a term that contains both a β- and an η-redex.
;; Formulate a Redex test that validates this claim.
;; Also use trace to graphically validate the claim.

(module+ test
  (define ex (term ((lambda (a b c) (lambda (x y) (z x y)))
                    1 2 3)))
  (test--> -->β-η #:equiv =α/racket
            ex
            (term ((lambda (a b c) z) 1 2 3)) ; η reduction
            (term (lambda (x y) (z x y))))    ; β reduction
  (test--> -->β-η
            (term (lambda (x y) (z x y)))     ; β reduction result from above
            (term z))
  (test-->> -->β-η
            ex
            (term z))
;  (traces -->β   ex)
;  (traces -->β-η ex)
  )

;;--------------------------------------------------
;; Develop the β and βη STANDARD REDUCTION RELATIONS.
;; Hint Look up extend-reduction-relation to save some work.
;; TODO - RESUME RIGHT HERE

(define-extended-language Standard-η Lambda-η
  (E ::=
     hole
     (v ... E e ...)))

(module+ test
  (define t0
    (term
     ((lambda (a b) (a b))
      ((lambda (d) d) (lambda (e) e))
      ((lambda (f) f) 5))))
  (define t0-one-step
    (term
     ((lambda (a b) (a b))
      (lambda (e) e)
      ((lambda (f) f) 5))))

  ; yields only one term, leftmost-outermost
  ; TODO
;  (test--> -->β-s #:equiv =α/racket t0 t0-one-step)
  ; but the transitive closure drives it to 5
  (test-->> -->β-η-s t0 5))

(define -->β-s
  (extend-reduction-relation
   -->β
   Standard-η
   (--> (in-hole E ((lambda (x_1 ..._n) e) v_1 ..._n))
        (in-hole E (subst ((v_1 x_1) ...) e)))))

(define -->β-η-s
  (extend-reduction-relation<commit_msg>PLT-REDEX<commit_after>#lang racket
(require redex)
(require "close.rkt")
(require "common.rkt")

;;
;; 5 Lab Designing Reductions
;;

;; Given:

(define-extended-language Lambda-η Lambda
  (e ::= .... n)
  (n ::= natural)
  (C ::=
     hole
     (e ... C e ...)         ; call-by-name
     (lambda (x_!_ ...) C))
  (v ::=                     ; values
     n
     (lambda (x ...) e)))

(define lambda-η? (redex-match? Lambda-η e))

(define -->β
  (reduction-relation
   Lambda-η
   (--> (in-hole C ((lambda (x_1 ..._n) e) e_1 ..._n)) ; call-by-name
        (in-hole C (subst ([e_1 x_1] ...) e))
        β)))

;; HC add tests:

(define e1 (term ((lambda (x) x) 3)))
(define e2 (term ((lambda (x) x)
                  ((lambda (y) y) 3))))
(define e3 (term ((lambda (a) (c a)) 1)))

(module+ test
  (test--> -->β (term  0                 )     ) ; expect nothing
  (test--> -->β (term  (lambda (x) x)    )     ) ; expect nothing
  (test--> -->β (term ((lambda (x) x) 3) )    3) ; β reduction
  (test--> -->β e1 3)
  ;; another β reduction
  (test--> -->β #:equiv =α/racket
           e3
           (term (c 1)))
  ;; β reduction (no futher redexes than above)
  (test-->> -->β #:equiv =α/racket
           e3
           (term (c 1)))
  ;; with α equivalence there is just one result
  (test--> -->β #:equiv =α/racket
           e2
           (term ((lambda (x) x) 3)))
  ;; withOUT α equivalence there are two results
  (test--> -->β
           e2
           (term ((lambda (x) x) 3))
           (term ((lambda (y) y) 3)))
  ;; do all redexes
  (test-->> -->β
           e2
           3)
  )
  
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Exercise 4.
;; Develop a βη reduction relation for Lambda-η.

(module+ test
  ;; see if new reduction handles examples from above
  (test-->> -->β-η
           e2
           3)
  (test--> -->β
           (term (lambda (a b c) (c a b c)))
                   ) ; nothing, does not reduce using -->β
  ; the η reduction
  (test--> -->β-η
           (term (lambda (a b c) (c a b c)))
           (term c))
  )

(define -->β-η
  (extend-reduction-relation
   -->β
   Lambda-η
   (--> (in-hole C (lambda (x ..._n) (e e_1 ..._n)))
        (in-hole C e)
        β-η)))

;; --------------------------------------------------
;; Find a term that contains both a β and an η redex.
;; Formulate a Redex test that validates this claim.
;; Also use trace to graphically validate the claim.

(module+ test
  (define ex (term ((lambda (a b c)
                      (lambda (x y) (z x y)))
                    1 2 3)))
  (test--> -->β-η #:equiv =α/racket
            ex
            (term ((lambda (a b c) z) 1 2 3)) ; η reduction
            (term (lambda (x y) (z x y))))    ; β reduction
  (test--> -->β-η
            (term (lambda (x y) (z x y)))     ; β reduction result from above
            (term z))
  ; do all redexes
  (test-->> -->β-η
            ex
            (term z))
;  (traces -->β   ex)
;  (traces -->β-η ex)
  )

;;--------------------------------------------------
;; Develop the β and βη STANDARD REDUCTION RELATIONS.
;; Hint Look up extend-reduction-relation to save some work.

(define-extended-language Standard-η Lambda-η
  (E ::=
     hole
     (v ... E e ...)))

(module+ test
  (define t0
    (term
     ((lambda (a b) (a b))
      ((lambda (d) d) (lambda (e) e))
      ((lambda (f) f) 5))))
  (define t0-one-step
    (term
     ((lambda (a b) (a b))
      (lambda (e) e)
      ((lambda (f) f) 5))))

  ; yields only one term, leftmost-outermost
  ; TODO : this currently returns multiple results
  (test--> -->β-s #:equiv =α/racket t0 t0-one-step)
  ; but the transitive closure drives it to final '5' value
  (test-->> -->β-η-s t0 5))

(define -->β-s
  (extend-reduction-relation
   -->β
   Standard-η
   (--> (in-hole E ((lambda (x_1 ..._n) e) v_1 ..._n))
        (in-hole E (subst ((v_1 x_1) ...) e)))))

(define -->β-η-s
  (extend-reduction-relation
{'fraction_non_alphanumeric': 0.2284449075280021, 'fraction_numerical': 0.012763740557436832, 'mean_word_length': 1.624401913875598, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 102, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1896442', 'n_tokens_mistral': 2886, 'n_tokens_neox': 2709, 'n_words': 924}