Некоторые приложения лямбда-исчислений с типами к атрибутным вычислениям в системах категорных преобразований графов
Ключевые слова:
теория категорий, универсальный квадрат, лямбда-исчисление, переписывание атрибутных графовАннотация
Рассматриваются преобразования моделей на основе преобразований атрибутных графов. Исследуется подход одинарного универсального квадрата (single pushout) для применения правил преобразования в категории атрибутных графов. Преобразование атрибутов задается при помощи лямбда-исчисления с индуктивными типами. Предлагаются решения, позволяющие работать с конструкцией одинарного универсального квадрата для преобразования структуры графа и атрибутных вычислительных функций. Использование индуктивных типов повышает выразительность и эффективность атрибутных вычислений по сравнению с известным подходом на основе сигма-алгебр. Приводится ряд примеров, демонстрирующих особенности предлагаемого подхода.Литература
Boisvert, B., Feraud, L., and Soloviev, S. Typed lambdaterms in categorical graph rewriting // In The International Conference Polynomial Computer Algebra, April 18-22, Saint-Petersburg, Russia, Euler International Mathematical Institute.
Chemouil, D. Isomorphisms of simple inductive types through extensional rewriting. Math. Structures in Computer Science, 15(5), pages 875-917.
Ehrig, H. Introduction to the algebraic theory of graph grammars (a survey). In Graph-Grammars and Their Application to Computer Science and Biology, 1978, pages 1-69.
Ehrig, H., Ehrig, K., Prange, U., and Taentzer, G. Fundamentals of Algebraic Graph Transformation (Monographs in Theoretical Computer Science. An EATCS Series). Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2006
Ehrig, H., Padberg, J., Prange, U., and Habel, A. Adhesive high-level replacement systems: A new categorical framework for graph transformation. Fundam. Inf., 2006, 74(1):1-29.
Lowe, M., editor Algebraic approach to single pushout graph transformation // TCS, 1993, volume 109.
Luo, Z. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford University Press, USA, 1994
Orejas, F. Symbolic graphs for attributed graph constraints // J. Symb. Comput., 2011, 46:294-315.
Rebout, M., Feraud, L., Marie-Magdeleine, L., Soloviev, S. Computations in Graph Rewriting: Inductive types and Pullbacks in DPO Approach. In Szmuc, T., Szpyrka, M., and Zendulka, J., editors, Advances in Software Engineering Techniques, CEE-SET 2009, Krakow, Poland, October 2009, volume 7054 of LNCS, pages 150163. Springer- Verlag.
Rebout, M., Feraud, L., Soloviev, S. A Unied Categorial Approach for Attributed Graph Rewriting. In Hirsch, E. And Razborov, A., editors, International Computer Science Symposium in Russia (CSR 2008), Moscou 07/06/2008-12/06/2008, volume 5010 of LNCS, pages 398-410. Springer-Verlag.
Rozenberg, G., editor Handbook of Graph Grammars and Computing by Graph Transformations, 1997, Volume 1: Foundations. World Scientic.
Tran, H. N., Percebois, C., Abou Dib, A., Feraud, L., Soloviev, S. Attribute Computations in the DPoPb Graph Transformation Engine (regular paper). In GRABATS 2010, University of Twente, Enschede, The Netherlands, 28/09/2010-28/09/2010, page (electronic medium), http://www.utwente.nl/en. University of Twente.
Chemouil, D. Isomorphisms of simple inductive types through extensional rewriting. Math. Structures in Computer Science, 15(5), pages 875-917.
Ehrig, H. Introduction to the algebraic theory of graph grammars (a survey). In Graph-Grammars and Their Application to Computer Science and Biology, 1978, pages 1-69.
Ehrig, H., Ehrig, K., Prange, U., and Taentzer, G. Fundamentals of Algebraic Graph Transformation (Monographs in Theoretical Computer Science. An EATCS Series). Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2006
Ehrig, H., Padberg, J., Prange, U., and Habel, A. Adhesive high-level replacement systems: A new categorical framework for graph transformation. Fundam. Inf., 2006, 74(1):1-29.
Lowe, M., editor Algebraic approach to single pushout graph transformation // TCS, 1993, volume 109.
Luo, Z. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford University Press, USA, 1994
Orejas, F. Symbolic graphs for attributed graph constraints // J. Symb. Comput., 2011, 46:294-315.
Rebout, M., Feraud, L., Marie-Magdeleine, L., Soloviev, S. Computations in Graph Rewriting: Inductive types and Pullbacks in DPO Approach. In Szmuc, T., Szpyrka, M., and Zendulka, J., editors, Advances in Software Engineering Techniques, CEE-SET 2009, Krakow, Poland, October 2009, volume 7054 of LNCS, pages 150163. Springer- Verlag.
Rebout, M., Feraud, L., Soloviev, S. A Unied Categorial Approach for Attributed Graph Rewriting. In Hirsch, E. And Razborov, A., editors, International Computer Science Symposium in Russia (CSR 2008), Moscou 07/06/2008-12/06/2008, volume 5010 of LNCS, pages 398-410. Springer-Verlag.
Rozenberg, G., editor Handbook of Graph Grammars and Computing by Graph Transformations, 1997, Volume 1: Foundations. World Scientic.
Tran, H. N., Percebois, C., Abou Dib, A., Feraud, L., Soloviev, S. Attribute Computations in the DPoPb Graph Transformation Engine (regular paper). In GRABATS 2010, University of Twente, Enschede, The Netherlands, 28/09/2010-28/09/2010, page (electronic medium), http://www.utwente.nl/en. University of Twente.
Опубликован
2012-12-01
Как цитировать
Баранов, С. Н., Буавер, Б., Соловьев, С. В., & Феро, Л. (2012). Некоторые приложения лямбда-исчислений с типами к атрибутным вычислениям в системах категорных преобразований графов. Труды СПИИРАН, 4(23), 296-323. https://doi.org/10.15622/sp.23.15
Раздел
Статьи
Авторы, которые публикуются в данном журнале, соглашаются со следующими условиями:
Авторы сохраняют за собой авторские права на работу и передают журналу право первой публикации вместе с работой, одновременно лицензируя ее на условиях Creative Commons Attribution License, которая позволяет другим распространять данную работу с обязательным указанием авторства данной работы и ссылкой на оригинальную публикацию в этом журнале.
Авторы сохраняют право заключать отдельные, дополнительные контрактные соглашения на неэксклюзивное распространение версии работы, опубликованной этим журналом (например, разместить ее в университетском хранилище или опубликовать ее в книге), со ссылкой на оригинальную публикацию в этом журнале.
Авторам разрешается размещать их работу в сети Интернет (например, в университетском хранилище или на их персональном веб-сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению, а также к большему количеству ссылок на данную опубликованную работу (Смотри The Effect of Open Access).
