Predicate abstractions in higher-order logic programming View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

1996-06

AUTHORS

Weidong Chen, David Scott Warren

ABSTRACT

Lambda calculus offers a natural representation of syntactic structures involving higher-order constructs and local variables, and supports flexible manipulation of such concepts. Thus an integration of logic programming with λ-terms would provide more direct support for metaprogramming. While it is conceptually straightforward to replace first-order terms with λ-terms, the extra search space in unification with respect to λ-conversions cannot be ignored from a practical point of view. Our objective is to explore useful alternatives with weaker conversions that are computationally more tractable. In this paper, we study predicate abstractions, in which λ-abstractions are used to provide anonymous predicates and functions that return predicates. The frameworks is based upon a simple logic of (untyped) λ-calculus, calledLa.La has a general model-theoretic semantics and an equality theory that corresponds to α-equivalence. Intended meanings of predicate abstractions are formalized by equivalence axioms over atomic formulas. We show that under certain conditions, computing with predicate abstractions does not incur any extra search space. Furthermore, programs in this language can be compiled statically into efficient Prolog programs and all most general answers are still preserved. More... »

PAGES

195-236

References to SciGraph publications

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/bf03037499

DOI

http://dx.doi.org/10.1007/bf03037499

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1019670986


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Computer Science & Engineering, Southern Methodist University, 75275-0122, Dallas, TX, USA", 
          "id": "http://www.grid.ac/institutes/grid.263864.d", 
          "name": [
            "Computer Science & Engineering, Southern Methodist University, 75275-0122, Dallas, TX, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Chen", 
        "givenName": "Weidong", 
        "id": "sg:person.01207355664.95", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01207355664.95"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, SUNY at Stony Brook, 11794-4400, Stony Brook, NY, USA", 
          "id": "http://www.grid.ac/institutes/grid.36425.36", 
          "name": [
            "Department of Computer Science, SUNY at Stony Brook, 11794-4400, Stony Brook, NY, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Warren", 
        "givenName": "David Scott", 
        "id": "sg:person.0611624774.02", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0611624774.02"
        ], 
        "type": "Person"
      }
    ], 
    "citation": [
      {
        "id": "sg:pub.10.1007/bf00243002", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1023837652", 
          "https://doi.org/10.1007/bf00243002"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bfb0038698", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1044395718", 
          "https://doi.org/10.1007/bfb0038698"
        ], 
        "type": "CreativeWork"
      }
    ], 
    "datePublished": "1996-06", 
    "datePublishedReg": "1996-06-01", 
    "description": "Lambda calculus offers a natural representation of syntactic structures involving higher-order constructs and local variables, and supports flexible manipulation of such concepts. Thus an integration of logic programming with \u03bb-terms would provide more direct support for metaprogramming. While it is conceptually straightforward to replace first-order terms with \u03bb-terms, the extra search space in unification with respect to \u03bb-conversions cannot be ignored from a practical point of view. Our objective is to explore useful alternatives with weaker conversions that are computationally more tractable. In this paper, we study predicate abstractions, in which \u03bb-abstractions are used to provide anonymous predicates and functions that return predicates. The frameworks is based upon a simple logic of (untyped) \u03bb-calculus, calledLa.La has a general model-theoretic semantics and an equality theory that corresponds to \u03b1-equivalence. Intended meanings of predicate abstractions are formalized by equivalence axioms over atomic formulas. We show that under certain conditions, computing with predicate abstractions does not incur any extra search space. Furthermore, programs in this language can be compiled statically into efficient Prolog programs and all most general answers are still preserved.", 
    "genre": "article", 
    "id": "sg:pub.10.1007/bf03037499", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": [
      {
        "id": "sg:journal.1053619", 
        "issn": [
          "0288-3635", 
          "1882-7055"
        ], 
        "name": "New Generation Computing", 
        "publisher": "Springer Nature", 
        "type": "Periodical"
      }, 
      {
        "issueNumber": "2", 
        "type": "PublicationIssue"
      }, 
      {
        "type": "PublicationVolume", 
        "volumeNumber": "14"
      }
    ], 
    "keywords": [
      "predicate abstraction", 
      "extra search space", 
      "logic programming", 
      "search space", 
      "higher-order logic programming", 
      "model-theoretic semantics", 
      "Prolog programs", 
      "abstraction", 
      "natural representation", 
      "flexible manipulation", 
      "lambda calculus", 
      "equality theory", 
      "simple logic", 
      "programming", 
      "local variables", 
      "equivalence axioms", 
      "predicates", 
      "atomic formulas", 
      "efficient Prolog programs", 
      "direct support", 
      "semantics", 
      "syntactic structure", 
      "practical point", 
      "such concepts", 
      "logic", 
      "language", 
      "calculus", 
      "space", 
      "framework", 
      "representation", 
      "integration", 
      "first-order terms", 
      "terms", 
      "higher-order construct", 
      "general answer", 
      "concept", 
      "axioms", 
      "program", 
      "unification", 
      "answers", 
      "support", 
      "view", 
      "manipulation", 
      "point", 
      "objective", 
      "equivalence", 
      "certain conditions", 
      "alternative", 
      "respect", 
      "meaning", 
      "constructs", 
      "function", 
      "theory", 
      "structure", 
      "variables", 
      "formula", 
      "useful alternative", 
      "conversion", 
      "conditions", 
      "La", 
      "paper", 
      "weak conversion", 
      "anonymous predicates", 
      "calledLa", 
      "general model-theoretic semantics"
    ], 
    "name": "Predicate abstractions in higher-order logic programming", 
    "pagination": "195-236", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1019670986"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/bf03037499"
        ]
      }
    ], 
    "sameAs": [
      "https://doi.org/10.1007/bf03037499", 
      "https://app.dimensions.ai/details/publication/pub.1019670986"
    ], 
    "sdDataset": "articles", 
    "sdDatePublished": "2021-11-01T18:01", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211101/entities/gbq_results/article/article_268.jsonl", 
    "type": "ScholarlyArticle", 
    "url": "https://doi.org/10.1007/bf03037499"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/bf03037499'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/bf03037499'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/bf03037499'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/bf03037499'


 

This table displays all metadata directly associated to this object as RDF triples.

141 TRIPLES      22 PREDICATES      93 URIs      83 LITERALS      6 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/bf03037499 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author Nb5a2da33944f4c408f9ecdf3df94304e
4 schema:citation sg:pub.10.1007/bf00243002
5 sg:pub.10.1007/bfb0038698
6 schema:datePublished 1996-06
7 schema:datePublishedReg 1996-06-01
8 schema:description Lambda calculus offers a natural representation of syntactic structures involving higher-order constructs and local variables, and supports flexible manipulation of such concepts. Thus an integration of logic programming with λ-terms would provide more direct support for metaprogramming. While it is conceptually straightforward to replace first-order terms with λ-terms, the extra search space in unification with respect to λ-conversions cannot be ignored from a practical point of view. Our objective is to explore useful alternatives with weaker conversions that are computationally more tractable. In this paper, we study predicate abstractions, in which λ-abstractions are used to provide anonymous predicates and functions that return predicates. The frameworks is based upon a simple logic of (untyped) λ-calculus, calledLa.La has a general model-theoretic semantics and an equality theory that corresponds to α-equivalence. Intended meanings of predicate abstractions are formalized by equivalence axioms over atomic formulas. We show that under certain conditions, computing with predicate abstractions does not incur any extra search space. Furthermore, programs in this language can be compiled statically into efficient Prolog programs and all most general answers are still preserved.
9 schema:genre article
10 schema:inLanguage en
11 schema:isAccessibleForFree false
12 schema:isPartOf N5e2f3af35ce443d3abfd25a168315638
13 Nf42e9e50a959432b961f821e6227fdea
14 sg:journal.1053619
15 schema:keywords La
16 Prolog programs
17 abstraction
18 alternative
19 anonymous predicates
20 answers
21 atomic formulas
22 axioms
23 calculus
24 calledLa
25 certain conditions
26 concept
27 conditions
28 constructs
29 conversion
30 direct support
31 efficient Prolog programs
32 equality theory
33 equivalence
34 equivalence axioms
35 extra search space
36 first-order terms
37 flexible manipulation
38 formula
39 framework
40 function
41 general answer
42 general model-theoretic semantics
43 higher-order construct
44 higher-order logic programming
45 integration
46 lambda calculus
47 language
48 local variables
49 logic
50 logic programming
51 manipulation
52 meaning
53 model-theoretic semantics
54 natural representation
55 objective
56 paper
57 point
58 practical point
59 predicate abstraction
60 predicates
61 program
62 programming
63 representation
64 respect
65 search space
66 semantics
67 simple logic
68 space
69 structure
70 such concepts
71 support
72 syntactic structure
73 terms
74 theory
75 unification
76 useful alternative
77 variables
78 view
79 weak conversion
80 schema:name Predicate abstractions in higher-order logic programming
81 schema:pagination 195-236
82 schema:productId Nc4cb7a5e95894e6eb69afa8a09fc992a
83 Nd973f425a8124f218007920f973fd545
84 schema:sameAs https://app.dimensions.ai/details/publication/pub.1019670986
85 https://doi.org/10.1007/bf03037499
86 schema:sdDatePublished 2021-11-01T18:01
87 schema:sdLicense https://scigraph.springernature.com/explorer/license/
88 schema:sdPublisher N212fbe90f492484f84beceee7b31449b
89 schema:url https://doi.org/10.1007/bf03037499
90 sgo:license sg:explorer/license/
91 sgo:sdDataset articles
92 rdf:type schema:ScholarlyArticle
93 N10d4b0cede6d4dda8f8c8f381d81bfbb rdf:first sg:person.0611624774.02
94 rdf:rest rdf:nil
95 N212fbe90f492484f84beceee7b31449b schema:name Springer Nature - SN SciGraph project
96 rdf:type schema:Organization
97 N5e2f3af35ce443d3abfd25a168315638 schema:volumeNumber 14
98 rdf:type schema:PublicationVolume
99 Nb5a2da33944f4c408f9ecdf3df94304e rdf:first sg:person.01207355664.95
100 rdf:rest N10d4b0cede6d4dda8f8c8f381d81bfbb
101 Nc4cb7a5e95894e6eb69afa8a09fc992a schema:name doi
102 schema:value 10.1007/bf03037499
103 rdf:type schema:PropertyValue
104 Nd973f425a8124f218007920f973fd545 schema:name dimensions_id
105 schema:value pub.1019670986
106 rdf:type schema:PropertyValue
107 Nf42e9e50a959432b961f821e6227fdea schema:issueNumber 2
108 rdf:type schema:PublicationIssue
109 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
110 schema:name Information and Computing Sciences
111 rdf:type schema:DefinedTerm
112 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
113 schema:name Computation Theory and Mathematics
114 rdf:type schema:DefinedTerm
115 sg:journal.1053619 schema:issn 0288-3635
116 1882-7055
117 schema:name New Generation Computing
118 schema:publisher Springer Nature
119 rdf:type schema:Periodical
120 sg:person.01207355664.95 schema:affiliation grid-institutes:grid.263864.d
121 schema:familyName Chen
122 schema:givenName Weidong
123 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01207355664.95
124 rdf:type schema:Person
125 sg:person.0611624774.02 schema:affiliation grid-institutes:grid.36425.36
126 schema:familyName Warren
127 schema:givenName David Scott
128 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0611624774.02
129 rdf:type schema:Person
130 sg:pub.10.1007/bf00243002 schema:sameAs https://app.dimensions.ai/details/publication/pub.1023837652
131 https://doi.org/10.1007/bf00243002
132 rdf:type schema:CreativeWork
133 sg:pub.10.1007/bfb0038698 schema:sameAs https://app.dimensions.ai/details/publication/pub.1044395718
134 https://doi.org/10.1007/bfb0038698
135 rdf:type schema:CreativeWork
136 grid-institutes:grid.263864.d schema:alternateName Computer Science & Engineering, Southern Methodist University, 75275-0122, Dallas, TX, USA
137 schema:name Computer Science & Engineering, Southern Methodist University, 75275-0122, Dallas, TX, USA
138 rdf:type schema:Organization
139 grid-institutes:grid.36425.36 schema:alternateName Department of Computer Science, SUNY at Stony Brook, 11794-4400, Stony Brook, NY, USA
140 schema:name Department of Computer Science, SUNY at Stony Brook, 11794-4400, Stony Brook, NY, USA
141 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...