Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Séance de cours

Simply Taped Lambda Calculus: Fondements et propriétés

Concepts associés (32)

Simply typed lambda calculus

The simply typed lambda calculus (), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor () that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus. The term simple type is also used to refer extensions of the simply typed lambda calculus such as products, coproducts or natural numbers (System T) or even full recursion (like PCF).

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type (for example, integer, floating point, string) to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term.

Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church dans les années 1930, qui fonde les concepts de fonction et d'application. On y manipule des expressions appelées λ-expressions, où la lettre grecque λ est utilisée pour lier une variable. Par exemple, si M est une λ-expression, λx.M est aussi une λ-expression et représente la fonction qui à x associe M. Le λ-calcul a été le premier formalisme pour définir et caractériser les fonctions récursives : il a donc une grande importance dans la théorie de la calculabilité, à l'égal des machines de Turing et du modèle de Herbrand-Gödel.

Typed lambda calculus

A typed lambda calculus is a typed formalism that uses the lambda-symbol () to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered (see kinds below). From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus, but from another point of view, they can also be considered the more fundamental theory and untyped lambda calculus a special case with only one type.

Langage de programmation

thumb|Fragment de code écrit dans le langage de programmation JavaScript. Un langage de programmation est un langage informatique destiné à formuler des algorithmes et produire des programmes informatiques qui les appliquent. D'une manière similaire à une langue naturelle, un langage de programmation est composé d'un alphabet, d'un vocabulaire, de règles de grammaire, de significations, mais aussi d'un environnement de traduction censé rendre sa syntaxe compréhensible par la machine.