Формализация задач в условиях дедуктивного синтеза

А. П. Бельтюков

Аннотация


Описывается построение и трансформации формулировок конструктивных задач в парадигме дедуктивного синтеза их решений. Предлагается подход к построению формализации конструктивной задачи, когда уже примерно известны и неформальная постановка задачи, и неформальная идея ее решения. В этой ситуации из неформальной постановки задачи и неформальной идеи ее решения вырабатывается система понятий, положенная в основу онтологии: типы объектов в наиболее общем для данной задачи виде, конструктивные свойства-атрибуты, конструктивные отношения и спецификации исходных и целевых функций и операторов. Под дедуктивным синтезом в настоящей работе понимается логический вывод решений конструктивных задач из их формальных постановок в определенных системах вывода. Под решениями конструктивных задач здесь понимается построение алгоритмов, структур данных и объектов, содержащих как данные, так и алгоритмы. Более того, задача может быть расширена так, что частями решений могут оказаться как физические объекты, так и компетенции людей. Такие решения можно назвать физико-антропно-техническими. При этом сама система построения таких решений может оказаться физико-антропно-технической, на что и рассчитывает настоящая работа. Вместо традиционных языков логических формул рассматриваются языки спецификации задач, более подходящие для описания предметной области в информатике. Роль языков доказательств здесь играют специальные языки дедуктивного программирования. Наиболее близкое к ним понятие в логике – доказательство как терм – выражение, которое, вообще говоря, можно вычислять (выполнять). Постановке задачи предшествует изучение предметной области и выявление проблем, связанных с ней. Для формулирования задач решения выявленных проблем строится определённая терминологическая система. Для успешного использования имеющимся традиционным аппаратом конструктивного дедуктивного синтеза терминологическая система должна иметь определенную структуру конструктивной онтологии. Она состоит в том, что все термины разбиваются на три класса: термины, обозначающие типы значений, термины, обозначающие предикаты и термины, обозначающие конструктивные функции.

Ключевые слова


дедуктивный синтез; физико-антропно-технические системы; онтологии; конструктивная логика; человеко-машинные системы

Полный текст:

PDF

Литература


Kleene S. C. Introduction to metamathematics – North-Holland, 1951, 500 p.

Шанин Н. А. Об иерархии способов понимания суждений в конструктивной математике // Тр. Матем. ин-та АН СССР, 1973, т. 129, с. 203–266. [N. A. Shanin, ”On the hierarchy of ways to understand judgments in constructive mathematics”, in: “Tr. Matem. in-ta AN SSSR”, 1973, V. 129, pp. 203-266.]

Марков А. А. Попытка построения логики конструктивной математики // В сб.: Исследования по теории алгорифмов и математической логике, М., 1976, т. 2, C.3–31. [A. A. Markov, “An attempt to build a logic of constructive mathematics”. in: Research in the theory of algorithms and mathematical logic, M, 1976, V. 2, pp. 3-31.]

Бельтюков А. П. Малые сложностные классы и автоматический дедуктивный синтез алгоритмов // Известия института математики и информатики УдГУ, Ижевск, 1995, вып. 2, C. 3–89. [A. P. Beltiukov, “Small complexity classes and automatic deductive synthesis of algorithms”, in: Izvestia instituta matematiki i informatiki UdGU, Izhevsk,1995, 2, pp. 3-89.]

Optimizing synthesis with metasketches /J. Bornholt et al. // ACM SIGPLAN Notices, ACM, 2016, volume 51, pp. 775–788. [James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze “Optimizing synthesis with metasketches”. In ACM SIGPLAN Notices, volume 51, pp. 775–788. ACM, 2016.]

Measuring and synthesizing systems in probabilistic environments / K. Chatterjee, et al, // J. ACM, 62(1):9:1–9:34, March 2015. ISSN 0004-5411. [Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, and Rohit Singh “Measuring and synthesizing systems in probabilistic environments”. J. ACM, 62(1):9:1–9:34, March 2015. ISSN 0004-5411.]

Chaudhuri S., Clochard M., and A. Solar-Lezama. Bridging boolean and quantitative synthesis using smoothed proof search // ACM SIGPLAN Notices, January 2014, 49(1) pp. 207–220, ISSN 0362-1340. [S. Chaudhuri, M. Clochard, and A. Solar-Lezama “Bridging boolean and quantitative synthesis using smoothed proof search”. ACM SIGPLAN Notices, 49(1):207–220, January 2014.] ISSN 0362-1340.

Flanagan С. Hybrid type checking // ACM Sigplan Notices, volume 41, ACM, 2006, pp. 245–256. [Cormac Flanagan “Hybrid type checking”. In ACM Sigplan Notices, volume 41, pp. 245-256. ACM, 2006.]

Example-directed synthesis: a type-theoretic interpretation/J. Frankle, et al, // ACM SIGPLAN Notices, volume 51, ACM, 2016, pp. 802–815. [Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewi “Example-directed synthesis: a type-theoretic interpretation”. In ACM SIGPLAN Notices, volume 51, pp. 802-815. ACM, 2016.]

An efficient boosting algorithm for combining preferences / Freund Y., et al, // The Journal of machine learning research, 2003, 4, pp. 933–969. [Yoav Freund, Raj Iyer, Robert E. Schapire, and Yoram Singer “An efficient boosting algorithm for combining preferences”. The Journal of machine learning research, 4:933-969, 2003.]

On the complexity of teaching/Goldman S. A. and Kearns M. J. // Journal of Computer and System Sciences, 50, 1992, pp. 303–314. [Sally A. Goldman and Michael J. Kearns “On the complexity of teaching”. Journal of Computer and System Sciences, 50:303–314, 1992.]

Complete completion using types and weights / T. Gvero, et al, // In ACM SIGPLAN Notices, ACM, 2013, V. 48, pp. 27–38. [Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, and Ruzica Piskac “Complete completion using types and weights”. In ACM SIGPLAN Notices, vol. 48, pp. 27-38. ACM, 2013.]

Educational pearl: Automata via macros / S. Krishnamurthi et al // Journal of Functional Programming, 2006, 16(03), pp. 253–267. [Shriram Krishnamurthi “Educational pearl: Automata via macros”. Journal of Functional Programming, 16(03):253–267, 2006.]

A generic method for automatic software repair/ C. Le Goues, at al, // IEEE Transactions on Software Engineering, 2012, 38(1), pp. 54–72. [Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, and Westley Weimer “Genprog: A generic method for automatic software repair”. IEEE Transactions on Software Engineering, 38(1):54–72, 2012.]

Meta-interpretive learning of higher-order dyadic Datalog: Predicate invention revisited / Muggleton S., Lin D., and Tamaddoni-Nezhad A. // Machine Learning, 2015, 100(1), pp.49–73. [Stephen Muggleton, Dianhuan Lin, and Alireza Tamaddoni-Nezhad “Meta-interpretive learning of higher-order dyadic Datalog: Predicate invention revisited”. Machine Learning, 100(1):49–73, 2015.]

Efficient synthesis of probabilistic programs / A. V. Nori, et all, // ACM SIGPLAN Notices, ACM, 2015, V. 50, pp. 208–217. [Aditya V. Nori, Sherjil Ozair, Sriram K. Rajamani, and Deepak Vijaykeerthy “Efficient synthesis of probabilistic programs”. In ACM SIGPLAN Notices, vol. 50, pp. 208-217. ACM, 2015.]

Automatically improving accuracy for floating point expressions / P. Panchekha, at al. // ACM SIGPLAN Notices, 2015, 50(6), pp. 1–11. [Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock Automatically improving accuracy for floating point expressions. ACM SIGPLAN Notices, 50(6):1-11, 2015.]

Type-directed completion of partial expression / D. Perelman, at al. // In ACM SIGPLAN Notices, ACM, 2012, V. 47, pp. 275–286. [Daniel Perelman, Sumit Gulwani, Thomas Ball, and Dan Grossman “Type-directed completion of partial expressions”. In ACM SIGPLAN Notices, V. 47, pp. 275-286. ACM, 2012.]

Chlorophyll: Synthesis-aided compiler for low-power spatial architectures/ P. P. Mangpo, at al. // ACM SIGPLAN Notices, ACM, 2014, V. 49, pp. 396–407. [Phitchaya Mangpo Phothilimthana, Tikhon Jelvis, Rohin Shah, Nishant Totla, Sarah Chasins, and Rastislav Bodik “Chlorophyll: Synthesis-aided compiler for low-power spatial architectures”. In ACM SIGPLAN Notices, vol. 49, pp. 396-407. ACM, 2014.]

Raychev V., Vechev M., and Yahav E. Code completion with statistical language models // ACM SIGPLAN Notices, ACM, 2014, vol. 49, pp. 419–428. [Veselin Raychev, Martin Vechev, and Eran Yahav “Code completion with statistical language models”. In ACM SIGPLAN Notices, vol. 49, pp. 419-428. ACM, 2014.]

Learning programs from noisy data / Raychev V., at al // ACM SIGPLAN Notices, ACM, 2016, volume 51, pp. 761–774. [Veselin Raychev, Pavol Bielik, Martin Vechev, and Andreas Krause “Learning programs from noisy data”. In ACM SIGPLAN Notices, vol, 51, pp. 761–774. ACM, 2016.]

Rondon P. M., Kawaguci M., and Ranjit J. Liquid types // ACM SIGPLAN Notices, ACM, 2008, vol. 43, pp. 159–169. [Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala “Liquid types”. In ACM SIGPLAN Notices, vol. 43, pp. 159–169. ACM, 2008.]

Schkufza E., Sharma R., and Aiken A. Stochastic superoptimization // ACM SIGARCH Computer Architecture News, ACM, 2013, vol. 41, pp. 305–316. [Eric Schkufza, Rahul Sharma, and Alex Aiken Stochastic superoptimization. In ACM SIGARCH Computer Architecture News, vol. 41, pp. 305–316. ACM, 2013.]

Srivastava S., Gulwani S., and Foster J. S. Templatebased program verification and program synthesis // International Journal on Software Tools for Technology Transfer (STTT), 2013, 15(5-6), pp. 497–518. [Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster “Templatebased program verification and program synthesis”. International Journal on Software Tools for Technology Transfer (STTT), 15(5-6):497–518, 2013]

Torlak E. and Bodik R. A lightweight symbolic virtual machine for solver-aided host languages // ACM SIGPLAN Notices, ACM, 2014, vol. 49, pp. 530–541. [Emina Torlak and Rastislav Bodik “A lightweight symbolic virtual machine for solver-aided host languages”, In ACM SIGPLAN Notices, ACM, 2014, vol. 49, pp. 530–541.]

Beltiukov A. P. Intuitionistic formal theories with realizability in subrecursive classes // Annals of Pure and Applied Logic, 89, 1997, pp. 3-15. [A. P. Beltiukov “Intuitionistic formal theories with realizability in subrecursive classes” In: Annals of Pure and Applied Logic, 89, 1997, pp. 3-15.]

Beltiukov A. P. A strong induction scheme that leads to polynomially computable realizations // Theoretical Computer Science, 322 (2004), P. 17-39. [A. P. Beltiukov “A strong induction scheme that leads to polynomially computable realizations” In: Theoretical Computer Science, 322 (2004), P. 17-39.]

Beltiukov A. P., Maslov S. G. Organizing understanding in the framework of ergatic system // CSIT’2015: Proceeding of the 17th International Workshop on Computer Science and Information Technologies, Rome, Italy, September 22-26, 2015, V.1, – Ufa.: Ufa State Aviation Technical Univercity, 2015, P. 60-64. [A. P. Beltiukov, S. G. Maslov “Organizing understanding in the framework of ergatic system”. In CSIT’2015: Proceeding of the 17th International Workshop on Computer Science and Information Technologies, Rome, Italy, September 22-26, 2015, V.1, Ufa.: Ufa State Aviation Technical Univercity, 2015, P. 60-64.]


Ссылки

  • На текущий момент ссылки отсутствуют.


(c) 2019 А. П. Бельтюков