Differentiation in logical form
File(s)lics-17-submit-without-app.pdf (344.49 KB)
Accepted version
Author(s)
Edalat, A
Maleki, M
Type
Conference Paper
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 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
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
Date Issued
2017-08-18
Date Acceptance
2017-03-22
Citation
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2017
Publisher
ACM / IEEE
Journal / Book Title
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Copyright Statement
© 2017 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Source
Logic in Computer Science (LICS 2017)
Subjects
Science & Technology
Technology
Computer Science, Theory & Methods
Logic
Computer Science
Science & Technology - Other Topics
Publication Status
Published
Start Date
2017-06-20
Finish Date
2017-06-23
Coverage Spatial
Reykjavik, Iceland
Date Publish Online
2017-08-18