A Treatment of Higher-Order Features in Logic Programming

Title: A Treatment of Higher-Order Features in Logic Programming

Research Question: How can higher-order notions be effectively incorporated into logic programming, and what are the implications of this approach?

Methodology: The authors propose using the terms of a typed lambda calculus as representational devices and implementing a richer form of unification for probing their structures. They address three main issues: suitable encoding of lambda terms, handling branching in unification, and dealing with dynamically emergent goals.

Results: The authors develop a satisfactory representation for lambda terms by exploiting de Bruijn's nameless notation and explicit encodings of substitutions. They design special mechanisms to support branching in unification and carrying of unification problems over other computation steps. An extended compilation model is presented that handles higher-order unification and dynamically emergent goals.

Implications: The ideas described in the paper have been employed in the Teyjus implementation of the λProlog language, which serves as a preliminary assessment of their effectiveness. The research suggests that logic programming can offer a more sophisticated understanding of higher-order notions compared to traditional imperative or functional programming paradigms. It also opens up new possibilities for metalanguage applications in logic programming.

Link to Article: https://arxiv.org/abs/0404020v1 Authors: arXiv ID: 0404020v1