Go backward to Semantics Go up to Top Go forward to Example

Recursively Defined Abstractions

• Typing rule:

  • p U {I:comm} |- C: comm

    rec-proc I=C: {I:comm}dec

    
    
  • Procedure binding visible to own body!
• Repetitive constructs:
  • while E do C od = call W
    where rec-proc W = if E then C; call W else skip fi.
• Semantics:
  • [[p |- rec-proc I=C: {I:comm}dec]]e s
    = {I=r}
    where r(s') = [[p U {I:comm} |- C:comm]]
    (e union{I=r})s'.
• Copy rule:
  • rec-proc I=C = define I=(rec I:comm. C).
  • (rec I:comm.C) => [(rec I:comm.C)/I]C.