Perceptrons and Rosette

percept.rkt

#lang rosette/safe

;; take weights and threshold
;; returns a function that implements a perceptron neuron
(define (neuron weights threshold)
  (λ inputs
    (if ((foldl + 0 (map * weights inputs)) . > . threshold)                                           
        1
        0)))

(define and (neuron `(1 1) 1.5))
(define not (neuron `(-1) -0.1))

(define and-cases
  `(((0 0) 0)
    ((0 1) 0)
    ((1 0) 0)
    ((1 1) 1)))

(define not-cases
  `(((0) 1)
    ((1) 0)))

(define xor-cases
  `(((0 0) 0)
    ((0 1) 1)
    ((1 0) 1)
    ((1 1) 0)))

(define (case-inputs c)
  (first c))

(define (case-answer case)
  (second case))

;; Does a given neuron conform to a set of input/outputs
(define (fits? test-cases neuron)
  (andmap (λ (c) (= (case-answer c)
                    (apply neuron (case-inputs c))))
          test-cases))

;; Generate n symbolic integers in a list
(define (symbolic-weights n)
  (if (zero? n)
      '()
      (begin
        (define-symbolic* weight integer?)
        (cons weight (symbolic-weights (sub1 n))))))

;; Create a neuron with n symbolic weights and a symbolic
;; threshold
(define (symbolic-neuron n)
  (define-symbolic* threshold real?)
  (neuron (symbolic-weights n) threshold))


; Use rosette to find an `and` perceptron
(assert (fits? and-cases (symbolic-neuron 2)))
(displayln "And: ")
(solve #t)
(clear-vc!)

; Now try xor, and it will fail
(assert (fits? xor-cases (symbolic-neuron 2)))
(displayln "Xor: ")
(solve #t)