Функция түрі: информатикадағы және математикалық логикадағы функциялардың типі, параметрлер мен нәтижелер түрлерін анықтайды. Жоғары ретті функциялар үшін маңызды.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Кіріспе
Компьютерлік ғылым мен математикалық логикада функция түрі (немесе жебе түрі немесе экспонента) – функцияны тағайындауға болатын немесе функция тағайындалған айнымалының немесе параметрдің түрі, сондай-ақ функцияны қабылдайтын немесе қайтаратын жоғары деңгейлі функцияның аргументі немесе нәтиже түрі. Функция түрі параметрлердің түріне және функцияның нәтиже түріне байланысты (немесе дәлірек айтқанда, қолданылмаған типтік конструктор · → ·, жоғары ретті тип). Теориялық тұрғыда және функциялар кари формасында анықталатын бағдарламалау тілдерінде, мысалы, қарапайым типтелген лямбда-есептеуде, функция түрі дәл екі типке – A доменіне және B диапазонына байланысты. Мұнда функция түрі математикалық конвенция бойынша көбінесе A → B немесе жинақтар санатындағы A-дан B-ға сәйкестіктердің экспоненциалды саны B^(A) болатындықтан B^(A) деп белгіленеді. Мұндай сәйкестіктер немесе функциялар класы экспоненциалды объект деп аталады. Карилеу амалы функция түрін өнім түріне қосады; бұл мәселе карилеу туралы мақалада егжей-тегжейлі қарастырылады. Функция түрін тәуелді өнім түрінің ерекше жағдайы деп қарастыруға болады, ол полиморфты функция идеясын қамтиды және басқа да қасиеттерге ие.
In computer science and mathematical logic, a function type (or arrow type or exponential) is the type of a variable or parameter to which a function has or can be assigned, or an argument or result type of a higher order function taking or returning a function. A function type depends on the type of the parameters and the result type of the function (it, or more accurately the unapplied type constructor · → ·, is a higher kinded type). In theoretical settings and programming languages where functions are defined in curried form, such as the simply typed lambda calculus, a function type depends on exactly two types, the domain A and the range B. Here a function type is often denoted A → B, following mathematical convention, or B^(A), based on there existing exactly B^(A) (exponentially many) set theoretic functions mappings A to B in the category of sets. The class of such maps or functions is called the exponential object. The act of currying makes the function type adjoint to the product type; this is explored in detail in the article on currying. The function type can be considered to be a special case of the dependent product type, which among other properties, encompasses the idea of a polymorphic function.
Денотациялық семантика
Бағдарламалау тілдеріндегі функция түрі барлық теориялық функциялар кеңістігіне сәйкес келмейді. Табиғи сандардың санаулы шексіз түрін домен ретінде, ал бульдіктерді ауқым ретінде қарастырғанда, олардың арасында санаулы емес шексіз саны (2ℵ₀ = c) теориялық функциялар бар. Бұл функциялар кеңістігі кез келген бағдарламалау тілінде анықталуы мүмкін функциялар санынан үлкен екендігі анық, себебі бағдарламалардың саны санаулы (бағдарлама – символдардың шекті санының шекті тізбегі), ал теориялық функциялардың бірі тоқтау мәселесін тиімді шешеді. Денотациялық семантика функция түрлері сияқты бағдарламалау тілінің ұғымдарын модельдеуге арналған қолайлы модельдерді (домендер деп аталады) табумен айналысады. Бағдарламалау тілі аяқталмайтын есептеулерді жазуға мүмкіндік берсе (яғни бағдарламалау тілі Тьюринг толық болса), өрнекті есептеуге болатын функциялар жиынымен шектеу жеткіліксіз болып шығады. Өрнекті «жалғасты функциялар» деп аталатын функциялармен шектеу керек (Скотт топологиясындағы жалғастылыққа сәйкес келеді, нақты аналитикалық мағынадағы жалғастылыққа сәйкес келмейді). Тіпті сонда да, жалғасты функциялар жиынында барлық бағдарламалау тілдерінде дұрыс анықталмайтын параллель немесе функция бар.
The function type in programming languages does not correspond to the space of all set theoretic functions. Given the countably infinite type of natural numbers as the domain and the booleans as range, then there are an uncountably infinite number (2ℵ0 = c) of set theoretic functions between them. Clearly this space of functions is larger than the number of functions that can be defined in any programming language, as there exist only countably many programs (a program being a finite sequence of a finite number of symbols) and one of the set theoretic functions effectively solves the halting problem. Denotational semantics concerns itself with finding more appropriate models (called domains) to model programming language concepts such as function types. It turns out that restricting expression to the set of computable functions is not sufficient either if the programming language allows writing non terminating computations (which is the case if the programming language is Turing complete). Expression must be restricted to the so called continuous functions (corresponding to continuity in the Scott topology, not continuity in the real analytical sense). Even then, the set of continuous function contains the parallel or function, which cannot be correctly defined in all programming languages.