11.Денотационна семантика на рекурсивните програми с предаване на параметри по стоиност.

Нека е даден терм c (Х₁,..., Х_n ,F₁^m ,, F_k^mk ). Можем да пресметнем стойноста на c ,стига да разполагаме с подходящи стойности на променливите.Ще предполагаме че подходящи стойности за обектoвите променливи са естествени числа а за функционалните променливи частични ф-ции на съответния брой аргументи в N.Нека са дадени естествените числа a₁ ,.., a_n и частичните ф-ции v ₁ ,.., v_к съответно на m₁ ,.., m_к аргумента.Тогава ст/ста c(a₁ ,.., a_n , v ₁ ,.., v_к) съкратено c(yаy, y vy), на терма c се дефинира индуктивно:

1.ако c е константа с ,то c(yаy, y vy) с;

2.ако c= Х_i то c(yаy, y vy) a_i ;

3.ako c =f(c₁,..., c_l) където f е l-местна основна операция ,то c(yаy, y vy) f(c₁(yаy, yхy),..., c_l (yаy,y vy));

4.ако c= if p then c₁else c₂ ,то

c(yаy, y vy) =

c1 (yаy, y vy), ако p (yаy, y vy) tt c2 (yаy, y vy) Ако p (yаy, y vy) ff |

5.ako c= F_i^mi (c_l,, c_mi),то c (yаy, y vy) v_i (c₁ (yаy, y vy,, c_mi (yаy, y vy)).

Нека c (Х₁,..., Х_n ,F₁^m1 ,, F_k^mk ) е терм.Нека са дадени v ₁ } x₁ F_m1 ,, v_к } x_k F_mk .Тогава при всеки избор на естествените числа a₁ ,.., a_n и на константа b от типа на c е в сила импликацията c(a₁ ,.., a_n , v ₁ ,.., v_к) b c(a₁ ,.., a_n , x₁ ,.., x_k ) b.

Нека c (Х₁,..., Х_n ,F₁^m1 ,, F_k^mk ) е терм , a₁ ,.., a_n са естествени числа и v ₁ ,.., v_к са частни ф-ции съответно на m₁ ,.., m_к аргумента. Ако c (yаy, y vy) бb то съществуват крайни ф-ции h_k } v ₁ ,.., h_к } v_к за които c(yаy, yhy ) b. Нека c(Х₁,..., Х_n ,F₁^m1 ,, F_k^mk ) е терм от тип Nat или условен терм.Тогава Гc е мепрекъснато изображение на F в F_n .

Денотационната семантика на програмата R с предаване на параметрите по ст/ст наричаме частичната ф-ция D_v (R) на n аргумента N, определена чрез равенството

D_v (R)( a₁ ,.., a_n ) c₀ (a₁ ,.., a_{n ,} v ₁ ,.., v_к ). Денотационната семантика е лишена от техническите детайли на операционната семантика.Тя е много по-мат. по своя характер .Неино основно предимство е че тя позволява да расъждаваме за свойствата на програмата R в термините на неподвижните точки и да прилагаме варианти на правилото за l-индукцията при верификацията на R. В този смисъл тази семантика е по подходяща за програмиста докато операционната семантика е по-подходяща за компютъра.

Нека c (Х₁,..., Х_n ,F₁^m1 ,, F_k^mk ) е произволен терм.Нека с₁ ,.., с_n са константи и l= c (Х₁ / с₁ ,..., Х_n / с_n, F).Тогава при всеки избор на частичните ф-ции x₁ F_m1 ,..., x_k F_mк имаме c (с₁ ,.., с_n , x₁ ,.., x_k ) l (x₁ ,.., x_k).