2.3.1
Доказательство коммутативности сложения с 1:
постановка задачи на суперкомпиляцию
(
"
x
Î
N)
x
+ 1 = 1 +
x
P(x) = Eq(x+1, 1+x)
Þ
P(x) = T
x + 0
= x
x + (y+1)
= (x+y)+1
Eq(0,
0)
=
T
Eq(x+1,
y+1)
=
Eq(x,y)
Eq(0,
y+1)
=
F
Eq(x+1,
0)
=
F
1 = 0+1
2 = (0+1)+1
...
На Рефале:
(
"
e
x
) <P e
x
> = T
P
{
e
x
= <Eq (<Ad (e
x
) (I)>) (<Ad (I) (e
x
)>)>;
}
Ad
{
(e
x
)
()
=
e
x
;
(e
x
)
(e
y
I)
=
<Ad (e
x
) (e
y
)> I;
}
Eq
{
()
()
=
T;
(e
x
I)
(e
y
I)
=
<Eq (e
x
) (e
y
)>;
()
(e
y
I)
=
F;
(e
x
I)
()
=
F;
}
Num
{
0 = ;
1 = I;
2 = I I;
...
10 = I I I I I I I I I I;
...
}