IAP1 (2007)
Attention à bien reprendre ces exemples avec des symboles
préfixes uniquement.
Ackermann
Signature
0 : constant
s : unary
ack : binary
Variables
x y z
Système
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x),y))
Unicité du résultat.
Quotient
Signature
0 : constant
s : unary
q : binary
q':3
Variables
x y z
Système
q(0,s(y)) → 0
q(s(x),s(y)) → q'(x,y,s(y))
q'(x,0,z) → s(q(x,z))
q'(0,s(y),z) → 0
q'(s(x),s(y),z) → q'(x,y,z)
Unicité du résultat.
PGDC
Signature
true, false : constant
0 : constant
s,p : unary
- : infix binary
ge,gcd : binary
ifgcd : 3
Variables
x y z
Système
p(0) → 0
p(s(x)) → x
x-0 → x
x-s(y) → p(x-y)
ge(x,0) → true
ge(0,s(y)) → false
ge(s(x),s(y)) → ge(x,y)
gcd(x,0) → x
gcd(0,y) → y
gcd(s(x),s(y)) → ifgcd(ge(x,y),s(x),s(y))
ifgcd(true,s(x),s(y)) → gcd(x-y,s(y))
ifgcd(false,s(x),s(y)) → gcd(s(x),y-x)
Unicité du résultat.
Arithmétique binaire
Signature
# : constant
0,1 : postfix unary
+,* : infix binary
Variables
x y
Système
(#)0 → #
# + x → x
x + # → x
(x)0 + (y)0 → (x+y)0
(x)0 + (y)1 → (x+y)1
(x)1 + (y)0 → (x+y)1
(x)1 + (y)1 → (x+y+(#)1)0
# * x → #
x * # → #
(x)0 * y → (x*y)0
(x)1 * y → (x*y)0 + y
Unicité du résultat.
Logarithme
Signature
# : constant
0,1 : postfix unary
+,- : infix binary
ge : binary
true,false : constant
not : unary
log : unary
log' : unary
if : 3
Variables
x y z
Système
(#)0 → #
# + x → x
x + # → x
(x)0 + (y)0 → (x+y)0
(x)0 + (y)1 → (x+y)1
(x)1 + (y)0 → (x+y)1
(x)1 + (y)1 → (x+y+(#)1)0
# - x → #
x - # → x
(x)0 - (y)0 → (x-y)0
(x)0 - (y)1 → ((x-y)-(#)1)1
(x)1 - (y)0 → (x-y)1
(x)1 - (y)1 → (x-y)0
not(true) → false
not(false) → true
if(true,x,y) → x
if(false,x,y) → y
ge((x)0,(y)0) → ge(x,y)
ge((x)0,(y)1) → not(ge(y,x))
ge((x)1,(y)0) → ge(x,y)
ge((x)1,(y)1) → ge(x,y)
ge(x,#) → true
ge(#,(x)0) → ge(#,x)
ge(#,(x)1) → false
log(x) → log'(x) - (#)1
log'(#) → #
log'((x)1) → log'(x) + (#)1
log'((x)0) → if(ge(x,(#)1),log'(x) + (#)1,#)
Attention il n'y a pas unicité du résultat.