Differentiation in logical form
We introduce a logical theory of differentiation for a real-valued function on a finite dimensional real Euclidean space. A real-valued continuous function is represented by a localic ap- proximable mapping between two semi-strong proximity lattices, representing the two stably locally compact Eucli...
Main Authors: | , |
---|---|
Format: | Conference Object |
Language: | unknown |
Published: |
ACM / IEEE
2017
|
Subjects: | |
Online Access: | http://hdl.handle.net/10044/1/45827 |
id |
ftimperialcol:oai:spiral.imperial.ac.uk:10044/1/45827 |
---|---|
record_format |
openpolar |
spelling |
ftimperialcol:oai:spiral.imperial.ac.uk:10044/1/45827 2023-05-15T16:51:50+02:00 Differentiation in logical form Edalat, A Maleki, M Reykjavik, Iceland 2017-03-22 http://hdl.handle.net/10044/1/45827 unknown ACM / IEEE This paper is embargoed until publication. 10000-01-01 Logic in Computer Science (LICS 2017) Conference Paper 2017 ftimperialcol 2018-09-16T05:58:48Z We introduce a logical theory of differentiation for a real-valued function on a finite dimensional real Euclidean space. A real-valued continuous function is represented by a localic ap- proximable mapping between two semi-strong proximity lattices, representing the two stably locally compact Euclidean spaces for the domain and the range of the function. Similarly, the Clarke subgradient, equivalently the L-derivative, of a locally Lipschitz map, which is non-empty, compact and convex valued, is repre- sented by an approximable mapping. Approximable mappings of the latter type form a bounded complete domain isomorphic with the function space of Scott continuous functions of a real variable into the domain of non-empty compact and convex subsets of the finite dimensional Euclidean space partially ordered with reverse inclusion. Corresponding to the notion of a single-tie of a locally Lipschitz function, used to derive the domain-theoretic L-derivative of the function, we introduce the dual notion of a single-knot of approximable mappings which gives rise to Lipschitzian approximable mappings. We then develop the notion of a strong single-tie and that of a strong knot leading to a Stone duality result for locally Lipschitz maps and Lipschitzian approximable mappings. The strong single-knots, in which a Lipschitzian approximable mapping belongs, are employed to define the Lipschitzian derivative of the approximable mapping. The latter is dual to the Clarke subgradient of the corresponding locally Lipschitz map defined domain-theoretically using strong single-ties. A stricter notion of strong single-knots is subsequently developed which captures approximable mappings of continu- ously differentiable maps providing a gradient Stone duality for these maps. Finally, we derive a calculus for Lipschitzian derivative of approximable mapping for some basic constructors and show that it is dual to the calculus satisfied by the Clarke subgradient Conference Object Iceland Imperial College London: Spiral |
institution |
Open Polar |
collection |
Imperial College London: Spiral |
op_collection_id |
ftimperialcol |
language |
unknown |
description |
We introduce a logical theory of differentiation for a real-valued function on a finite dimensional real Euclidean space. A real-valued continuous function is represented by a localic ap- proximable mapping between two semi-strong proximity lattices, representing the two stably locally compact Euclidean spaces for the domain and the range of the function. Similarly, the Clarke subgradient, equivalently the L-derivative, of a locally Lipschitz map, which is non-empty, compact and convex valued, is repre- sented by an approximable mapping. Approximable mappings of the latter type form a bounded complete domain isomorphic with the function space of Scott continuous functions of a real variable into the domain of non-empty compact and convex subsets of the finite dimensional Euclidean space partially ordered with reverse inclusion. Corresponding to the notion of a single-tie of a locally Lipschitz function, used to derive the domain-theoretic L-derivative of the function, we introduce the dual notion of a single-knot of approximable mappings which gives rise to Lipschitzian approximable mappings. We then develop the notion of a strong single-tie and that of a strong knot leading to a Stone duality result for locally Lipschitz maps and Lipschitzian approximable mappings. The strong single-knots, in which a Lipschitzian approximable mapping belongs, are employed to define the Lipschitzian derivative of the approximable mapping. The latter is dual to the Clarke subgradient of the corresponding locally Lipschitz map defined domain-theoretically using strong single-ties. A stricter notion of strong single-knots is subsequently developed which captures approximable mappings of continu- ously differentiable maps providing a gradient Stone duality for these maps. Finally, we derive a calculus for Lipschitzian derivative of approximable mapping for some basic constructors and show that it is dual to the calculus satisfied by the Clarke subgradient |
format |
Conference Object |
author |
Edalat, A Maleki, M |
spellingShingle |
Edalat, A Maleki, M Differentiation in logical form |
author_facet |
Edalat, A Maleki, M |
author_sort |
Edalat, A |
title |
Differentiation in logical form |
title_short |
Differentiation in logical form |
title_full |
Differentiation in logical form |
title_fullStr |
Differentiation in logical form |
title_full_unstemmed |
Differentiation in logical form |
title_sort |
differentiation in logical form |
publisher |
ACM / IEEE |
publishDate |
2017 |
url |
http://hdl.handle.net/10044/1/45827 |
op_coverage |
Reykjavik, Iceland |
genre |
Iceland |
genre_facet |
Iceland |
op_source |
Logic in Computer Science (LICS 2017) |
op_rights |
This paper is embargoed until publication. 10000-01-01 |
_version_ |
1766041946036371456 |