Differentiation in logical form
File(s)DTRS17-6.pdf (383.87 KB)
Published version
Author(s)
Edalat, Abbas
Maleki, Mehrdad
Type
Report
Abstract
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 approximable
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 represented
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 continuously
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.
real-valued function on a finite dimensional real Euclidean space.
A real-valued continuous function is represented by a localic approximable
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 represented
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 continuously
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.
Date Issued
2017-01-01
Citation
Departmental Technical Report: 17/6, 2017, pp.1-16
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
16
Journal / Book Title
Departmental Technical Report: 17/6
Copyright Statement
© 2017 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
17/6