Hovedprogrammet kan kalde såvel p som q, kroppen for q kan kalde p og q, og p kan kun kalde p.

I proceduren p1 forsøges en boolsk værdi (angivet ved den globalevariabel b) lagt over i en heltalsvariablen i. I p2 erklæres en lokal variabel a, som er et heltalsarray, og der forsøges lagt værdien false ind på arrayets 3. plads. Parametren x optræder på venstre side i en assignment, hvilket sådan set er OK, men højresiden skulle i såfald have en type svarende til heltal og ikke som her en type svarende til int_array(3). I hovedprogrammet er det også helt galt, alle procedurer havde pr. definition heltalsparametre, men her kaldes p1 med arrayet c som parameter, p2 kaldes med et forkert antal parametre, c som er af type svarende til int_array(7) forsøges assignet en værdi af type int_array(3). Endelig er sætningen xxx:= yyy ikke tilladt, da den benytter to variable, som ikke er erklæret.

Ethvert korrekt udtryk i Pax har en veldefineret type , og følgende typer er mulige: int, bool, int_array(2), int_array(3), int_array(4), ... .

• Typen af en variabel er den, som er angivet i erklæringen.
• Typen af en parameter inde i en procedure er altid int, og parameteren kan bruges som en vilkårlig lokal variabel.
• Inde i en procedure kan der kun refereres til følgende variable:

• Hvis v er en variabel at type int_array(n) og u et udtryk af type int, da er v^u af type int (Vi betragter ikke indeksfejl som typefejl, men som køretidsfejl).
• For en sætning v:= udtryk, skal v og udtryk have samme type.
• De udtryk, som optræder som betingelse i if, while og repeat konstruktionerne skal have type bool.
• Et udtryk u1 + u2 har type int, såfremt u1 og u2 har type int; tilsvarende for -, *, //.
• Et udtryk u1 = u2 har type bool, såfremt u1 og u2 har type int; tilsvarende for >, >=, <, =<, =\=.
• Et udtryk u1 /\ u2 har type bool, såfremt u1 og u2 har type bool; tilsvarende for /\.
• Et udtryk \+ u har type bool, såfremt u har type bool.
• Et procedurekald p(u) er korrekt typet, såfremt p er erklæret med én parameter og u har type int.
• Et procedurekald p(u1, u2) er korrekt typet, såfremt p er erklæret med to parametre og u1 og u2 har type int.
• Et udtryk af formen [u1, ..., un] har type int_array(n) hvis u1,...,un alle har type int (for n³2).
• Ingen andre udtryk, end de, som er omtalt overfor, er korrekt typede.
• Ethvert andet syntakstræ er korrekt typet, såfremt de indgående udtryk er korrekt typede.

Hvis vi for en stund ser bort fra variable i udtrykkene, kan vi beskrive typebetingelsen ved at tilføje et ekstra argument til de syntaktiske prædikater, som holder typen. Vi ændrer prædikaternes navne ved at sætte ªt_´ foran, så man kan se, at det er et nyt prædikat, som foretager typecheck. I eksemplet med plus-udtrykket kommer reglen til at se således ud:

Hvis vi har en erklæring var(n, int), er det relevant, at der produceres en symboltabel, som indeholder et par (x, int). For at transportere symboltabellerne ud i alle udtryk og deludtryk kan type-checkprædikaterne udstyres med nok et argument, som indeholder den aktuelle symboltabel. Plus-reglen kommer nu til at se således ud:

På denne måde vil vi opnå en typechecker, som accepterer korrekt typede programmer, og som fejler (dvs. Prolog siger ªno´, hvis programmet ikke er korrekt.

Af hensyn til at lokalisere typefejl – og de programmeringsfejl, man utvivlsomt vil lave under løsning af opgaven – foreslås det, at man erstatter kaldet af member med er prædikat fremstillet til formålet kaldet symbol_tabel_find, så reglen kommer til at se sådan ud:

Her er eksempler på fejlmeddelelser produceret af symbol_tabel_find ved typecheck at fejlagtige programmer.

Sammenhængen mellem procedurers parameterantal i erklæring og anvendelse kan beskrives ved knytte nogle typer vi vil kalde proc1 og proc2 (for procedurer med hhv. én og med to heltalsparametre), der opbevares i symboltabellen helt ligesom variables værdier. Så erklæringen af en procedure ved navn p med to argumenter vil resultere i en indgang (p,proc2) i symboltabellen.

Det er nemmest, hvis de prædikater, som producerer tabeller udstyrese med to argumenter, en tabel-før og en tabel-efter. Så hvis vi eksempelvis har en symboltabel [(x,int)] før vi processerer erklæringen var(b, bool), vil vi efterfølgende få en tabel

Den eneste egenskab, som fortolkeren må kontrollere løbende er index-check for arrays, dvs. hvis eksempelvis a er bundet til array-værdien [1,2,3,4], og i er en heltalsvariabel, så is værdi udregnes, og det skal kontrolleres, at denne værdi ligger mellem 1 og 4 for at a^i kan udregnes Alt vdr. indekscheck er indbygget i prædikater, der er givet på forhånd til håndtering af rekursionsstakken – men nu er fænomenet nævnt for en ordens skyld.

Stakken repræsenteres som en liste af stakafsnit, hvor vi tænker på bunden af stakken som det sidste (= ªhøjreste´) element, og det indeholder de globale variable. Der hægtes så nye afsnit på, når der kaldes en procedure, og stakkes af, når en procedure forlades. Bindinger til variable repræsenteres ved par af formen (Variabel-navn, Værdi). Det er vigtigt at bemærke forskellen mellem bindingerne i rekursionsstakken og informationen gemt i en symboltabel: Symboltabellen vedrører statiske egenskaber ved symbolerne, i vores tilfælde deres type, hvorimod stakafsnittene i rekursionsstakken rummer bindinger af variable til deres dynamisk genererede værdier.

Betragt som eksempel quicksortprogrammet vist i afsnit 1. Lige inden procedurekaldet proc(qsort,1,n) ser rekursionsstakken således ud:

Nu kaldes proceduren, parametrenes værdier udregnes og overføres til lokale variable (kaldet left og right) til dette procedurekalds stakafsnit, og der afsættes plads til de lokale variable i, j, x og w. Stakken ser nu således ud:

Nu går procedurens sorteringsalgoritme igang, og når repeat-sætningen er udført og lige inden de to if-sætninger ser stakken således ud; der er de samme stakafsnit, men nogle variables værdier er ændret:

Man kan se videre, at betingelse i første if-sætning vil evaluere til false, mens betingelsen for den anden bliver til true, hvilket giver anledning til et rekursivt procedurekald. Når parametrene er udregnet og overført, og der er afsat plads til et nyt sæt lokale variable, har vi følgende stak:

Vi har nu stakafsnit svarende til to inkarnationer af proceduren qsort, dvs. der ligger to indgange i stakken for (eksempelvis) parametren right, den øverste for det seneste og nu aktive kald, og en ªlavere-liggende´ for det første procedurekald. Der vil blive aktiveret endnu flere rekursive kald, hvilket resulterer i endnu flere stakafsnit – op på et tidspunkt, når de har afsluttet og deres stakafsnit er afstakket, når vi (hvis ellers fortolkeren er programmeret korrekt) tilbage til en stak:

Ydermere er virkefeltsreglerne indrettet så visseligt at hvis der i en given aktivering af en procedure refereres til en variabel x, så

• hvis x findes i det øverste afsnit, så er x lokal, og der er værdien i den øverste afsnit, som er den relevante,
• eller, hvis x ikke findes her, så er x global og findes i det nederste afsnit.

Som eksempel på en global variabel har vi arrayet a i quicksortprogrammet, hvor alle aflæsninger og tilskrivninger i de mange rekursive kald netop (og heldigvis) nåede ned til det globale afsnit.

Variable kan angives som atomer (og referere til simple variable eller hele arrays) og som enkelt-celler i et array ved VariabelNavn^Index, hvor Index er et heltal.

Den regel i fortolkeren, som skal behandle en arrayindicering (som et udtryk) som a^(i+j), skal først udregne i+j, og hvis det nu f.eks. giver resultatet 7, er det relevant at kalde

Tilsvarende, for en sætning af formen a^(i+j):= (x+y)//z. Her skal i+j igen udregnes (og vi antager, den stadig er 7), og (x+y)//z skal også udregnes, skal vi sige med værdi 117, så kan vi derefter kalde

hvor Stak1 refererer til den aktuelle stak og Stak2 til den opdaterede, som gives videre til næste sætning.

Udover at sende rekursionsstakken med rundt til alle sætninger og udtryk, er der også behov for information om de erklærede procedurer: Der skal være en måde, hvorpå en sætning som proc(qsort, 1, n) kan finde ud af, hvad den skal foretage sig. Vi kan her vælge at bruge en proceduretabel, som genereres ud fra procedureerklæringerne, og som ganske enkelt er en liste med alle procedurefinitioner (dvs. deres abstrakte syntakstræ, som det nu engang er givet). I quicksortprogrammet, hvor der kun er én procedure, vil proceduretabellen se således ud:

Reglen for sætningsformen proc(...) kan så i eksemplet med quicksort slå op i tabellen ved et kald som følger, idet Pt forventes at være instantieret til den nævnte tabel:

Denne generelle for procedurekald kan dernæst evaluere de udtryk, der stå for de aktuelle parametre (her ª1´ og ªn´), og sætte et nyt stakafsnit op, som binder parametrenes værdier til de formelle parametre, samt rummer pladser til de (øvrige) lokale variable – sådan som vi så det i rekursionsstakkene vist for et par sider siden.

Når det rette stakafsnit er opbygget – og sat i forrest=øverst på stakken – kan vi kalde den normale procedure for fortolkning af sætninger med procedurens krop som argument. Når dette fortolkerkald har afsluttet, skal vi så sørge for, at den stak som proc(qsort, 1, n) totalt har produceret er den rette, dvs. med det øverste stakafsnit pillet af igen, men hvor resten af stakken (med de indtrufne sideeffekter på global variable) er bevaret.

Til at fortolke sætninger generelt kunne man foreslå et prædikat med følgende form, idet vi generelt skelner fortolkerprædikaterne fra andre ved at sætte ªf_´ foran navnet på den syntaktiske kategori:

Tag som eksempel de globale variabelerklæringer i quicksortprogrammet (var(n,int) ; var(a, int_array(4))). Det, at ªudføre´ eller fortolke dem bør give anledning til følgende endnu uberørte stakafsnit:

Bemærk, at den afsluttende rekursionsstak ignoreres, et Pax-program forventes selv at kunne præsentere sit resultat til omverdenen ved hjælp passende brug ad write og write_text.