2.2.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
...
 

На Рефале: 

(" ex)   <P ex> = T,   если <P ex> определено

 
P     {    ex   =   <Eq (<Ad (ex) (I)>) (<Ad (I) (ex)>)>;
}
Ad   { (ex (ey) = ex ey;
}
Eq    {    () () T;
(ex I)  (ey I)   = <Eq (ex) (ey)>;
() (ey I) = F;
(ex I) () = F;
}
Num   { 0  =  ;
1  =  I;
2  =  I I;
...
10 = I I I I I I I I I I;
...
}