Machine de Krivine
ordinateur virtuel pour évaluer des fonctions / De Wikipedia, l'encyclopédie encyclopedia
Cher Wikiwand IA, Faisons court en répondant simplement à ces questions clés :
Pouvez-vous énumérer les principaux faits et statistiques sur Machine de Krivine?
Résumez cet article pour un enfant de 10 ans
En informatique théorique, la machine de Krivine est une machine abstraite au même titre que les machines de Turing ou que la machine SECD avec laquelle elle partage un certain nombre de spécificités. Elle explique comment calculer une fonction récursive. Plus précisément, elle sert à définir rigoureusement la réduction en forme normale de tête d'un terme du lambda-calcul en utilisant la réduction par appel par nom[1]. À ce titre, elle explique en détail comment se passe une certaine forme de réduction et sert de support théorique à la sémantique opérationnelle des langages de programmation fonctionnelle.
D'autre part, elle implémente l'appel par nom, parce qu'elle évalue le corps d'un β-redex[2] avant d'en évaluer le paramètre, autrement dit dans une expression (λ x. t) u elle évalue d'abord λ x. t avant d'évaluer u. En programmation fonctionnelle cela voudrait dire que pour évaluer une fonction appliquée à un paramètre, on évalue d'abord la partie fonction avant d'évaluer le paramètre.
La machine de Krivine a été inventée par le logicien français Jean-Louis Krivine au début des années 1980.