Есть ли теория / абстракция за ООП?

Функциональное программирование имеет очень элегантное Lambda Calculus и его варианты в качестве теории резервного копирования. Есть ли такая вещь для ООП? Что такое абстракция для объектно-ориентированной модели?

Существует четыре основных подхода, хотя они лишь затрагивают поверхность того, что доступно:

• через лямбды и записи: идея состоит в том, чтобы кодировать объекты, классы и методы в терминах более традиционных конструкций. Работа Бенджамина Пирса с середины 90-х годов является представителем этого подхода.
• Объектные исчисления Абади и Карделли (см. Книгу Абади и Карделли « Теория объектов» : их основная абстракция - это запись методов, и этот подход ближе к реализации объектно-ориентированного программирования на основе прототипов, хотя классы и наследование могут кодироваться в условия более примитивных элементов.
• Мультиметодное исчисление Кастаньи (см. Книгу Кастаньи « Объектно-ориентированное программирование единой основы» ): его подход использует мультиметоды как ключевую абстракцию.
• Основанные на классах исчисления (такие как в книге Кима Брюса « Основы объектно-ориентированных языков: типы и семантика или легковесная Java» ): эти подходы направлены на то, чтобы охватить суть программирования на основе классов и сосредоточиться на классах и наследовании.

Связь между ядром объектной модели и теорией множеств описана в следующих документах:

• Членство в объекте: основная структура технологии объекта
• Членство в объекте - Базовая структура
• Что такое метакласс?

Документы представляют структуру отношений экземпляра и наследования между объектами. Такую структуру можно считать максимально возможной абстракцией ООП. Показано, как структура применяется к конкретным языкам программирования (Ruby, Python, Java, Scala, Smalltalk-80, Objective-C, CLOS, Perl, Dylan, JavaScript), а также к языкам онтологии (RDF Schema и OWL 2 Full).

В документах классы являются объектами подхода, принятого таким образом, что базовая структура является односортированной. В основном виде структура может быть выражена как (O, ϵ , ≤, .ec) где

• O - множество объектов ,
• ϵ - это (объектное) членское отношение, уточнение отношения экземпляра ,
• ≤ отношение наследования , и
• .ec является картой powerclass, которая является выделенной, возможно пустой, взаимосвязью ϵ.

Пример структуры ядра в соответствии с объектной моделью Ruby показан на следующей диаграмме. Зеленые ссылки показывают отношение наследования в рефлексивном переходном сокращении, синие ссылки показывают отношение членства в «сокращении потребления» - голубая ссылка от x указывает на наименьший контейнер x . Карта powerclass .ec состоит из горизонтальных синих ссылок. Объекты с изображения этой карты - классы мощности (серого цвета). В Ruby их называют собственными классами или также синглтон-классами (последний термин довольно устарел). Объекты s , u и v (розовые) являются терминальнымиостальные объекты являются потомками корня наследования r .

  r = BasicObject; c = Class; A = c.new(r); B = c.new(A); s = A.new; u = B.new; v = B.new; class << s; end; class << v; end

Основные части объектной модели всех вышеперечисленных языков можно рассматривать как специализации структуры без каких-либо дополнительных компонентов или только с их несколькими. С теоретической точки зрения наиболее значимым случаем дополнительной составляющей является одноэлементное отображение (обозначено .ɛϲ ), введенное Диланом. Это делает Dylan единственным языком программирования (из вышеупомянутого), который не подчиняется условию монотонности (≤) ○ (ϵ) ⊆ (ϵ), где символ композиции ○ интерпретируется слева направо.

Одним из способов формализовать связь между ядром объектной модели и теорией множеств является использование семейства структур (O, ≤, r, .ec, .ɛϲ), называемых структурами метаобъектов в ссылочных документах, поскольку можно рассмотреть x.ec или x.ɛϲ как метаобъекты х . В этих структурах x.ec определен для каждого объекта x, а x.ɛϲ определен для каждого ограниченного («маленького») объекта x . Структуры подчиняются девяти аксиомам ниже. Аксиоматизация использует определение дефиниции, которое довольно просто для первых восьми аксиом ( Tобозначает множество терминальных объектов - тех, которые не являются потомками r , а .ec ^∗ является рефлексивным транзитивным замыканием .ec ), а скорее задействованы для последней аксиомы.

1. Наследование ≤ является частичным порядком.
2. Отображение степенного класса, .ec , является вложением порядка (O, ≤) в себя.
3. Объекты из T.ec ^∗ минимальны.
4. Каждый powerclass является потомком r .
5. Множество r.ec ^∗ не имеет нижней границы.
6. Одиночное отображение, .ɛϲ , инъективно.
7. Объекты из O.ɛϲ.ec ^∗ минимальны.
8. Для каждых объектов х , у , такие , что x.ɛς определено, x.ɛς ≤ y.ec ↔ х ≤ у .
9. Для каждого объекта х , x.ɛς определяется ↔ XD <π .

В последней аксиоме ϖ - фиксированный предельный ординал, а .d - функция ранга, полученная из дефиниционного расширения. Отношение принадлежности к объекту, ϵ, получается как (( .ɛϲ ) ∪ ( .ec )) ○ (≤). Согласно последней аксиоме, ограничение области ϵ на множество ограниченных объектов равно ( .ɛϲ ) ○ (≤). В ссылочных документах это отношение называется ограниченным членством и обозначается ∊. В качестве существенной характеристики это соотношение является обоснованным. Это в отличие от ϵ, который не является обоснованным, так как r ϵ r, Оказывается, что основное соответствие между (основной частью) объектной технологии и теорией множеств можно выразить как

↔ ↔ ∈

т.е. ограниченное членство соответствует множеству принадлежностей между обоснованными множествами. Как частный случай, частичная вселенная фон Неймана ранга ϖ + 1 является структурой метаобъекта по определению расширения. В общем, любая абстрактная ( ϖ + 1 ) - надстройка (O, ∊ ) по определению эквивалентна полной структуре метаобъекта. Каждая структура метаобъекта может быть точно встроена в целостную структуру метаобъекта, которая, в свою очередь, может быть точно встроена во вселенную фон Неймана.

Термин базовая структура используется для обобщения структур метаобъектов. В этом обобщении .ec и .ɛϲ могут быть (произвольно) частичными, возможно, пустыми. В частности, возможны конечные базовые структуры с минимальной структурой, содержащей только корень наследования r . Каждая базовая структура может быть расширена до структуры метаобъекта с помощью дополнения PowerClass, за которым следует одноэлементное завершение, что, в свою очередь, делает базовые структуры достоверно встраиваемыми во вселенную фон Неймана.