تولید طرح‌ها از اثبات‌ها ۲۰۲۲
Generating Plans from Proofs 2022

بازنویسی پرس‌وجو به فرآیند ترجمه‌ی یک پرس‌وجوی مبدأ – درخواستی برای اطلاعات به زبانی سطح بالا و مبتنی بر منطق – به یک طرح هدف اشاره دارد که از محدودیت‌های رابط کاربری خاصی پیروی می‌کند. بسیاری از مسائل عملی در مدیریت داده‌ها را می‌توان به عنوان نمونه‌هایی از مسئله‌ی بازنویسی در نظر گرفت. به عنوان مثال، مسئله‌ی ترجمه‌ی یک پرس‌وجوی SQL که بر روی مجموعه‌ای از جداول پایه نوشته شده، به یک پرس‌وجوی دیگر که بر روی مجموعه‌ای از نماها (views) نوشته شده است؛ مسئله‌ی پیاده‌سازی یک پرس‌وجو از طریق ترجمه به برنامه‌ای که مجموعه‌ای از APIهای پایگاه داده را فراخوانی می‌کند؛ مسئله‌ی پیاده‌سازی یک پرس‌وجو با استفاده از مجموعه‌ای از سرویس‌های وب.

در این کتاب، ما به بازنویسی پرس‌وجو در یک محیط بسیار کلی می‌پردازیم که شامل همه‌ی مسائل فوق می‌شود، و آن را به خطی از تحقیقات در منطق ریاضی مرتبط می‌کنیم. برای دهه‌ها، منطق‌دانان به مسئله‌ی تبدیل “تعاریف ضمنی” به “تعاریف صریح” با استفاده از رویکردی به نام درون‌یابی (interpolation) پرداخته‌اند. ما نظریه‌ی درون‌یابی را بررسی خواهیم کرد و ارتباط نزدیک آن را با بازنویسی پرس‌وجو توضیح خواهیم داد. ما به طور مفصل به نحوه‌ی استفاده از رویکرد مبتنی بر درون‌یابی برای تولید ترجمه‌ها بین پرس‌وجوهای مبتنی بر منطق بر روی واژگان مختلف، و همچنین نحوه‌ی استفاده از آن برای رفتن از پرس‌وجوهای مبتنی بر منطق به برنامه‌ها خواهیم پرداخت.

Query reformulation refers to a process of translating a source query—a request for information in some high-level logic-based language—into a target plan that abides by certain interface restrictions. Many practical problems in data management can be seen as instances of the reformulation problem. For example, the problem of translating an SQL query written over a set of base tables into another query written over a set of views; the problem of implementing a query via translating to a program calling a set of database APIs; the problem of implementing a query using a collection of web services. In this book we approach query reformulation in a very general setting that encompasses all the problems above, by relating it to a line of research within mathematical logic. For many decades logicians have looked at the problem of converting “implicit definitions” into “explicit definitions,” using an approach known as interpolation. We will review the theory of interpolation, and explain its close connection with query reformulation. We will give a detailed look at how the interpolation-based approach is used to generate translations between logic-based queries over different vocabularies, and also how it can be used to go from logic-based queries to programs.