Automating Elementary Interpretations
Harald Zankl
Sarah Winkler
Aart Middeldorp
University of Innsbruck, Austria
WST
July 17–18, 2014
Example (Addition)
x +0→x
x + s(y ) → s(x + y )
HZ SW AM (UIBK)
FBI
2/15
Example (Addition)
x +0→x
x + s(y ) → s(x + y )
0N = 1
sN (x) = x + 1
x +N y = x + 2y
Theorem
A TRS is terminating if it is compatible with a well-founded monotone algebra.
HZ SW AM (UIBK)
FBI
2/15
Example (Addition)
x +0→x
x + s(y ) → s(x + y )
0N = 1
sN (x) = x + 1
x +2>x
x + 2y + 2 > x + 2y + 1
x +N y = x + 2y
Theorem
A TRS is terminating if it is compatible with a well-founded monotone algebra.
HZ SW AM (UIBK)
FBI
2/15
Example (Multiplication)
x +0→x
x + s(y ) → s(x + y )
x +2>x
x + 2y + 2 > x + 2y + 1
0·x →0
s(x) · y → x · y + y
0N = 1
sN (x) = x + 1
x +N y = x + 2y
Theorem
A TRS is terminating if it is compatible with a well-founded monotone algebra.
HZ SW AM (UIBK)
FBI
2/15
Example (Multiplication)
x +0→x
x + s(y ) → s(x + y )
x +2>x
x + 2y + 2 > x + 2y + 1
0·x →0
s(x) · y → x · y + y
0N = 1
sN (x) = x + 1
x +N y = x + 2y
x ·N y = 2xy + 2x + y
Theorem
A TRS is terminating if it is compatible with a well-founded monotone algebra.
HZ SW AM (UIBK)
FBI
2/15
Example (Multiplication)
x +0→x
x + s(y ) → s(x + y )
0·x →0
s(x) · y → x · y + y
0N = 1
sN (x) = x + 1
x +2>x
x + 2y + 2 > x + 2y + 1
3x + 2 > 1
2xy + 2x + 3y + 2 > 2xy + 2x + 3y
x +N y = x + 2y
x ·N y = 2xy + 2x + y
Theorem
A TRS is terminating if it is compatible with a well-founded monotone algebra.
HZ SW AM (UIBK)
FBI
2/15
Example (Factorial)
x +0→x
x + s(y ) → s(x + y )
0·x →0
s(x) · y → x · y + y
x +2>x
x + 2y + 2 > x + 2y + 1
3x + 2 > 1
2xy + 2x + 3y + 2 > 2xy + 2x + 3y
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
0N = 1
sN (x) = x + 1
x +N y = x + 2y
x ·N y = 2xy + 2x + y
Theorem
A TRS is terminating if it is compatible with a well-founded monotone algebra.
HZ SW AM (UIBK)
FBI
2/15
Example (Factorial)
x +0→x
x +2>x
x + s(y ) → s(x + y )
x + 2y + 2 > x + 2y + 1
0·x →0
s(x) · y → x · y + y
3x + 2 > 1
2xy + 2x + 3y + 2 > 2xy + 2x + 3y
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
0N = 1
sN (x) = x + 1
x +N y = x + 2y
factN (x) = (2x + 2)
x ·N y = 2xy + 2x + y
2x+1
Theorem
A TRS is terminating if it is compatible with a well-founded monotone algebra.
HZ SW AM (UIBK)
FBI
2/15
Example (Factorial)
x +0→x
x +2>x
x + s(y ) → s(x + y )
x + 2y + 2 > x + 2y + 1
0·x →0
s(x) · y → x · y + y
3x + 2 > 1
2xy + 2x + 3y + 2 > 2xy + 2x + 3y
43 > 2
fact(0) → s(0)
(2x + 4)2x+3 > (2x + 3)(2x + 2)2x+1 + 2x + 2
fact(s(x)) → s(x) · fact(x)
0N = 1
sN (x) = x + 1
x +N y = x + 2y
factN (x) = (2x + 2)
x ·N y = 2xy + 2x + y
2x+1
Theorem
A TRS is terminating if it is compatible with a well-founded monotone algebra.
HZ SW AM (UIBK)
FBI
2/15
Example (Factorial)
x +0→x
?>?
x + s(y ) → s(x + y )
?>?
0·x →0
?>?
s(x) · y → x · y + y
?>?
fact(0) → s(0)
?>?
fact(s(x)) → s(x) · fact(x)
0N = ?
sN (x) = ?
?>?
x +N y = ?
x ·N y = ?
factN (x) = ?
Theorem
A TRS is terminating if it is compatible with a well-founded monotone algebra.
HZ SW AM (UIBK)
FBI
2/15
Overview
History
Encoding
Implementation
Conclusion
HZ SW AM (UIBK)
FBI
3/15
History
Why elementary interpretations?
Some history
method
polynomials
HZ SW AM (UIBK)
theory
Lankford’79
implementation
FBI
4/15
History
Why elementary interpretations?
Some history
method
polynomials
HZ SW AM (UIBK)
theory
Lankford’79
implementation
Contejean et al.’05, Fuhs et al.’07
FBI
4/15
History
Why elementary interpretations?
Some history
method
polynomials
theory
Lankford’79
implementation
Contejean et al.’05, Fuhs et al.’07
ordinals
HZ SW AM (UIBK)
FBI
4/15
History
Why elementary interpretations?
Some history
method
polynomials
theory
Lankford’79
ordinals
Touzet’98
HZ SW AM (UIBK)
implementation
Contejean et al.’05, Fuhs et al.’07
FBI
4/15
History
Why elementary interpretations?
Some history
method
polynomials
theory
Lankford’79
implementation
Contejean et al.’05, Fuhs et al.’07
ordinals
Touzet’98
Winkler et al.’13
HZ SW AM (UIBK)
FBI
4/15
History
Why elementary interpretations?
Some history
method
polynomials
theory
Lankford’79
implementation
Contejean et al.’05, Fuhs et al.’07
Touzet’98
Winkler et al.’13
elementary functions
ordinals
HZ SW AM (UIBK)
FBI
4/15
History
Why elementary interpretations?
Some history
method
polynomials
elementary functions
ordinals
HZ SW AM (UIBK)
theory
Lankford’79
Lescanne’95
implementation
Contejean et al.’05, Fuhs et al.’07
Touzet’98
Winkler et al.’13
FBI
4/15
History
Why elementary interpretations?
Some history
method
polynomials
elementary functions
ordinals
HZ SW AM (UIBK)
theory
Lankford’79
Lescanne’95
implementation
Contejean et al.’05, Fuhs et al.’07
Touzet’98
Winkler et al.’13
7
FBI
4/15
History
Why elementary interpretations?
Some history
method
polynomials
elementary functions
ordinals
HZ SW AM (UIBK)
theory
Lankford’79
Lescanne’95
Lucas’09
Touzet’98
implementation
Contejean et al.’05, Fuhs et al.’07
7
Winkler et al.’13
FBI
4/15
History
Why elementary interpretations?
Some history
method
polynomials
elementary functions
ordinals
HZ SW AM (UIBK)
theory
Lankford’79
Lescanne’95
Lucas’09
Touzet’98
implementation
Contejean et al.’05, Fuhs et al.’07
7
7
Winkler et al.’13
FBI
4/15
History
Why elementary interpretations?
Some history
method
polynomials
elementary functions
ordinals
theory
Lankford’79
Lescanne’95
Lucas’09
Touzet’98
implementation
Contejean et al.’05, Fuhs et al.’07
7
7
Winkler et al.’13
RTA List of open problems #28
(Lescanne, 1991)
Develop effective methods to decide whether a system decreases with
respect to some exponential interpretation.
HZ SW AM (UIBK)
FBI
4/15
History
Why elementary interpretations?
Some history
method
polynomials
elementary functions
ordinals
theory
Lankford’79
Lescanne’95
Lucas’09
Touzet’98
implementation
Contejean et al.’05, Fuhs et al.’07
7
7
Winkler et al.’13
RTA List of open problems #28
(Lescanne, 1991)
Develop effective methods to decide whether a system decreases with
respect to some exponential interpretation.
Which functions
+, ·, 2x
HZ SW AM (UIBK)
3
x 2 , xy , y x
?
FBI
sin(x), log(x),
√
n
m
7
4/15
History
Which shape?
Linear elementary interpretation (LEI)
• f (~
x ) = p(~x ) + b(~x )q(~x )
proposed by Lucas’09
p(~x ), b(~x ), q(~x ) linear functions
HZ SW AM (UIBK)
FBI
5/15
History
Which shape?
Linear elementary interpretation (LEI)
• f (~
x ) = p(~x ) + b(~x )q(~x )
proposed by Lucas’09
p(~x ), b(~x ), q(~x ) linear functions
x + 2y , x + y 2 , y 3x
HZ SW AM (UIBK)
3
xy , 2x y , 2x 3
FBI
7
5/15
History
Which shape?
Linear elementary interpretation (LEI)
• f (~
x ) = p(~x ) + b(~x )q(~x )
proposed by Lucas’09
p(~x ), b(~x ), q(~x ) linear functions
x + 2y , x + y 2 , y 3x
3
xy , 2x y , 2x 3
7
Example (Factorial)
x +0→x
x + s(y ) → s(x + y )
HZ SW AM (UIBK)
0·x →0
s(x) · y → x · y + y
FBI
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
5/15
History
Which shape?
Linear elementary interpretation (LEI)
• f (~
x ) = p(~x ) + b(~x )q(~x )
proposed by Lucas’09
p(~x ), b(~x ), q(~x ) linear functions
x + 2y , x + y 2 , y 3x
3
xy , 2x y , 2x 3
7
Example (Factorial)
x +0→x
x + s(y ) → s(x + y )
0N = 1
x ·N y = 2xy + 2x + y
HZ SW AM (UIBK)
0·x →0
s(x) · y → x · y + y
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
sN (x) = x + 1
factN (x) = (2x + 2)
FBI
x +N y = x + 2y
2x+1
5/15
History
Which shape?
Linear elementary interpretation (LEI)
• f (~
x ) = p(~x ) + b(~x )q(~x )
proposed by Lucas’09
p(~x ), b(~x ), q(~x ) linear functions
x + 2y , x + y 2 , y 3x
3
xy , 2x y , 2x 3
7
Example (Factorial)
x +0→x
x + s(y ) → s(x + y )
0N = 1
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
sN (x) = x + 1
x ·N y = 2xy + 2x + y
2>0
3x + 2 > 1
2>1
y +2>0
HZ SW AM (UIBK)
0·x →0
s(x) · y → x · y + y
factN (x) = (2x + 2)
x +N y = x + 2y
2x+1
43 > 2
(2x + 3)2x+3 > (2x + 3)(2x + 2)2x+1 + 2x + 2
FBI
5/15
History
Which shape?
Linear elementary interpretation (LEI)
• f (~
x ) = p(~x ) + b(~x )q(~x )
proposed by Lucas’09
p(~x ), b(~x ), q(~x ) linear functions
x + 2y , x + y 2 , y 3x
3
xy , 2x y , 2x 3
7
Example (Factorial)
x +0→x
x + s(y ) → s(x + y )
0N = 1
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
sN (x) = x + 1
x ·N y = 2xy + 2x + y
2>0
3x + 2 > 1
2>1
y +2>0
HZ SW AM (UIBK)
0·x →0
s(x) · y → x · y + y
factN (x) = (2x + 2)
x +N y = x + 2y
2x+1
43 > 2
(2x + 3)2x+3 > (2x + 3)(2x + 2)2x+1 + 2x + 2
FBI
5/15
History
Which shape?
Linear elementary interpretation (LEI)
• f (~
x ) = p(~x ) + b(~x )q(~x )
proposed by Lucas’09
p(~x ), b(~x ), q(~x ) linear functions
x + 2y , x + y 2 , y 3x
3
xy , 2x y , 2x 3
7
Example (Factorial)
x +0→x
x + s(y ) → s(x + y )
0N = 1
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
sN (x) = x + 1
x ·N y = 2xy + 2x + y
2>0
3x + 2 > 1
2>1
y +2>0
HZ SW AM (UIBK)
0·x →0
s(x) · y → x · y + y
factN (x) = (2x + 2)
x +N y = x + 2y
2x+1
43 > 2
(2x + 3)2x+3 > (2x + 3)(2x + 2)2x+1 + 2x + 2
FBI
5/15
History
Which shape? (cont’d)
Fixed base elementary interpretations (FBI)
0
• f (~
x ) = p(~x ) + b f (~x ) · q(~x )
this work
p(~x ), q(~x ) linear function, b ∈ N>2 ,
HZ SW AM (UIBK)
FBI
f 0 (~x )
FBI
6/15
History
Which shape? (cont’d)
Fixed base elementary interpretations (FBI)
0
• f (~
x ) = p(~x ) + b f (~x ) · q(~x )
this work
p(~x ), q(~x ) linear function, b ∈ N>2 ,
x+
2y ,
HZ SW AM (UIBK)
2x 3,
2x y
3
f 0 (~x )
xy , x +
FBI
FBI
y 2,
y 3x
7
6/15
History
Which shape? (cont’d)
Fixed base elementary interpretations (FBI)
0
• f (~
x ) = p(~x ) + b f (~x ) · q(~x )
this work
p(~x ), q(~x ) linear function, b ∈ N>2 ,
x+
2y ,
2x 3,
2x y
3
f 0 (~x )
xy , x +
FBI
y 2,
y 3x
7
Example (Factorial)
x +0→x
x + s(y ) → s(x + y )
HZ SW AM (UIBK)
0·x →0
s(x) · y → x · y + y
FBI
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
6/15
History
Which shape? (cont’d)
Fixed base elementary interpretations (FBI)
0
• f (~
x ) = p(~x ) + b f (~x ) · q(~x )
this work
p(~x ), q(~x ) linear function, b ∈ N>2 ,
x+
2y ,
2x 3,
2x y
3
f 0 (~x )
xy , x +
FBI
y 2,
y 3x
7
Example (Factorial)
x +0→x
0·x →0
fact(0) → s(0)
x + s(y ) → s(x + y )
s(x) · y → x · y + y
0N = 2
sN (x) = x + 2
x ·N y = 2x y
HZ SW AM (UIBK)
fact(s(x)) → s(x) · fact(x)
x +N y = 2x + y + 1
x
factN (x) = 22
FBI
6/15
History
Which shape? (cont’d)
Fixed base elementary interpretations (FBI)
0
• f (~
x ) = p(~x ) + b f (~x ) · q(~x )
this work
p(~x ), q(~x ) linear function, b ∈ N>2 ,
x+
2y ,
2x 3,
2x y
3
f 0 (~x )
xy , x +
FBI
y 2,
y 3x
7
Example (Factorial)
x +0→x
0·x →0
fact(0) → s(0)
x + s(y ) → s(x + y )
s(x) · y → x · y + y
0N = 2
sN (x) = x + 2
x ·N y = 2x y
x +N y = 2x + y + 1
x
factN (x) = 22
x +5>x
2x + y + 5 > 2x + y + 3
HZ SW AM (UIBK)
fact(s(x)) → s(x) · fact(x)
4x > 2
2x+2 y > 2x+1 y + y + 1
FBI
2
22 > 4
x+2
22
x
> 2x+2 22
6/15
History
Which shape? (cont’d)
Fixed base elementary interpretations (FBI)
0
• f (~
x ) = p(~x ) + b f (~x ) · q(~x )
this work
p(~x ), q(~x ) linear function, b ∈ N>2 ,
x+
2y ,
2x 3,
2x y
3
f 0 (~x )
xy , x +
FBI
y 2,
y 3x
7
Example (Factorial)
x +0→x
0·x →0
fact(0) → s(0)
x + s(y ) → s(x + y )
s(x) · y → x · y + y
0N = 2
sN (x) = x + 2
x ·N y = 2x y
x +N y = 2x + y + 1
x
factN (x) = 22
x +5>x
2x + y + 5 > 2x + y + 3
HZ SW AM (UIBK)
fact(s(x)) → s(x) · fact(x)
4x > 2
2x+2 y > 2x+1 y + y + 1
FBI
2
22 > 4
x+2
22
x
> 2x+2 22
6/15
History
Which shape? (cont’d)
Fixed base elementary interpretations (FBI)
0
• f (~
x ) = p(~x ) + b f (~x ) · q(~x )
this work
p(~x ), q(~x ) linear function, b ∈ N>2 ,
x+
2y ,
2x 3,
2x y
3
f 0 (~x )
xy , x +
FBI
y 2,
y 3x
7
Example (Factorial)
x +0→x
0·x →0
fact(0) → s(0)
x + s(y ) → s(x + y )
s(x) · y → x · y + y
0N = 2
sN (x) = x + 2
x ·N y = 2x y
x +N y = 2x + y + 1
x
factN (x) = 22
x +5>x
2x + y + 5 > 2x + y + 3
HZ SW AM (UIBK)
fact(s(x)) → s(x) · fact(x)
4x > 2
2x+2 y > 2x+1 y + y + 1
FBI
2
22 > 4
x+2
22
x
> 22
+x+2
6/15
Encoding
FBIs - General idea
f (~x ) =
X
16i6n
HZ SW AM (UIBK)
xi fi + f0 + b f
0 (~
x)
(
X
xi f˙i + f˙0 )
16i6n
FBI
7/15
Encoding
FBIs - General idea
f (~x ) =
X
xi fi + f0 + b f
0 (~
x)
16i6n
with f0 , . . . , fn , f˙0 , . . . , f˙n ∈ N and
HZ SW AM (UIBK)
(
X
xi f˙i + f˙0 )
16i6n
f 0 (x)
FBI
an FBI
7/15
Encoding
FBIs - General idea
f (~x ) =
X
xi fi + f0 + b f
0 (~
x)
16i6n
with f0 , . . . , fn , f˙0 , . . . , f˙n ∈ N and
HZ SW AM (UIBK)
(
X
xi f˙i + f˙0 )
16i6n
f 0 (x)
FBI
an FBI
7/15
Encoding
FBIs - General idea
f (~x ) =
X
xi fi + f0 + b f
0 (~
x)
16i6n
with f0 , . . . , fn , f˙0 , . . . , f˙n ∈ N and
HZ SW AM (UIBK)
(
X
0
xi f˙i + f˙0 ) = f (~x ) + b f (x) f˙(~x )
16i6n
f 0 (x)
FBI
an FBI
7/15
Encoding
FBIs - General idea
f (~x ) =
X
xi fi + f0 + b f
0 (~
x)
(
16i6n
X
0
xi f˙i + f˙0 ) = f (~x ) + b f (x) f˙(~x )
16i6n
with f0 , . . . , fn , f˙0 , . . . , f˙n ∈ N and
f 0 (x)
an FBI
Problem (FBIs not closed under typical operations)
• addition: 2x + 2y
• multiplication:
7
2x (x
• composition: (x +
+ 2y ) = 2x x + 2x+y
2x x)
◦
2x
=
2x
+
7
x
2 2 2x
• scalar multiplication: (x + 2x y )4 = 4x + 2x 4y
HZ SW AM (UIBK)
FBI
x +x
= 2x + 22
7
3
7/15
Encoding
FBIs - General idea
f (~x ) =
X
xi fi + f0 + b f
0 (~
x)
(
16i6n
X
0
xi f˙i + f˙0 ) = f (~x ) + b f (x) f˙(~x )
16i6n
with f0 , . . . , fn , f˙0 , . . . , f˙n ∈ N and
f 0 (x)
an FBI
Problem (FBIs not closed under typical operations)
• addition: 2x + 2y
• multiplication:
7
2x (x
• composition: (x +
+ 2y ) = 2x x + 2x+y
2x x)
◦
2x
=
2x
+
7
x
2 2 2x
x +x
= 2x + 22
• scalar multiplication: (x + 2x y )4 = 4x + 2x 4y
7
3
Solution
• use approximations
ν
• if [α]µ
N (`) > [α]N (r ) for all ` → r ∈ R then R is terminating
HZ SW AM (UIBK)
FBI
7/15
Encoding
Desired properties
X
f (~x ) =
xi fi + f0 + b f
16i6n
0 (~
x)
(
X
xi f˙i + f˙0 ) = f (~x ) + b f
0 (~
x)
f˙(~x )
16i6n
Monotonicity
mon(f ) :=
HZ SW AM (UIBK)
V
16i6n
fi > 0 ∨ f˙i > 0 ∨ (f˙(~x ) > 0 ∧ mon(f 0 (~x ))
FBI
8/15
Encoding
Desired properties
X
f (~x ) =
xi fi + f0 + b f
16i6n
0 (~
x)
(
X
xi f˙i + f˙0 ) = f (~x ) + b f
0 (~
x)
f˙(~x )
16i6n
Monotonicity
mon(f ) :=
V
16i6n
fi > 0 ∨ f˙i > 0 ∨ (f˙(~x ) > 0 ∧ mon(f 0 (~x ))
Well-definedness (N>1 )
wd(f ) := [f (~x ) > 1]
HZ SW AM (UIBK)
FBI
8/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
16i6n
0
(~
x)
(
X
xi f˙i +f˙0 )
g (~
x) =
16i6n
X
16i6n
xi gi +g0 +b g
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
f (~
x ) +µ g (~
x) =
HZ SW AM (UIBK)
FBI
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
f (~
x ) +µ g (~
x) =
(
X
xi f˙i +f˙0 )
g (~
x) =
16i6n
X
X
16i6n
xi gi +g0 +b g
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
HZ SW AM (UIBK)
FBI
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +µ g (~
x) =
X
X
g (~
x) =
16i6n
xi gi +g0 +b g
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
HZ SW AM (UIBK)
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ): min(f 0 (~
x ),g 0 (~
x ))
FBI
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +µ g (~
x) =
X
X
g (~
x) =
xi gi +g0 +b g
16i6n
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ): min(f 0 (~
x ),g 0 (~
x ))
X
xi (f˙i + g˙i ) + (f˙0 + g˙0 )
16i6n
HZ SW AM (UIBK)
FBI
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +µ g (~
x) =
X
X
g (~
x) =
xi gi +g0 +b g
16i6n
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ): min(f 0 (~
x ),g 0 (~
x ))
X
xi (f˙i + g˙i ) + (f˙0 + g˙0 )
16i6n
Example
• 2x + µ 2y 0 =
• 2x + µ 2x y =
• 2x +µ 2x+1 =
• 2x + µ 2y
HZ SW AM (UIBK)
=
FBI
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +µ g (~
x) =
X
X
g (~
x) =
xi gi +g0 +b g
16i6n
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ): min(f 0 (~
x ),g 0 (~
x ))
X
xi (f˙i + g˙i ) + (f˙0 + g˙0 )
16i6n
Example
• 2x + µ 2y 0 = 2x
• 2x + µ 2x y =
• 2x +µ 2x+1 =
• 2x + µ 2y
HZ SW AM (UIBK)
=
FBI
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +µ g (~
x) =
X
X
g (~
x) =
xi gi +g0 +b g
16i6n
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ): min(f 0 (~
x ),g 0 (~
x ))
X
xi (f˙i + g˙i ) + (f˙0 + g˙0 )
16i6n
Example
• 2x + µ 2y 0 = 2x
• 2x +µ 2x y = 2x (y + 1)
• 2x +µ 2x+1 =
• 2x + µ 2y
HZ SW AM (UIBK)
=
FBI
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +µ g (~
x) =
X
X
g (~
x) =
xi gi +g0 +b g
16i6n
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ): min(f 0 (~
x ),g 0 (~
x ))
X
xi (f˙i + g˙i ) + (f˙0 + g˙0 )
16i6n
Example
• 2x + µ 2y 0 = 2x
• 2x +µ 2x y = 2x (y + 1)
• 2x +µ 2x+1 = 2x 2 ≡ 2x+1
• 2x + µ 2y =
HZ SW AM (UIBK)
FBI
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +µ g (~
x) =
X
X
g (~
x) =
xi gi +g0 +b g
16i6n
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ): min(f 0 (~
x ),g 0 (~
x ))
X
xi (f˙i + g˙i ) + (f˙0 + g˙0 )
16i6n
Example
• 2x + µ 2y 0 = 2x
• 2x +µ 2x y = 2x (y + 1)
• 2x +µ 2x+1 = 2x 2 ≡ 2x+1
• 2x + µ 2y = 20
HZ SW AM (UIBK)
FBI
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +ν g (~
x) =
X
X
g (~
x) =
xi gi +g0 +b g
16i6n
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ):max(f 0 (~
x ),g 0 (~
x ))
X
xi (f˙i + g˙i ) + (f˙0 + g˙0 )
16i6n
Example
• 2x + µ 2y 0 = 2x
• 2x +µ 2x y = 2x (y + 1)
• 2x +µ 2x+1 = 2x 2 ≡ 2x+1
• 2x + µ 2y = 20
HZ SW AM (UIBK)
• 2x +ν 2y 0 =
• 2x +ν 2x y =
• 2x +ν 2x+1 =
• 2x +ν 2y
FBI
=
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +ν g (~
x) =
X
X
g (~
x) =
xi gi +g0 +b g
16i6n
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ):max(f 0 (~
x ),g 0 (~
x ))
X
xi (f˙i + g˙i ) + (f˙0 + g˙0 )
16i6n
Example
• 2x + µ 2y 0 = 2x
• 2x +µ 2x y = 2x (y + 1)
• 2x +µ 2x+1 = 2x 2 ≡ 2x+1
• 2x + µ 2y = 20
HZ SW AM (UIBK)
• 2x +ν 2y 0 = 2x
• 2x +ν 2x y =
• 2x +ν 2x+1 =
• 2x +ν 2y
FBI
=
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +ν g (~
x) =
X
X
g (~
x) =
xi gi +g0 +b g
16i6n
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ):max(f 0 (~
x ),g 0 (~
x ))
X
xi (f˙i + g˙i ) + (f˙0 + g˙0 )
16i6n
Example
• 2x + µ 2y 0 = 2x
• 2x +µ 2x y = 2x (y + 1)
• 2x +µ 2x+1 = 2x 2 ≡ 2x+1
• 2x + µ 2y = 20
HZ SW AM (UIBK)
• 2x +ν 2y 0 = 2x
• 2x +ν 2x y = 2x (y + 1)
• 2x +ν 2x+1 =
• 2x +ν 2y
FBI
=
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +ν g (~
x) =
X
X
g (~
x) =
xi gi +g0 +b g
16i6n
0
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ):max(f 0 (~
x ),g 0 (~
x ))
X
xi (f˙i + g˙i ) + (f˙0 + g˙0 )
16i6n
Example
• 2x + µ 2y 0 = 2x
• 2x +µ 2x y = 2x (y + 1)
• 2x +µ 2x+1 = 2x 2 ≡ 2x+1
• 2x + µ 2y = 20
HZ SW AM (UIBK)
• 2x +ν 2y 0 = 2x
• 2x +ν 2x y = 2x (y + 1)
• 2x +ν 2x+1 = 2x+1 2 ≡ 2x+2
• 2x +ν 2y
FBI
=
9/15
Encoding
Addition
f (~
x) =
X
xi fi +f0 +b f
0
(~
x)
16i6n
X
(
xi f˙i +f˙0 )
16i6n
f (~
x ) +ν g (~
x) =
X
X
g (~
x) =
xi gi +g0 +b g
0
16i6n
(~
x)
(
X
xi g˙i +g˙0 )
16i6n
xi (fi + gi ) + (f0 + g0 )
16i6n
˙
+ b f (~x )=0?g
0
(~
x ):g˙ (~
x )=0?f 0 (~
x ):max(f 0 (~
x ),g 0 (~
x ))
X
xi (f˙i + g˙i ) + (f˙0 + g˙0 )
16i6n
Example
• 2x + µ 2y 0 = 2x
• 2x +µ 2x y = 2x (y + 1)
• 2x +µ 2x+1 = 2x 2 ≡ 2x+1
• 2x + µ 2y = 20
HZ SW AM (UIBK)
• 2x +ν 2y 0 = 2x
• 2x +ν 2x y = 2x (y + 1)
• 2x +ν 2x+1 = 2x+1 2 ≡ 2x+2
• 2x +ν 2y
FBI
= 2x+y
9/15
Encoding
Multiplication
f (~x ) =
X
xi fi + f0 + b f
16i6n
bg
0
(~
x)
0
(~
x)
(
X
xi f˙i + f˙0 )
16i6n
·µ f (~x ) =
HZ SW AM (UIBK)
FBI
10/15
Encoding
Multiplication
f (~x ) =
X
xi fi + f0 + b f
16i6n
bg
0
(~
x)
0
(~
x)
(
X
xi f˙i + f˙0 )
16i6n
·µ f (~x ) = (f˙(~x ) = 0)
HZ SW AM (UIBK)
FBI
10/15
Encoding
Multiplication
f (~x ) =
X
xi fi + f0 + b f
0
16i6n
b
g 0 (~
x)
0
·µ f (~x ) = (f˙(~x ) = 0) ? b g (~x )
(~
x)
(
X
xi f˙i + f˙0 )
16i6n
X
xi fi + f0
16i6n
:
HZ SW AM (UIBK)
FBI
10/15
Encoding
Multiplication
f (~x ) =
X
xi fi + f0 + b f
0
16i6n
b
g 0 (~
x)
(~
x)
(
X
xi f˙i + f˙0 )
16i6n
0
·µ f (~x ) = (f˙(~x ) = 0) ? b g (~x )
X
xi fi + f0
16i6n
:
X
xi fi + f0 + b f
16i6n
HZ SW AM (UIBK)
0
(~
x )+µ g 0 (~
x)
X
xi f˙i + f˙0
16i6n
FBI
10/15
Encoding
Multiplication
f (~x ) =
X
xi fi + f0 + b f
0
16i6n
b
g 0 (~
x)
(~
x)
(
X
xi f˙i + f˙0 )
16i6n
0
·µ f (~x ) = (f˙(~x ) = 0) ? b g (~x )
X
xi fi + f0
16i6n
:
X
xi fi + f0 + b f
16i6n
0
(~
x )+µ g 0 (~
x)
X
xi f˙i + f˙0
16i6n
Example
• 2x ·µ y
x
=
y
• 2 ·µ (x + 2 z) =
• 2x ·µ (x + 2y 0) =
• 2x ·µ 2y
HZ SW AM (UIBK)
=
FBI
10/15
Encoding
Multiplication
X
f (~x ) =
xi fi + f0 + b f
0
16i6n
b
g 0 (~
x)
(~
x)
(
X
xi f˙i + f˙0 )
16i6n
0
·µ f (~x ) = (f˙(~x ) = 0) ? b g (~x )
X
xi fi + f0
16i6n
:
X
xi fi + f0 + b f
16i6n
0
(~
x )+µ g 0 (~
x)
X
xi f˙i + f˙0
16i6n
Example
• 2x ·µ y
= 2x y
• 2x ·µ (x + 2y z) =
• 2x ·µ (x + 2y 0) =
• 2x ·µ 2y
HZ SW AM (UIBK)
=
FBI
10/15
Encoding
Multiplication
X
f (~x ) =
xi fi + f0 + b f
0
16i6n
b
g 0 (~
x)
(~
x)
(
X
xi f˙i + f˙0 )
16i6n
0
·µ f (~x ) = (f˙(~x ) = 0) ? b g (~x )
X
xi fi + f0
16i6n
:
X
xi fi + f0 + b f
16i6n
0
(~
x )+µ g 0 (~
x)
X
xi f˙i + f˙0
16i6n
Example
• 2x ·µ y
= 2x y
• 2x ·µ (x + 2y z) = x + 2x+y z
• 2x ·µ (x + 2y 0) =
• 2x ·µ 2y
HZ SW AM (UIBK)
=
FBI
10/15
Encoding
Multiplication
X
f (~x ) =
xi fi + f0 + b f
0
16i6n
b
g 0 (~
x)
(~
x)
(
X
xi f˙i + f˙0 )
16i6n
0
·µ f (~x ) = (f˙(~x ) = 0) ? b g (~x )
X
xi fi + f0
16i6n
:
X
xi fi + f0 + b f
16i6n
0
(~
x )+µ g 0 (~
x)
X
xi f˙i + f˙0
16i6n
Example
• 2x ·µ y
= 2x y
• 2x ·µ (x + 2y z) = x + 2x+y z
• 2x ·µ (x + 2y 0) = 2x x
• 2x ·µ 2y
HZ SW AM (UIBK)
=
FBI
10/15
Encoding
Multiplication
X
f (~x ) =
xi fi + f0 + b f
0
16i6n
b
g 0 (~
x)
(~
x)
(
X
xi f˙i + f˙0 )
16i6n
0
·µ f (~x ) = (f˙(~x ) = 0) ? b g (~x )
X
xi fi + f0
16i6n
:
X
xi fi + f0 + b f
16i6n
0
(~
x )+µ g 0 (~
x)
X
xi f˙i + f˙0
16i6n
Example
• 2x ·µ y
= 2x y
• 2x ·µ (x + 2y z) = x + 2x+y z
• 2x ·µ (x + 2y 0) = 2x x
• 2x ·µ 2y
HZ SW AM (UIBK)
= 2x+y
FBI
10/15
Encoding
Multiplication
X
f (~x ) =
xi fi + f0 + b f
0
(~
x)
(
16i6n
b
g 0 (~
x)
X
xi f˙i + f˙0 )
16i6n
0
·ν f (~x ) = (f˙(~x ) = 0) ? b g (~x )
: bf
0
X
xi fi + f0
16i6n
(~
x )+ν g 0 (~
x)
X
xi (fi + f˙i ) + f0 + f˙0
16i6n
Example
• 2x ·µ y
x
= 2x y
y
• 2 ·µ (x + 2 z) = x + 2
• 2 x ·ν y
x+y
=
• 2x ·ν (x + 2y z) =
z
• 2x ·µ (x + 2y 0) = 2x x
• 2x ·ν (x + 2y 0) =
• 2x ·µ 2y
• 2x ·ν 2y
HZ SW AM (UIBK)
= 2x+y
FBI
=
10/15
Encoding
Multiplication
X
f (~x ) =
xi fi + f0 + b f
0
(~
x)
(
16i6n
b
g 0 (~
x)
xi f˙i + f˙0 )
16i6n
0
·ν f (~x ) = (f˙(~x ) = 0) ? b g (~x )
: bf
X
0
X
xi fi + f0
16i6n
(~
x )+ν g 0 (~
x)
X
xi (fi + f˙i ) + f0 + f˙0
16i6n
Example
• 2x ·µ y
= 2x y
• 2 x ·ν y
= 2x y
• 2x ·µ (x + 2y z) = x + 2x+y z
• 2x ·ν (x + 2y z) =
• 2x ·µ (x + 2y 0) = 2x x
• 2x ·ν (x + 2y 0) =
• 2x ·µ 2y
• 2x ·ν 2y
HZ SW AM (UIBK)
= 2x+y
FBI
=
10/15
Encoding
Multiplication
X
f (~x ) =
xi fi + f0 + b f
0
(~
x)
(
16i6n
b
g 0 (~
x)
xi f˙i + f˙0 )
16i6n
0
·ν f (~x ) = (f˙(~x ) = 0) ? b g (~x )
: bf
X
0
X
xi fi + f0
16i6n
(~
x )+ν g 0 (~
x)
X
xi (fi + f˙i ) + f0 + f˙0
16i6n
Example
• 2x ·µ y
= 2x y
• 2 x ·ν y
= 2x y
• 2x ·µ (x + 2y z) = x + 2x+y z
• 2x ·ν (x + 2y z) = 2x+y (x + z)
• 2x ·µ (x + 2y 0) = 2x x
• 2x ·ν (x + 2y 0) =
• 2x ·µ 2y
• 2x ·ν 2y
HZ SW AM (UIBK)
= 2x+y
FBI
=
10/15
Encoding
Multiplication
X
f (~x ) =
xi fi + f0 + b f
0
(~
x)
(
16i6n
b
g 0 (~
x)
xi f˙i + f˙0 )
16i6n
0
·ν f (~x ) = (f˙(~x ) = 0) ? b g (~x )
: bf
X
0
X
xi fi + f0
16i6n
(~
x )+ν g 0 (~
x)
X
xi (fi + f˙i ) + f0 + f˙0
16i6n
Example
• 2x ·µ y
= 2x y
• 2 x ·ν y
= 2x y
• 2x ·µ (x + 2y z) = x + 2x+y z
• 2x ·ν (x + 2y z) = 2x+y (x + z)
• 2x ·µ (x + 2y 0) = 2x x
• 2x ·ν (x + 2y 0) = 2x x
• 2x ·µ 2y
• 2x ·ν 2y
HZ SW AM (UIBK)
= 2x+y
FBI
=
10/15
Encoding
Multiplication
X
f (~x ) =
xi fi + f0 + b f
0
(~
x)
(
16i6n
b
g 0 (~
x)
xi f˙i + f˙0 )
16i6n
0
·ν f (~x ) = (f˙(~x ) = 0) ? b g (~x )
: bf
X
0
X
xi fi + f0
16i6n
(~
x )+ν g 0 (~
x)
X
xi (fi + f˙i ) + f0 + f˙0
16i6n
Example
• 2x ·µ y
= 2x y
• 2 x ·ν y
= 2x y
• 2x ·µ (x + 2y z) = x + 2x+y z
• 2x ·ν (x + 2y z) = 2x+y (x + z)
• 2x ·µ (x + 2y 0) = 2x x
• 2x ·ν (x + 2y 0) = 2x x
• 2x ·µ 2y
• 2x ·ν 2y
HZ SW AM (UIBK)
= 2x+y
FBI
= 2x+y
10/15
Encoding
Composition
Let f (~g )(~x ) := f (g1 (~x ), . . . , gn (~x )) and
f (~g )µ (~x ) =
f (~g )ν (~x ) =
µ
X
16i6n
ν
X
gi (~x )fi +µ f0 +µ b f
gi (~x )fi +ν f0 +ν b f
16i6n
HZ SW AM (UIBK)
Pµ
16i6n
0 (~
g )µ (~
x)
0 (~
g )ν (~
x)
hi := h1 +µ · · · +µ hn .
·µ (
·ν (
µ
X
16i6n
ν
X
gi (~x )f˙i +µ f˙0 )
gi (~x )f˙i +ν f˙0 )
16i6n
FBI
11/15
Encoding
Comparison
f (~x ) = f (~x ) + b f
0 (~
x)
f˙(~x )
g (~x ) = g (~x ) + b g
0 (~
x)
g˙ (~x )
[f (~x ) > g (~x )]
HZ SW AM (UIBK)
FBI
12/15
Encoding
Comparison
f (~x ) = f (~x ) + b f
0 (~
x)
f˙(~x )
g (~x ) = g (~x ) + b g
0 (~
x)
g˙ (~x )
[f (~x ) > g (~x )] := (g˙ (~x ) > 0 → [f 0 (~x ) > g 0 (~x )]) ∧ (À ∨ Á ∨ Â)
HZ SW AM (UIBK)
FBI
12/15
Encoding
Comparison
f (~x ) = f (~x ) + b f
0 (~
x)
f˙(~x )
g (~x ) = g (~x ) + b g
0 (~
x)
g˙ (~x )
[f (~x ) > g (~x )] := (g˙ (~x ) > 0 → [f 0 (~x ) > g 0 (~x )]) ∧ (À ∨ Á ∨ Â)
À f˙(~x ) > 0 ∧ [f 0 (~x )b > g (~x )]
HZ SW AM (UIBK)
FBI
12/15
Encoding
Comparison
f (~x ) = f (~x ) + b f
0 (~
x)
f˙(~x )
g (~x ) = g (~x ) + b g
0 (~
x)
g˙ (~x )
[f (~x ) > g (~x )] := (g˙ (~x ) > 0 → [f 0 (~x ) > g 0 (~x )]) ∧ (À ∨ Á ∨ Â)
À f˙(~x ) > 0 ∧ [f 0 (~x )b > g (~x )]
Á f (~x ) > g (~x ) ∧ f˙(~x ) > g˙ (~x )
HZ SW AM (UIBK)
FBI
12/15
Encoding
Comparison
f (~x ) = f (~x ) + b f
0 (~
x)
f˙(~x )
g (~x ) = g (~x ) + b g
0 (~
x)
g˙ (~x )
[f (~x ) > g (~x )] := (g˙ (~x ) > 0 → [f 0 (~x ) > g 0 (~x )]) ∧ (À ∨ Á ∨ Â)
À f˙(~x ) > 0 ∧ [f 0 (~x )b > g (~x )]
Á f (~x ) > g (~x ) ∧ f˙(~x ) > g˙ (~x )
0
0
 f (~x ) + bb p(~x ) cbb g (~x ) cf˙(~x ) > g (~x ) + bb g (~x ) cg˙ (~x )
∧ [f 0 (~x ) > g 0 (~x ) + p(~x )] ∧ · · ·
HZ SW AM (UIBK)
FBI
12/15
Encoding
Comparison
f (~x ) = f (~x ) + b f
0 (~
x)
f˙(~x )
g (~x ) = g (~x ) + b g
0 (~
x)
g˙ (~x )
[f (~x ) > g (~x )] := (g˙ (~x ) > 0 → [f 0 (~x ) > g 0 (~x )]) ∧ (À ∨ Á ∨ Â)
À f˙(~x ) > 0 ∧ [f 0 (~x )b > g (~x )]
Á f (~x ) > g (~x ) ∧ f˙(~x ) > g˙ (~x )
0
0
 f (~x ) + bb p(~x ) cbb g (~x ) cf˙(~x ) > g (~x ) + bb g (~x ) cg˙ (~x )
∧ [f 0 (~x ) > g 0 (~x ) + p(~x )] ∧ · · ·
˙ x ) = 0) ? 1 : b(h(~x ) + h(~
˙ x ))
bb h(~x ) c := (h(~x ) + h(~
HZ SW AM (UIBK)
FBI
12/15
Implementation
Heuristics
d limit degree of FBIs (based on call-graph)
HZ SW AM (UIBK)
FBI
13/15
Implementation
Heuristics
d limit degree of FBIs (based on call-graph)
Example (Factorial)
x +0→x
0·x →0
x + s(y ) → s(x + y )
function symbol
degree
HZ SW AM (UIBK)
0
s
s(x) · y → x · y + y
+
·
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
fact
FBI
13/15
Implementation
Heuristics
d limit degree of FBIs (based on call-graph)
Example (Factorial)
x +0→x
0·x →0
x + s(y ) → s(x + y )
function symbol
degree
HZ SW AM (UIBK)
0
0
s
s(x) · y → x · y + y
+
·
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
fact
FBI
13/15
Implementation
Heuristics
d limit degree of FBIs (based on call-graph)
Example (Factorial)
x +0→x
0·x →0
x + s(y ) → s(x + y )
function symbol
degree
HZ SW AM (UIBK)
0
0
s
0
s(x) · y → x · y + y
+
·
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
fact
FBI
13/15
Implementation
Heuristics
d limit degree of FBIs (based on call-graph)
Example (Factorial)
x +0→x
0·x →0
x + s(y ) → s(x + y )
function symbol
degree
HZ SW AM (UIBK)
0
0
s
0
s(x) · y → x · y + y
+
0
·
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
fact
FBI
13/15
Implementation
Heuristics
d limit degree of FBIs (based on call-graph)
Example (Factorial)
x +0→x
0·x →0
x + s(y ) → s(x + y )
function symbol
degree
HZ SW AM (UIBK)
0
0
s
0
s(x) · y → x · y + y
+
0
·
1
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
fact
FBI
13/15
Implementation
Heuristics
d limit degree of FBIs (based on call-graph)
Example (Factorial)
x +0→x
0·x →0
x + s(y ) → s(x + y )
function symbol
degree
HZ SW AM (UIBK)
0
0
s
0
s(x) · y → x · y + y
+
0
·
1
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
fact
2
FBI
13/15
Implementation
Heuristics
d limit degree of FBIs (based on call-graph)
+ limit shape/coefficients of FBIs
Example (Factorial)
x +0→x
0·x →0
x + s(y ) → s(x + y )
function symbol
degree
HZ SW AM (UIBK)
0
0
s
0
s(x) · y → x · y + y
+
0
·
1
fact(0) → s(0)
fact(s(x)) → s(x) · fact(x)
fact
2
FBI
13/15
Implementation
Experimental results
TTT2
method
poly
a
TPDB 8.0.6a
YES avg. time
125
0.4
Example (Factorial)
time
-
TRS Standard
HZ SW AM (UIBK)
FBI
14/15
Implementation
Experimental results
TTT2
method
poly
fbi
a
TPDB 8.0.6a
YES avg. time
125
0.4
32
31.8
Example (Factorial)
time
1243.7
TRS Standard
HZ SW AM (UIBK)
FBI
14/15
Implementation
Experimental results
TTT2
method
poly
fbi
fbi(d)
fbi(d+)
a
TPDB 8.0.6a
YES avg. time
125
0.4
32
31.8
159
5.8
162
5.7
Example (Factorial)
time
1243.7
20.2
9.1
TRS Standard
HZ SW AM (UIBK)
FBI
14/15
Conclusion
Conclusion
Summary
• implementation of (some) elementary functions
• harder than ordinal arithmetic
HZ SW AM (UIBK)
FBI
15/15
Conclusion
Conclusion
Summary
• implementation of (some) elementary functions
• harder than ordinal arithmetic
Limitations
• fails if x x is needed
• multiple exponential derivational complexity
HZ SW AM (UIBK)
FBI
15/15
Conclusion
Conclusion
Summary
• implementation of (some) elementary functions
• harder than ordinal arithmetic
Limitations
• fails if x x is needed
• multiple exponential derivational complexity
Future work
• suitable for AC
• suitable for ordered completion
HZ SW AM (UIBK)
FBI
15/15

Annelies Törös - Juwelier Paul Roelandt