Dependent Type Theory
We are creating a development environment for dependent type theories.
Automatic Differentiation
A prototype for automatic differentiation in Scheme.
Partial application
> (reduce + (map (flip expt 2)
'(0 1 2 3)))
14The sum of squares of a list.
Defining new functions
(definec (f x θ)
(adot θ x 1))
(definec (mse x y)
(mean (expt (- y x)
2)))
(definec loss
(∘ (mse #0(1))
(f #(1/4 3/4))))
> (map loss '(#(4 4/3) #(1 0) #(2 2/3)))
(1 9/16 0)
Loss over parameters `θ' of a model `f' evaluated at `x' = #(1/4 3/4) using the mean square error `mse' with respect to an expected output of 1.
Automatic differentiation
> (map (rdiff loss) '(#(4 4/3) #(1 0) #(2 2/3)))
(#(1/2 3/2) #(-3/8 -9/8) #(0 0))
> (map (fdiff (flip expt 2)) '(0 1 2 3))
(0 2 4 6)The derivative of the loss at each input and the derivative 2x of x^2.
Acknowledgements
We acknowledge and are grateful for the support of the NGI Zero Core project from NLnet.
Contact
Email: admin@vouivredigital.com