> In particular, note the appearance of an existential quantifier in the premises of the sequential composition and Kleene star cases, and note the nondetermini

> In particular, note the appearance of an existential quantifier in the premises of the sequential composition and Kleene star cases, and note the nondeterministic choice of a branch in the alternation case. So read as a logic program, this semantics is not well-moded. Is this saying that you cannot mechanically convert a "declarative language" into a program? Or is it saying it may allow multiple choices? If so, how is it not included in the Curry-Howard correspondence?