Well-Typed Logic Programs Are not Wrong

Details Well-Typed Logic Programs Are not Wrong Well-Typed Logic Programs Are not Wrong

2000-12-20

arxiv.org/abs/cs/0012015v2

Computer Science

Logic in Computer Science

21 pages, 7 figures

Scientific paper

We consider prescriptive type systems for logic programs (as in Goedel or Mercury). In such systems, the typing is static, but it guarantees an operational property: if a program is "well-typed", then all derivations starting in a "well-typed" query are again "well-typed". This property has been called subject reduction. We show that this property can also be phrased as a property of the proof-theoretic semantics of logic programs, thus abstracting from the usual operational (top-down) semantics. This proof-theoretic view leads us to questioning a condition which is usually considered necessary for subject reduction, namely the head condition. It states that the head of each clause must have a type which is a variant (and not a proper instance) of the declared type. We provide a more general condition, thus reestablishing a certain symmetry between heads and body atoms. The condition ensures that in a derivation, the types of two unified terms are themselves unifiable. We discuss possible implications of this result. We also discuss the relationship between the head condition and polymorphic recursion, a concept known in functional programming.

Affiliated with

Also associated with

No associations

Rating

Well-Typed Logic Programs Are not Wrong does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Well-Typed Logic Programs Are not Wrong, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Well-Typed Logic Programs Are not Wrong will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-374495