Abstract
We introduce a typed lambda calculus in which real numbers, real
functions, and in particular continuously differentiable and more generally Lipschitz functions can
be defined. Given an expression representing a real-valued function
of a real variable in this calculus, we are able to evaluate the expression on an
argument but also evaluate the L-derivative of the expression on an
argument. The language is an extension of PCF with
a real number data-type but is equipped
with primitives for min and weighted average to capture
computable continuously differentiable or Lipschitz functions on real numbers. We
present an operational semantics and a denotational semantics based on
continuous Scott domains and several logical relations on these
domains. We then prove an adequacy result for the two semantics. The
denotational semantics also provides denotational
semantics for Automatic Differentiation. We derive a definability
result showing that for any computable Lipschitz function there is a
closed term in the language whose evaluation on any real number
coincides with the value of the function and whose derivative
expression also evaluates on the argument to the value of the
L-derivative of the function.