• Arts
• Business
• Computers
• Games
• Health
• Home
• Kids and Teens
• News
• Recreation
• Reference
• Regional
• Science
• Shopping
• Society
• Sports

Proof Theory as an Alternative to Model Theory

Proof Theory as an Alternative to Model Theory Proof Theory as an Alternative to Model Theory LFCS, University of Edinburgh and CIS, University of Pennsylvania The design and analysis of declarative programming languages require that computation be described in two separate ways: by an interpreter that extracts values from a program and by a declarative specification of what values should be attributed to a program. A soundness theorem for a programming language states that its interpreter computes only attributed values and a completeness theorem states that the interpreter extracts all such values. For example, in the logic programming literature, SLD-resolution is often used to define an interpreter that extracts values from a Horn clause program while minimal Herbrand models attribute values to programs. Since these two concepts -- resolution and model theory -- are very different, soundness and completeness theorems give us some confidence that Horn clause programming is not "hacky" and that they will have useful meta-level properties. Such meta-level properties can then be exploited in sophisticated program manipulations (e.g., partial evaluation, fold/unfold), in implementations on different models of computation (e.g., sequential, parallel), and in the proofs of program correctness. The separate descriptions of what values are extracted by an interpreter from a program and what values should be attributed to a program gives declarative programming languages their character.

Contact Information