Vaje

Vaje

Naloga 1

Preverite primere, izpuščene v zgornjih dokazih.

Naloga 2

Vpeljite relacijo \(\leadsto^*\), ki je tranzitivna in refleksivna ovojnica relacije malih korakov \(\leadsto\). Razložite, kakšen je njen intuitivni pomen ter pokažite, da je res tranzitivna.

Naloga 3

Definirajte vrednosti v za posamezne družine izrazov.

Pokažite pomožno lemo oblike:

s , c1 ~~> s' , c1' 
=> 
s' , c1' --> s'' 
=> 
s , c1 --> s''

Pokažite ujemanje ~~*> in --> (semantika velikih korakov):

s , e --> s', v 
<=> 
s , e ~~*> s' , v

Ujemanje je potrebno pokazati za vsako družino izrazov.