Subject Reduction of Logic Programs as Proof-Theoretic Property.

摘要: We consider prescriptive type systems for logic programs (as in Godel or Mercury). In such systems, the typing is static, but it guarantees an operational property: if a program “well-typed”, then all derivations starting “well-typed” query are again “well-typed”. This property has been called subject reduction. show that this can also be phrased as of proof-theoretic semantics programs, thus abstracting from usual (top-down) semantics. view leads us to questioning condition which usually considered necessary reduction, namely head condition. It states each clause must have variant (and not proper instance) declared type. study more general conditions, reestablishing certain symmetry between heads and body atoms. The underlying idea derivation, terms should only unified their types unifiable. discuss possible implications our results.