A formal operational semantics for languages of type Prolog III