kmicinski

#lang racket

(define (expr? e)
  (match e
    [(? number? n) #t]
    [(? symbol? x) #t]
    [`(λ (,(? symbol? x)) ,(? expr? e)) #t]
    [`(,(? expr? e0) ,(? expr? e1)) #t]
    [_ #f]))

kmicinski

#lang racket

;; general direct-style recursive template over lists
#;(define (my-function lst)
  (if (empty? lst)
      'base-case
      (let ([result-from-rest-of-list (my-function (rest lst))]
            [first-list (first lst)])
        (f first-list result-from-rest-of-list))))

kmicinski

#lang racket

;; omega term = 
;; ((lambda (x) (x x)) (lambda (x) (x x)))
;; (x x) [ x ↦ (lambda (x) (x x)) ] =
;; ((lambda (x) (x x)) (lambda (x) (x x)))

;; there are two options
'((lambda (x) (lambda (y) y)) ((lambda (x) (x x)) (lambda (x) (x x))))

kmicinski

#lang racket

;; λ-calculus expressions
(define (expr? e)
  (match e
    [(? symbol? x) #t] ;; variables
    [`(λ (,(? symbol? x)) ,(? expr? e-body)) #t] ;; λ abstractions
    [`(,(? expr? e-f) ,(? expr? e-a)) #t] ;; applications
    [_ #f]))

kmicinski

#lang racket

;; CIS700, Fall 2023 -- Kris Micinski
;; 
;; Demo of SMT (SMTLIB) to perform bounded-model checking for an example
;; program.
;; 
;;  // input x, a bit vector of length N
;;  i = 0;
;;  r = 0;

kmicinski

;; CIS352 -- Fall 2023
;; Closure-Creating Interpreters
#lang racket

(define (expr? e)
  (match e
    [(? symbol? x) #t] ;; variables
    [(? number? n) #t]
    ;; single-variable let binding
    [`(let ([,(? symbol? x) ,(? expr? e-let-binding)]) ,(? expr? e-body)) #t]

kmicinski

#lang racket

;; CIS352 Office hours code -- 9/27/2023
;; matching and type predicates

;; Direct-style length
(define (length lst)
  (if (empty? lst)
      0
      (add1 (length (rest lst)))))

kmicinski

#lang racket

;; CIS352 -- Fall 2023
;; Lambdas

;; first order function -- no functions as arguments
;; O(n^2) the way it's written -- an easier implementation
;; is not easy functionally, need a different representation 
(define (reverse lst)
  (if (empty? lst)

kmicinski

#lang racket

;; Recursion over lists
(cons 1 (cons 2 (cons 3 (cons 4 '()))))

;; more laboriously as ...
(let ([last-link (cons 4 '())])
  (let ([second-to-last-link (cons 3 last-link)])
    (let ([third-to-last-link (cons 2 second-to-last-link)])
      (cons 1 third-to-last-link))))

kmicinski

-- see cek.slog
def var := String

-- terms
inductive term : Type where
  | Ref : var → term
  | Lam : var → term → term
  | App : term → term → term
open term