Imperial College London
Portrait Picture

ProfessorAbbasEdalat

Faculty of Engineering, Department of Computing

Professor in Computer Science & Maths
 
 
 
//

Contact

 

+44 (0)20 7594 8245a.edalat Website

 
 
//

Location

 

420Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Di:2013:10.1007/978-3-642-37075-5_22,
author = {Di, Gianantonio P and Edalat, A},
doi = {10.1007/978-3-642-37075-5_22},
pages = {337--352},
publisher = {Springer},
title = {A Language for Differentiable Functions},
url = {http://dx.doi.org/10.1007/978-3-642-37075-5_22},
year = {2013}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - We introduce  a typed lambda calculus in which real numbers, realfunctions, and in particular continuously differentiable and more generally Lipschitz functions canbe defined.  Given an expression representing a real-valued functionof a real variable in this calculus, we are able to evaluate the expression on anargument but also evaluate the generalised derivative, i.e., theL-derivative, equivalently the Clarke gradient, of the expression on anargument. Moreover, the whole hierarchy of higher order functions onreal numbers can be defined. The language is an extension of PCF witha real number data-type, similar to Real PCF and RL, but is equippedwith primitives for min and max and weighted average to capturecomputable continuously differentiable or Lipschitz functions on real numbers. Wepresent an operational semantics and a denotational semantics based oncontinuous Scott domains and several logical relations on thesedomains. We then prove an adequacy result for the two semantics. Thedenotational semantics is closely linked with AutomaticDifferentiation also called Algorithmic Differentiation, which hasbeen an active area of research in numerical analysis for decades, andour framework can also be considered as providing denotationalsemantics for Automatic Differentiation. We derive a definabilityresult showing that for any computable Lipschitz function there is aclosed  term in the language whose evaluation on any real numbercoincides with the value of the function and whose derivativeexpression also evaluates on the argument to the value of thegeneralised derivative of the function.
AU  - Di,Gianantonio P
AU  - Edalat,A
DO  - 10.1007/978-3-642-37075-5_22
EP  - 352
PB  - Springer
PY  - 2013///
SP  - 337
TI  - A Language for Differentiable Functions
UR  - http://dx.doi.org/10.1007/978-3-642-37075-5_22
UR  - http://www.doc.ic.ac.uk/~ae/
UR  - http://link.springer.com/chapter/10.1007/978-3-642-37075-5_22
ER  -
Download