close

Вход

Забыли?

вход по аккаунту

код для вставкиСкачать
Domain Theory and Differential Calculus
Abbas Edalat
Imperial College
http://www.doc.ic.ac.uk/~ae
Joint work with
Andre Lieutier
Dassault Systemes
Oxford
17/2/2003
Computational Model for Classical Spaces
• A research project since 1993:
Reconstruct some basic mathematics
• Embed classical spaces into the set of
maximal elements of suitable domains
x
{x}
X
Classical Space
DX
Domain
2
Computational Model for Classical Spaces
Previous Applications:
• Fractal Geometry
• Measure & Integration Theory
• Exact Real Arithmetic
• Computational Geometry/Solid Modelling
3
Non-smooth
Smooth
Mathematics
Mathematics
•
•
•
•
•
•
Set Theory
Logic
Algebra
Point-set Topology
Graph Theory
Model Theory
.
.
•
•
•
•
•
Geometry
Differential Topology
Manifolds
Dynamical Systems
Mathematical Physics
.
.
All based on
differential calculus
4
A Domain-Theoretic Model for
Differential Calculus
•
•
•
•
•
•
Indefinite integral of a Scott continuous function
Derivative of a Scott continuous function
Fundamental Theorem of Calculus
Domain of C1 functions
(Domain of Ck functions)
Picard’s Theorem:
A data-type for differential equations
The Domain of nonempty compact Intervals of R
• (IR, ) is a bounded complete dcpo:
⊔iI ai = iI ai
• a ≪ b  ao  b
• (IR, ⊑) is -continuous:
Basis {[p,q] | p < q & p, q  Q}
• (IR, ⊑) is, thus, a continuous Scott domain.
• Scott topology has basis:
↟a = {b | a ≪ b}
x 
• x  {x} : R  IR
Topological embedding
{x}
R
IR
6
Continuous Functions
• f : [0,1]  R, f  C0[0,1], has continuous extension
If : [0,1]  IR
x
 {f (x)}
• Scott continuous maps [0,1]  IR with:
f ⊑ g  x  R . f(x) ⊑ g(x)
is another continuous Scott domain.
•
 : C0[0,1] ↪ ( [0,1]  IR), with f  If
is a topological embedding into a proper subset of
maximal elements of [0,1]  IR .
7
Step Functions
• a↘b : [0,1]  IR, with a  I[0,1], b  IR:
x 
b
x  ao

otherwise
• Finite lubs of consistent single step functions
⊔1in(ai ↘ bi)
with ai, bi rational intervals, give a basis for
[0,1]  IR
8
Step Functions-An Example
R
b3
a3
b1
b2
a1
a2
0
1
9
Refining the Step Functions
R
b3
a3
b1
a1
b2
a2
0
1
10
Operations in Interval Arithmetic
• For a = [a, a]  IR, b = [b, b]  IR,
and *  { +, –,  } we have:
a * b = { x*y | x  a, y  b }
For example:
• a + b = [ a + b, a + b]
11
The Basic Construction
• What is the indefinite integral of a single step
function a↘b ?
• Classically, 
f  { F  a | a  R}
with
F ' f
• We expect  a↘b  ([0,1]  IR)
• For what f  C1[0,1], should we have If   a↘b ?
• Intuitively, we expect f to satisfy:
 x  a . b  f ' (x)  b
o
12
Interval Derivative
• Assume f  C1[0,1], a  I[0,1], b  IR.
• Suppose x  ao . b  f (x)  b.
• We think of [b, b] as an interval derivative
for f at a.
• Note that x  ao . b  f (x)  b
iff x1, x2  ao & x1 > x2 ,
b(x1 – x2)  f(x1) – f(x2)  b(x1 – x2), i.e.
b(x1 – x2) ⊑ {f(x1) – f(x2)} = {f(x1)} – {f(x2)}
13
Definition of Interval Derivative
• f  ([0,1]  IR) has an interval derivative
b  IR at a  I[0,1] if x1, x2  ao,
b(x1 – x2) ⊑ f(x1) – f(x2).
• The tie of a with b, is
(a,b) := { f | x1,x2  ao. b(x1 – x2) ⊑ f(x1) – f(x2)}
• Proposition. For f: [0,1]  IR, we have f (a,b)
iff f(x)  Maximal (IR) for x  ao ,
and Graph(f) is
(x, f(x)) b Graph(f)
within lines of slope
b
b & b at each point
(x, f(x)), x  ao.
a
.
14
For Classical Functions
Let f  C1[0,1]; the following are equivalent:
• If  (a,b)
• x  ao . b  f (x)  b
• x1,x2 [0,1], x1,x2  ao.
b(x1 – x2) ⊑ If (x1) – If (x2)
• a↘b ⊑ If
Thus, (a,b) is our candidate for  a↘b .
15
Properties of Ties
• (a1,b1)  (a2,b2) iff a2 ⊑ a1 & b1 ⊑ b2
• ni=1 (ai,bi)   iff {ai↘bi | 1 i  n} consistent.
• iI (ai,bi)   iff
iff
J finite I
{ai↘bi | iI } consistent
iJ (ai,bi)  
• In fact, (a,b) behaves like a↘b;
we call (a,b) a single-step tie.
16
The Indefinite Integral
•  : ([0,1]  IR)  (P([0,1]  IR),  )
( P the power set)
•  a↘b := (a,b)
•  ⊔i I ai ↘ bi := iI (ai,bi)
•  is well-defined and Scott continuous.
• But unlike the classical case,  is not 1-1.
17
Example
 ([0,1/2] ↘ {0}) ⊔ ([1/2,1] ↘ {0}) ⊔ ([0,1] ↘ [0,1]) =
([0,1/2] , {0})   ([1/2,1] ↘ {0})   ([0,1] ↘ [0,1]) =
([0,1] , {0}) =
 [0,1] ↘ {0}
18
The Derivative Operator
•
d
dx
: (I[0,1]  IR)  (I[0,1]  IR)
f 
df
dx
is monotone but not continuous. Note that the
classical operator is not continuous either.
•
•
d
dx
d
(a↘b)= x . 
is not linear! For f : x  x : I[0,1]  IR
dx
d
dx
(f+g) 
df
dx
+
dg
g : x  –x : I[0,1]  IR
= x . (1 – 1) = x . 0
dx
19
The Derivative
• Definition. Given f : [0,1]  IR the derivative
of f is:
df
:
[0,1]

IR
dx
df
dx
= ⊔ {a↘b | f  (a,b) }
• Theorem. (Compare with the classical case.)
df
•
is well–defined & Scott continuous.
dx
• If f 
then
df
• f  (a,b) iff a↘b ⊑ dx
C1[0,1],
d If
 If'
dx
20
Examples
f : x  | x |: R  R
x | x |
If : x  {| x |} : R  IR
d If
: R  IR
dx
{  1} x  0

x  [  1,1] x  0
{1}
0 x

2
f : x  x sin( x
d If
1
):R  R
: R  IR
dx
x  0
 If 
x  
[  1,1] x  0
x
f : x  x sin( x
d If
1
):R  R
: R  IR
dx
 If 
x  

x  0
x  0
21
Domain of Ties, or Indefinite Integrals
• Recall  : ([0,1]  IR)  (P([0,1]  IR),  )
• Let T[0,1] = Image ( ), i.e.   T[0,1] iff
x is the nonempty intersection of a family of single ties:
 = iI  (ai,bi)  
• Domain of ties: ( T[0,1] ,  )
• Theorem. ( T[0,1] ,  ) is a continuous Scott domain.
22
The Fundamental Theorem of Calculus

• Define
d
: (T[0,1] , )  ([0,1]  IR)
dx
∆ ⊓{
df
dx
|f∆}

• Theorem.
: (T[0,1] , )  ([0,1]  IR)
d
dx

is upper adjoint to
: ([0,1]  IR)  (T[0,1] , )

In fact,
Id =
 ° dx
d

and
Id ⊑
d
dx
°
23
Fundamental Theorem of Calculus
• For f, g  C1[0,1], let f ~ g if f = g + r, for some r  R.
• We have:

x

1
C [ 0 ,1]
~
0
C [ 0 ,1]
d
dx
 g  
f 
{  x .{ g(x)}  c | c  R}
T[0,1]
 x.{f(x)}

[ 0 ,1]  IR

d
dx
24
F.T. of Calculus: Isomorphic version
• For f , g  [0,1]  IR, let f ≈ g if f = g a.e.
• We then have:

x

1
C [ 0 ,1]
~
0
C [ 0 ,1]
d
dx
 g  
f 
{  x .{ g(x)}  c | c  R}
 x.{f(x)}

T[0,1]

([ 0 ,1]  IR)/ 

d
dx
25
A Domain for C1 Functions
• If h C1[0,1] , then
( Ih , Ih )  ([0,1]  IR)  ([0,1]  IR)
• We can approximate ( Ih, Ih ) in ([0,1]  IR)2
i.e. ( f, g) ⊑ ( Ih ,Ih ) with f ⊑ Ih and g ⊑ Ih
• What pairs ( f, g)  ([0,1]  IR)2
approximate a differentiable function?
26
Function and Derivative Consistency
• Define the consistency relation:
Cons  ([0,1]  IR)  ([0,1]  IR) with
(f,g)  Cons if (f)  ( g)  
• Proposition
(f,g)  Cons iff there is a continuous h: dom(g)  R
with f ⊑ Ih and g ⊑
d Ih
dx
.
• In fact, if (f,g)  Cons, there are always a least and a
greatest functions h with the above properties.
27
Consistency for basis elements
• (⊔i ai↘bi, ⊔j cj↘dj)  Cons is a finitary property:
G(f,g)= greatest function
Approximating function:
f=
⊔i ai↘bi
fg(t)
L(f,g) = least function
t
Approximating derivative: g = ⊔j cj↘dj
• (f,g)  Cons iff L(f,g) G(f,g) . Cons is decidable on the basis.
• Up(f,g) := (fg , g) where fg : t  [ L(f,g)(t) , G(f,g)(t) ]
28
The Domain of C1 Functions
• Lemma. Cons  ([0,1]  IR)2 is Scott closed.
• Theorem.
D1 [0,1]:= { (f,g)  ([0,1]IR)2 | (f,g)  Cons}is a continuous
Scott domain, which can be given an effective structure.
•
Define
D1c := {(f0,f1)  C1C0 | f0 = f1 }
• Theorem.
 : C1[0,1]  C0[0,1]  ([0,1]  IR)2
restricts to give a topological embedding
D1c
↪
D1
(with C1 norm)
(with Scott topology)
29
Higher Interval Derivative
• Let 1(a,b) = (a,b)
• Definition. (the second tie)
df
2
f   (a,b)  P([0,1]  IR) if
 1(a,b)
dx
• Note the recursive definition, which can be
extended to higher derivatives.
• Proposition. For f  C2[0,1], the following are
equivalent:
• If  2(a,b)
• x  a0. b  f (x)  b
• x1,x2 a0. b (x1 – x2) ⊑ If (x1) – If (x2)
30
• a↘b ⊑ If
Higher Derivative and Indefinite Integral
• For f : [0,1]  IR we define:
2
d f
dx
2
: [0,1]  IR by
• Then
2
d f
dx
2
2
d f
dx
2

d
df
dx dx
= ⊔f   (a,b) a↘b
2
(2)
•  : ([0,1]  IR)  (P([0,1]  IR),  )
(2)
•  a↘b :=  2(a,b)
(2)
•  ⊔i I ai ↘ bi := iI  (ai,bi)
2
(2)
•  is well-defined and Scott continuous.
31
Domains of C 2 functions
(2)
• Define Cons (f0,f1,f2) iff f0   f1   f2 
Theorem. Cons (f0,f1,f2) is decidable on basis elements.
(The present algorithm to check is NP-hard.)
• D2 := { (f0,f1,f2)  (I[0,1]IR)3 | Cons (f0,f1,f2) }
• D2c := {(f0,f1,f2)  C2C1C0 | f0 = f1, f1 = f2}
• Theorem.  restricts to give a topological
embedding D2c ↪ D2
32
Domains of C k functions
• Let (fi)0ik  (I[0,1]IR)k+1
(i)
Define Cons (fi)0ik iff  0ik  fi  
• The decidability of Cons on basis elements for k  3 is an
open question.
• Dk := { (fi)0ik  (I[0,1]IR)k+1 | Cons (fi)0ik }
• D∞:= { (fk)k0 ( I[0,1]IR)ω |  k0. (fi)0ik  Dk }
33
Picard’s Theorem
•
dx
dt
with F: R2  R
= F(t,x)
with (t0,x0) R2
x(t0) = x0
where F is Lipschitz in x uniformly in t for some
neighbourhood of (t0,x0).
• Theorem. There exists a neighbourhood of t0 where
there is a unique solution, the fixed point of:
P: C0 [t0-k , t0+k] 
C0 [t0-k , t0+k]
f
for some k>0 .

t
t . (x0 +  F(t , f(t) ) dt)
t0
34
Picard’s Solution Reformulated
•
t
P: f  t . (x0 +  t0 F(t , f(t)) dt)
can be considered as upgrading the information
about the function f and the information about its
derivative g.
•
•
ApF:
(f,g)  (f , t. F(t,f(t)))
Up: (f,g)  ( t . (x0 +
t
t0 g(t)
dt) , g )
t
• Up⃘ApF: (f,g)  (t . (x0 +  gt0 dt , t . F(t,f(t)))
has a fixed point (f,g) with f = g = t . F(t,f(t))
35
A domain-theoretic Picard’s theorem
• We now have the basic framework to obtain
Picard’s theorem with domain theory.
• However, we have to make sure that derivative
updating preserves consistency.
• Say (f , g) is strongly consistent, (f , g) S-Cons, if
 h ⊒ g. (f , h)  Cons
• On basis elements, strong consistency is decidable.
36
A domain-theoretic Picard’s theorem
• Let F : [0,1]  IR  IR and
ApF : ([0,1]  IR)2 
([0,1]  IR)2
(f,g)
 ( f , F (. , f ) )
Up : ([0,1]  IR)2 
([0,1]  IR)2
Up(f,g) = (fg , g) where fg (t) = [ L (f,g) (t) , G (f,g) (t) ]
• Consider any initial value f  [0,1]  IR with
(f, F (. , f ) )  S-Cons
• Then the continuous map P = Up ⃘ ApF has a least fixed
point above (f, F (. , f ))
• Theorem. If F = Ih for a map h : [0,1]  R  R which
satisfies the Lipschitz property of Picard’s theorem, then the
domain-theoretic solution coincides with the classical solution.
37
Example
f
We solve:
dx
= F(t,x), x(t0) =x0
dt
for t [0,1] with
F(t,x) = t and t0=1/2, x0=9/8.
b1 b2 b3
1
F is approximated by a
sequence of step
functions, F1, F2, …
.
aa3
2
a1
1
g
1
t
The initial condition is
approximated by
rectangles aibi:
F1
F2
F3
F = ⊔i Fi
{(1/2,9/8)} =
F
1
t
⊔i aibi,
38
Solution
f
At each stage we
find Li and Gi
1
.
1
g
1
1
39
Solution
f
At each stage we
find Li and Gi
1
.
1
g
1
1
40
Solution
f
At each stage we
find Li and Gi
1
.
1
g
1
1
Li and Gi tend to
the exact solution:
f: t  t2/2 + 1
41
Further Work
•
•
•
•
Solving Differential Equations with Domains
Differential Calculus with Several Variables
Implicit and Inverse Function Theorems
Reconstruct Geometry and Smooth Mathematics
with Domain Theory
• Continuous processes, robotics,…
42
THE END
http://www.doc.ic.ac.uk/~ae
43
44
Higher Interval Derivative
• Let 1(a,b) = (a,b)
• Definition. (the second tie)
df
2
f   (a,b)  P(I[0,1]  IR) if
 1(a,b)
dx
• Note the recursive definition, which can be
extended to higher derivatives.
• Proposition. For f  C2[0,1], the following are
equivalent:
• If  2(a,b)
• x  a0. b  f (x)  b
• x1,x2 ≫ a. b (x1 – x2) ⊑ If (x1) – If (x2)
45
• a↘b ⊑ If
Higher Interval Derivative
• For f : I[0,1]  IR we define:
2
d f
dx
2
: I[0,1]  IR by
• Then
2
d f
dx
2
2
d f
dx
2

d
df
dx dx
= ⊔f   (a,b) a↘b
2
(2)
•  : (I[0,1]  IR)  (P(I[0,1]  IR),  )
(2)
•  a↘b :=  2(a,b)
46
Domains of C 2and C k functions
(2)
• D2 := { (f0,f1,f2)  (I[0,1]IR)3 | f0   f1   f2  }
• D2c := {(f0,f1,f2)  C2C1C0 | f0 = f1, f1 = f2}
• Theorem.  restricts to give a
topological embedding D2c ↪ D2
•
Dk :=
{ (fi)0ik 
(I[0,1]IR)k+1
(i)
|  0ik  fi   }
• D∞:= { (fk)k0 ( I[0,1]IR) |  k0. fk  Dk }
47
Consistency Test for (f,g)
• For x  Dom(g), let g({x})=[g (x),g+(x)] where
g ,g+: Dom(g) R are semi-continuous functions.
Similarly we define f , f+: Dom(f) R.
• Let O be a connected component of Dom(g) with
O  Dom(f)  . For x , y  O define:
x 
  g ( u ) du
y


d
( x, y )  
x
 g  ( u ) du


y

y  x


 d
x  y



x 
  g ( u ) du
y


( x, y )  
x
 g  ( u ) du


y

y  x



x  y



• Also define: L(x) := supyODom(f)(f –(y) + d–+(x,y))
and
G(x) := infyODom(f)(f +(y) + d+–(x,y))
48
Consistency Test
• Theorem. (f, g)  Con iff x  O. L(x)  G(x).
For (f, g) = (⊔1in ai↘bi, ⊔1jm cj↘dj)
the rational end–points of ai and cj induce a
partition X = {x0 < x1 < x2 < … < xk} of O.
• Proposition. For arbitrary x  O, there is
p, where 0  p  k, with:
L(x) = f –(xp) + d–+(x,xp).
• Similarly for G(x).
49
1/--страниц
Пожаловаться на содержимое документа