From philosophy to computation: how Russell’s type theory impacts programming languages
Type theory introduced by Russell and Whitehead to overcome a paradox found in Frege’s work. The design of lambda-calculus in functional programming languages. The isomorphism between concepts of logic and concepts in type theory and programming.
| Рубрика | Программирование, компьютеры и кибернетика |
| Вид | статья |
| Язык | английский |
| Дата добавления | 22.02.2021 |
| Размер файла | 135,3 K |
Отправить свою хорошую работу в базу знаний просто. Используйте форму, расположенную ниже
Студенты, аспиранты, молодые ученые, использующие базу знаний в своей учебе и работе, будут вам очень благодарны.
Type ::= ... | QuantifiedType QuantifiedType ::= VA. T ype | Universal Quantification EA. Type | Existential Quantification VAcType. Type | EAcType. Type Bounded Quantification
As shown above, this notion uses quantifiers over an interval of subtypes of a specific type. Bounded quantification, which connects subtyping with parametric polymorphism, improves lambda-calculus. In fact, inheritance is used in a way that subtypes are created as specialized entities regarding the supertypes.
In other words, in object-oriented languages types are defined as bounded quantification, and can be seen as supertypes allowing the creation of subtypes by inheritance.
The lambda-calculus improved by these different notions (polymorphism, inheritance, etc.) and supporting well the type systems can perfectly model important programming principles such as data abstractions.
Conclusion
In this paper we have seen how a challenging philosophical question aimed to prove the logicism position in the philosophy of Mathematics has led Russell and Whitehead to develop the type theory. It failed to realize this objective, but succeeded in building involuntarily major foundations in computer science. Practically, type systems are used to detect errors in computer programs before appearing as runtime errors which are more critical. This kind of program-analysis has drastically improved the software quality. In addition, type theory has been fundamental in building type checking algorithms in the semantic stage of the languages compilers design [7, p.4].
Hence, as mentioned in [7, p.2], three central domains where type theory is inevitably used are the typed programming languages, the type-driven program analysis and optimization, and type-aided security mechanisms.
Furthermore, the theoretical studies of type theory have been used as mathematical basis to the Church' typed lambda-calculus and the intuitionistic type theory developed by Per Martin-Lцf [11]. Other fundamental theoretical results, such as the Curry-Howard isomorphism, have shown during decades their importance in practical use of computer science in general, and in the design of automated theorem proving and formal verification in particular.
russell logicism programming language
References
1. Gottlob Frege 1879. Begriffsschrift, Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, English translation in Jean van Heijenoort (ed.), From Frege to Gцdel: A Source Book in Mathematical Logic, 1879-1931, Harvard University Press, pp. 1-82, 1977.
2. Alfred North Whitehead and Bertrand Russell. Principia Mathematica. 1910-1913. Cambridge University Press, Cambridge, revised edition, 19251927.
3. Kurt Gцdel. 1934. On undecidable propositions of formal mathematical systems.
4. Reprinted with revisions in Davis (1965), 39-74.
5. Donald Gillies. 2002. Logicism and the development of computer science, A. C. Kakas and F. Sadri (eds,): Computational Logic, Springer-verlag Berlin Heidelberg, pp. 588-604.
6. Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, and Victor Vianu. 2001. On the Unusual Effectiveness of Logic in Computer Science, The Bulletin of Symbolic Logic, volume 7, issue 2, pp. 213-236.
7. Luca Cardelli, Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. Computing Surveys, Vol 17 n. 4, pp 471-522.
8. Cйsar Munoz. 1999. Type Theory and Its Applications to Computer Science. News Letter of the Institute for Computer Applications in Science and Engineering (ICASE), Vol. 8, No. 4.
9. Alonso Church. 1940. A Formulation of the Simple Theory of Types, Journal of Symbolic Logic, 5, pp. 56 68.
10. Robin Milner. 1977. A theory of type polymorphism in programming. J. Comp. Syst. Scs., 17:348-375.
11. Robert L. Constable. 2011. The Triumph of Types: Creating a Logic of Computational Reality. Cornell university. www.semanticscholar.org
12. Per Martin-Lцf. 1984. Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, Naples, Italy.
Размещено на Allbest.ru
...Подобные документы
Написaние прoграммы, выполняющей трансляцию с языка программирования Пaскaль нa язык прoгрaммирoвaния Си и транслирующей конструкции, такие кaк integer, repeat … until Le, procedure, type, record для type. Обработка арифметических и логических выражений.
курсовая работа [314,3 K], добавлен 03.07.2011Формализованное описание закона Pearson Type V. Характеристика методов получения выборки с распределением Pearson Type V. Исследование временных рядов с шумом заданным Rayleigh. Экспериментальное исследование средней трудоемкости Pirson Type V и Rayleigh.
курсовая работа [4,5 M], добавлен 20.06.2010Использование в программах, написанных на языке C, Windows application programming interfaces. Роль центрального процессора. Архитектура Фон Неймана. Оперативная память. Графическая плата. Создание интерфейса программы. Разработка машинного кода.
реферат [101,5 K], добавлен 15.05.2014Составление транслятора на языке С для перевода кода программы из языка Pascal в код программы на языке Cи. Распознавание и перевод конструкций: for, type, function, integer. Вешняя спецификация, описание, структура, текст программы; распечатка текстов.
курсовая работа [287,8 K], добавлен 24.06.2011Creation of the graphic program with Visual Basic and its common interface. The text of program code in programming of Visual Basic language creating in graphics editor. Creation of pictures in Visual Basic, some graphic actions with graphic editor.
лабораторная работа [1,8 M], добавлен 06.07.2009Lines of communication and the properties of the fiber optic link. Selection of the type of optical cable. The choice of construction method, the route for laying fiber-optic. Calculation of the required number of channels. Digital transmission systems.
дипломная работа [1,8 M], добавлен 09.08.2016Social network theory and network effect. Six degrees of separation. Three degrees of influence. Habit-forming mobile products. Geo-targeting trend technology. Concept of the financial bubble. Quantitative research method, qualitative research.
дипломная работа [3,0 M], добавлен 30.12.2015The solving of the equation bose-chaudhuri-hocquenghem code, multiple errors correcting code, not excessive block length. Code symbol and error location in the same field, shifts out and fed into feedback shift register for the residue computation.
презентация [111,0 K], добавлен 04.02.2011Проектирование базы данных "Учет товаров на складе". Сущность типа связи "один – к – одному", "один – ко – многим". Реализация базы данных на компьютере. Define Secondary Indexes. Взаимосвязанные таблицы информационной части в формате "Paradox 7.0".
контрольная работа [713,0 K], добавлен 18.05.2014Розробка принципової електричної схеми системи управління конвеєрною лінією, яка складається з трьох послідовних конвеєрів. Реалізація алгоритму роботи на мові сходинкових діаграм LD. Розробка керуючої програми для мікроконтролерів Zelio Logic та ОВЕН.
курсовая работа [230,2 K], добавлен 15.06.2015Окно для работ с Design Assistant. Пример комбинационной логики, используемой в качестве тактового сигнала. Условия эффективного снижения энергопотребления с помощью сигнала синхронизации, полученного при помощи логической ячейки. Вкладка Fitter Settings.
курсовая работа [562,7 K], добавлен 05.11.2014История образования ТОО "ABC Design". Разработка программного и информационного обеспечения компьютерных сетей, автоматизированных систем вычислительных комплексов и сервисов. Работа с CRM системой Task Manager и с панелью управления сайтов JOOMLA.
отчет по практике [727,4 K], добавлен 13.07.2017Рассмотрение особенностей структурного разбиения предметной области. Характеристика функциональной и информационной модели бизнес-процессов предметной области. Построение IDEF0- и IDEF1Х-модели заданной предметной области с помощью пакета Design/IDEF.
контрольная работа [486,5 K], добавлен 08.06.2019Структура економічної інформації підприємства, її основні елементи та їх взаємозв’язок. Структуризація економічної інформації. Класифікація та різновиди інформаційних систем. Особливості СУБД Approach, Paradox, Access, перспективи їх подальшого розвитку.
контрольная работа [28,9 K], добавлен 27.07.2009Расчет трудоемкости алгоритма. Определение быстродействия процессора. Характеристика контроллеров серии Direct Logic DL. Устройства, которые вошли в структуру системы. Выбор программного обеспечения. Расчет работоспособности и надежности системы.
курсовая работа [2,0 M], добавлен 14.01.2013Информация, хранящаяся в наших компьютерах, главное содержание, принципы построения и требования к ней. Основные методы учета рисков при анализе проектов. Теория Нечеткой Логики (Fuzzy Logic), направления и специфика применения с помощью пакета Matlab.
контрольная работа [2,9 M], добавлен 06.10.2014Обоснование выбора средств разработки приложения. Добавление, удаление, редактирование информации. Отражение информации из базы данных. Поиск информации по выбранной таблице. Проекты Data, Entity, Logic, Firm. Схема взаимодействия проектов программы.
курсовая работа [1,8 M], добавлен 18.01.2015Проектирование экспертной системы выбора нейронной сети. Сущность семантических сетей и фреймов. MatLab и системы Фаззи-регулирования. Реализация программы с использованием пакета fuzzy logic toolbox системы MatLab 7. Составление продукционных правил.
курсовая работа [904,4 K], добавлен 17.03.2016Структурированные кабельные сети. Универсальная среда передачи информации, объединяющая локальные вычислительные и телефонные сети, системы безопасности, видеонаблюдения. Деятельность компании Step Logic. Применение программ Raster Desk и PlanTracer.
доклад [597,2 K], добавлен 24.02.2013Основные направления деятельности компании Step Logic в области сетевой интеграции. Использование растрового изображения в качестве подложки. Особенности применение программы Raster Desk и PlanTracer. Отключение видимости при распознавании объекта.
доклад [599,1 K], добавлен 04.04.2013
