2025-11-10T02:31:47.007663

CoLF Logic Programming as Infinitary Proof Exploration

Chen, Pfenning
Logical Frameworks such as Automath [de Bruijn, 1968] or LF [Harper et al., 1993] were originally conceived as metalanguages for the specification of foundationally uncommitted deductive systems, yielding generic proof checkers. Their high level of abstraction was soon exploited to also express algorithms over deductive systems such as theorem provers, type-checkers, evaluators, compilers, proof transformers, etc. in the paradigm of computation-as-proof-construction. This has been realized in languages such as $λ$-Prolog [Miller et al., 1991] or Elf [Pfenning, 1991] based on backward chaining, and LolliMon [Lopez et al., 2005] or Celf [Schack-Nielsen and Schuermann, 2008], which integrated forward chaining. None of these early frameworks supported the direct expression of infinitary objects or proofs, which are available in the recently developed CoLF$^ω$ [Chen, 2023]. In this work-in-progress report, we sketch an approach to computation-as-proof-construction over the first-order fragment of CoLF$^ω$ (called CoLF$^ω_1$ ) that already includes infinitary objects and proofs. A key idea is the interpretation of logic variables as communication channels and computation as concurrent message-passing. This is realized in a concrete compiler from CoLF$^ω_1$ to Sax, a proof-theoretically inspired parallel programming language based on the proof-reduction in the semi-axiomatic sequent calculus [DeYoung et al., 2020].
academic

CoLF लॉजिक प्रोग्रामिंग अनंत प्रमाण अन्वेषण के रूप में

बुनियादी जानकारी

  • पेपर ID: 2510.12302
  • शीर्षक: CoLF Logic Programming as Infinitary Proof Exploration
  • लेखक: Zhibo Chen (Carnegie Mellon University), Frank Pfenning (Carnegie Mellon University)
  • वर्गीकरण: cs.LO (कंप्यूटर विज्ञान में तर्क)
  • प्रकाशन सम्मेलन: LFMTP 2025 (तार्किक ढांचे और मेटा-भाषाओं पर अंतर्राष्ट्रीय कार्यशाला: सिद्धांत और व्यवहार)
  • पेपर लिंक: https://arxiv.org/abs/2510.12302

सारांश

यह पेपर CoLF^ω के प्रथम-क्रम खंड (CoLF^ω_1) पर "गणना प्रमाण निर्माण है" विधि को लागू करने का अन्वेषण करता है, जिस खंड में पहले से ही अनंत वस्तुएं और प्रमाण शामिल हैं। मूल विचार तार्किक चर को संचार चैनलों के रूप में व्याख्यायित करना है और गणना को समवर्ती संदेश पारेषण के रूप में व्याख्यायित करना है। यह विचार एक ठोस संकलक कार्यान्वयन के माध्यम से साकार होता है, जो CoLF^ω_1 को Sax में संकलित करता है—एक प्रमाण-सैद्धांतिक रूप से प्रेरित समानांतर प्रोग्रामिंग भाषा जो अर्ध-स्वयंसिद्ध अनुक्रम कलन में प्रमाण न्यूनीकरण पर आधारित है।

अनुसंधान पृष्ठभूमि और प्रेरणा

समस्या की पृष्ठभूमि

  1. पारंपरिक तार्किक ढांचे की सीमाएं: Automath और LF जैसे प्रारंभिक तार्किक ढांचे "गणना प्रमाण निर्माण है" प्रतिमान को सफलतापूर्वक लागू करते हैं, लेकिन अनंत वस्तुओं या प्रमाणों को सीधे व्यक्त करने का समर्थन नहीं करते हैं
  2. मौजूदा कार्यान्वयन की समस्याएं: बैकट्रैकिंग-आधारित प्रमाण खोज अनंत सेटिंग में कई कठिनाइयों का सामना करती है:
    • जब इनपुट अनंत होता है तो समाप्ति की समस्या
    • अनंत वस्तुओं और बैकट्रैकिंग की परस्पर क्रिया (कभी स्पष्ट रूप से विफल नहीं हो सकती)
    • एकीकरण एल्गोरिदम केवल तर्कसंगत (चक्रीय) शब्दों पर समाप्ति की गारंटी देता है, लेकिन कई अनुप्रयोगों में वस्तुएं या प्रमाण तर्कसंगत नहीं होते हैं

अनुसंधान प्रेरणा

  1. अनंत गणना का समर्थन: एक गतिशील शब्दार्थ की आवश्यकता है जो इनपुट से क्रमिक रूप से आउटपुट की गणना कर सके, जैसे धाराओं के बीच ट्रांसड्यूसर
  2. बैकट्रैकिंग से बचना: पैटर्न और विशिष्टता जांच के माध्यम से स्थिर रूप से सुनिश्चित करना कि प्रत्येक अद्वितीय इनपुट के लिए अधिकतम एक प्रमाण है
  3. समानांतरीकरण: साझा चर के बीच संचार का उपयोग करके कई परिसरों के बीच और-समानांतरता को लागू करना

मुख्य योगदान

  1. CoLF^ω_1 तार्किक प्रोग्रामिंग भाषा का प्रस्ताव: अनंत शब्द प्रतिनिधित्व का समर्थन करने वाले प्रमाण, बैकट्रैकिंग-मुक्त प्रमाण निर्माण, साझा तार्किक चर का उपयोग करके संचार के लिए समानांतर परिसर मूल्यांकन
  2. नवीन गणना मॉडल: तार्किक चर को संचार चैनलों के रूप में व्याख्यायित करना, गणना को समवर्ती संदेश पारेषण के रूप में व्याख्यायित करना
  3. संकलक का कार्यान्वयन: CoLF^ω_1 से Sax तक का ठोस संकलक कार्यान्वयन
  4. समृद्ध उदाहरण प्रणाली: धारा प्रसंस्करण, फिबोनैचि अनुक्रम, समाकलन संचालन आदि जटिल संबंधों का कार्यान्वयन

विधि विवरण

कार्य परिभाषा

यह पेपर अनंत वस्तुओं का समर्थन करने वाले तार्किक ढांचे में तार्किक प्रोग्रामिंग को कैसे लागू किया जाए, इसका अध्ययन करता है, विशेष रूप से कार्य है:

  • इनपुट: CoLF^ω_1 प्रोग्राम विनिर्देश
  • आउटपुट: समवर्ती संदेश पारेषण के माध्यम से गणना की गई अनंत संरचनाएं (जैसे धाराएं)
  • बाधाएं: बैकट्रैकिंग-मुक्त, समानांतर गणना का समर्थन, विशिष्टता की गारंटी

मुख्य तकनीकी आर्किटेक्चर

1. डेटा प्रकार प्रणाली

conat: cotype.          % सह-प्राकृतिक संख्या प्रकार
z: conat.               % शून्य निर्माता
s: conat -> conat.      % उत्तराधिकारी निर्माता

stream: cotype.         % धारा प्रकार
cons: conat -> stream -> stream.  % धारा निर्माता

2. संबंध परिभाषा और पैटर्न घोषणा

add: conat -> conat -> conat -> cotype. %mode add + + -.
add_z : add z A A.
add_s : add A B C -> add (s A) B (s C).

3. गणना शब्दार्थ

प्रोग्राम का व्यवहार निम्नलिखित संचालन के माध्यम से परिभाषित किया गया है:

  • चैनल संचालन: प्रत्येक पैरामीटर को संचार चैनल के रूप में माना जाता है, पैटर्न घोषणा इनपुट (+) या आउटपुट (-) चैनल निर्दिष्ट करती है
  • पढ़ना-लिखना संचालन: प्रोग्राम इनपुट चैनल से मान पढ़ सकता है, आउटपुट चैनल में मान लिख सकता है
  • चैनल अग्रेषण: इनपुट चैनल को सीधे आउटपुट चैनल में अग्रेषित करना
  • समानांतर पीढ़ी: नए चैनल आवंटित करना और नई प्रक्रियाएं उत्पन्न करना

तकनीकी नवाचार बिंदु

1. बैकट्रैकिंग-मुक्त गारंटी

स्थिर विशिष्टता जांच के माध्यम से सुनिश्चित करना कि प्रत्येक प्रोग्राम बिंदु पर अधिकतम एक संभावित कार्य है, पारंपरिक तार्किक प्रोग्रामिंग में बैकट्रैकिंग की आवश्यकता को समाप्त करता है।

2. समवर्ती निष्पादन मॉडल

mult_s : mult A B C -> add B C D -> mult (s A) B D.

उपरोक्त गुणन परिभाषा में, mult A B C और add B C D दोनों परिसरों को समानांतर में मूल्यांकन किया जा सकता है, साझा चर C के माध्यम से संचार करते हुए।

3. वृद्धिशील गणना

आलसी मूल्यांकन का समर्थन करता है, जब आउटपुट D क्रमिक रूप से प्रकट होता है, तो पहले B चरणों में mult A B C का मूल्यांकन करने की आवश्यकता नहीं है, क्योंकि C अपरिवर्तित रहता है।

प्रायोगिक सेटअप

परीक्षण मामले

पेपर विधि की प्रभावशीलता को सत्यापित करने के लिए कई ठोस उदाहरणों के माध्यम से:

  1. बुनियादी धारा संचालन:
    • repeat n: संख्या n को अनंत बार दोहराने वाली धारा
    • up n: n से शुरू होने वाली बढ़ती धारा
  2. जटिल संबंध:
    • सह-प्राकृतिक संख्या जोड़
    • धारा का बिंदु-वार जोड़
    • फिबोनैचि अनुक्रम पीढ़ी
  3. उन्नत संचालन:
    • समाकलन संचालन (संचयी योग)
    • सम संख्या धारा पीढ़ी

कार्यान्वयन विवरण

  • संकलक CoLF^ω_1 स्रोत कोड को Sax कोड में उत्पन्न करता है
  • पूर्वनिर्धारित गहराई तक मूल्यांकन के बाद रुकता है
  • समवर्ती प्रक्रियाओं के बीच संदेश पारेषण का समर्थन करता है

प्रायोगिक परिणाम

मुख्य परिणाम

1. बुनियादी धारा पीढ़ी

up z निष्पादन परिणाम:
(cons z
(cons (s z)
(cons (s (s z))
(cons (s (s (s z)))
(cons (s (s (s (s z)))) ...)))))

2. अनंत वस्तु हैंडलिंग

omega : conat = s omega.
main : stream = repeat omega.

परिणाम:
(cons (s (s (s (s ...))))
(cons (s (s (s ...)))
(cons (s (s ...))
(cons (s ...)
(cons ...)))))

3. जटिल गणना सत्यापन

फिबोनैचि अनुक्रम:

(cons z
(cons (s z)
(cons (s z)
(cons (s (s z))
(cons (s (s (s z)))
(cons (s (s (s (s (s z)))))
(cons (s (s (s (s (s (s (s (s z)))))))) ...)))))))

समाकलन संचालन परिणाम:

(cons z
(cons (s z)
(cons (s (s (s z)))
(cons (s (s (s (s (s (s z))))))
(cons (s (s (s (s (s (s (s (s (s (s z)))))))))) ...)))))

प्रायोगिक निष्कर्ष

  1. समानांतरता सत्यापन: कई परिसरों को वास्तव में समानांतर में निष्पादित किया जा सकता है, साझा चर के माध्यम से प्रभावी संचार
  2. अनंत संरचना हैंडलिंग: अनंत पुनरावर्ती परिभाषाओं को सफलतापूर्वक संभाला, जैसे ω = s ω
  3. वृद्धिशील गणना: आलसी मूल्यांकन और वृद्धिशील आउटपुट की प्रभावशीलता सत्यापित

संबंधित कार्य

पारंपरिक तार्किक ढांचे

  • LF श्रृंखला: Harper आदि द्वारा LF ढांचा, बुनियादी प्रमाण जांच का समर्थन करता है
  • λ-Prolog/Elf: पिछड़ी श्रृंखला पर आधारित गणना प्रमाण निर्माण है
  • LolliMon/Celf: आगे की श्रृंखला को एकीकृत करने वाला ढांचा

इस पेपर के संबंधित कार्य पर लाभ

  1. अनंत समर्थन: तार्किक ढांचे में पहली बार अनंत वस्तुओं और प्रमाणों का सीधा समर्थन
  2. समवर्ती मॉडल: नवीन समवर्ती संदेश पारेषण गणना मॉडल
  3. बैकट्रैकिंग-मुक्त: स्थिर विश्लेषण के माध्यम से बैकट्रैकिंग की आवश्यकता को समाप्त करता है

निष्कर्ष और चर्चा

मुख्य निष्कर्ष

  1. अनंत वस्तुओं का समर्थन करने वाली तार्किक प्रोग्रामिंग भाषा CoLF^ω_1 को सफलतापूर्वक लागू किया
  2. तार्किक चर को संचार चैनलों के रूप में व्याख्यायित करने की व्यवहार्यता सत्यापित की
  3. समवर्ती संदेश पारेषण मॉडल की तार्किक प्रोग्रामिंग में प्रभावशीलता सिद्ध की

सीमाएं

  1. वर्तमान में केवल सह-आगमनात्मक खंड का समर्थन करता है: मिश्रित आगमनात्मक और सह-आगमनात्मक मामलों का समर्थन नहीं करता है
  2. प्रथम-क्रम प्रतिबंध: वर्तमान में केवल प्रथम-क्रम खंड लागू, उच्च-क्रम शब्दों का समर्थन नहीं
  3. प्रकार प्रणाली सीमा: आश्रित प्रकार शब्दों का समर्थन नहीं करता है (केवल प्रमाण वस्तु स्तर पर समर्थन)

भविष्य की दिशाएं

  1. पूर्ण CoLF^ω तक विस्तार: उच्च-क्रम शब्दों, आश्रित प्रकार शब्दों का समर्थन
  2. मिश्रित आगमनात्मक सह-आगमनात्मक: आगमनात्मक और सह-आगमनात्मक प्रकारों के मिश्रण का समर्थन
  3. औपचारिक शब्दार्थ: संकलन प्रक्रिया का पूर्ण औपचारिकीकरण विवरण

गहन मूल्यांकन

लाभ

  1. सिद्धांत नवाचार मजबूत: तार्किक प्रोग्रामिंग ढांचे में पहली बार अनंत वस्तुओं का परिचय, महत्वपूर्ण सैद्धांतिक मूल्य
  2. कार्यान्वयन पूर्णता: सिद्धांत से कार्यान्वयन तक पूर्ण पथ प्रदान करता है, संकलक कार्यान्वयन सहित
  3. समृद्ध उदाहरण: कई ठोस उदाहरणों के माध्यम से विधि की व्यावहारिकता स्पष्ट रूप से प्रदर्शित
  4. समवर्ती मॉडल नवीन: तार्किक प्रोग्रामिंग को समवर्ती गणना के साथ जैविक रूप से संयोजित करता है

कमियां

  1. सैद्धांतिक विश्लेषण अपर्याप्त गहराई: प्रगति रिपोर्ट के रूप में, औपचारिक शब्दार्थ परिभाषा और सही प्रमाण की कमी
  2. प्रदर्शन विश्लेषण अनुपस्थित: प्रदर्शन बेंचमार्क परीक्षण और जटिलता विश्लेषण प्रदान नहीं करता है
  3. लागू सीमा प्रतिबंधित: वर्तमान संस्करण कार्यक्षमता सीमित, व्यावहारिकता से दूर

प्रभाव

  1. शैक्षणिक योगदान: तार्किक प्रोग्रामिंग क्षेत्र में नई अनुसंधान दिशा का परिचय
  2. व्यावहारिक मूल्य: अनंत डेटा संरचनाओं को संभालने के लिए नई प्रोग्रामिंग प्रतिमान प्रदान करता है
  3. पुनरुत्पादनीयता: ठोस कार्यान्वयन प्रदान करता है, सत्यापन और विस्तार को सुविधाजनक बनाता है

लागू परिदृश्य

  1. धारा प्रसंस्करण प्रणाली: अनंत डेटा धाराओं को संभालने वाले अनुप्रयोगों के लिए उपयुक्त
  2. प्रतीकात्मक गणना: अनंत गणितीय वस्तुओं को संभालने की आवश्यकता वाली गणना
  3. समवर्ती प्रणाली मॉडलिंग: समवर्ती प्रणालियों के व्यवहार को मॉडल और सत्यापित करने के लिए उपयोग किया जा सकता है

संदर्भ

पेपर तार्किक ढांचे, प्रमाण सिद्धांत और समानांतर गणना क्षेत्र के महत्वपूर्ण साहित्य का हवाला देता है, जिसमें शामिल हैं:

  • de Bruijn की Automath प्रणाली
  • Harper आदि द्वारा LF ढांचा
  • Miller आदि द्वारा λ-Prolog
  • DeYoung आदि द्वारा अर्ध-स्वयंसिद्ध अनुक्रम कलन

समग्र मूल्यांकन: यह एक नवीन सैद्धांतिक कंप्यूटर विज्ञान पेपर है, जो तार्किक ढांचे में पहली बार अनंत वस्तु समर्थन का परिचय देता है और एक नवीन समवर्ती गणना मॉडल प्रस्तावित करता है। हालांकि प्रगति रिपोर्ट के रूप में सैद्धांतिक गहराई में सुधार की गुंजाइश है, लेकिन इसके मूल विचार और प्रारंभिक कार्यान्वयन इस क्षेत्र के लिए नई अनुसंधान दिशाएं खोलते हैं।