Constructions Calculus (Thierry Coquand's Constructions Analytical Study)

Document Type : Original Article

Author

Abstract

This research explores the term construct calculus since its inception in the 6th and 17th centuries, through the 20th century and the most important additions of messengers and contemporary regions. To this day, this research examines the logical side of structural calculation. It also sheds light on the construction of "Thierry Coquand" (1961), because the term is of great importance today among the common programming languages ​​in the computer languages ​​such as LISP, ALgol, Pascal, etc., as well as its importance in mathematics. In spite of the progress of these areas, the basis remains logical From the engineering perspective of the German mathematician Eueler in the sixteenth century, the idea of ​​calculus developed into calculus. Renee Descartes discussed it in the seventeenth century with the idea of ​​solution and its influence on François Veet and the establishment of algebraic constructions. From the construction of engineering to the construction of forced, and then moved to the presentation of the term in Bertrand Russell in his view of classes and types, and addressed the idea of ​​logical atomic to turn the term construct on his hands to a logical construction, And focused on the Russell of some kind because of the logical importance that make the basis of mathematics logic according to his logistic approach, and his logical atomic article is a work in translation, which is in line with the goal of research, and then moved to the main research axis, Thierry Coquand, a computer scientist, and the transfer of the construction calculus to the programming languages. She explained how his account shed light on new terms and ideas such as Alonzo Church as the Lambda account, the Coquand revolution on what is known in the mathematics"Noetherian mathematics" founded by German mathematician Amalie Noether, and the construction of the inductive aspect of the constructions based on the typical aspect of Lambda's account. π  calculates, and other equations that govern the language and method of work of the computer, and its spread to various technological fields, given the importance it now in our daily lives, but the basis remains logical.

Main Subjects