| Property |
Value |
| dbo:abstract
|
- En informatique théorique, la machine de Krivine est une machine abstraite (on peut aussi dire une machine virtuelle) 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. À 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 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. (fr)
- En informatique théorique, la machine de Krivine est une machine abstraite (on peut aussi dire une machine virtuelle) 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. À 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 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. (fr)
|
| dbo:thumbnail
| |
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 15088 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| prop-fr:année
| |
| prop-fr:auteur
|
- Pierre-Louis Curien (fr)
- Roberto Amadio (fr)
- Pierre-Louis Curien (fr)
- Roberto Amadio (fr)
|
| prop-fr:collection
|
- Cambridge Tracts in theoretical computer science (fr)
- Cambridge Tracts in theoretical computer science (fr)
|
| prop-fr:titre
|
- Domains and Lambda-calculi (fr)
- Domains and Lambda-calculi (fr)
|
| prop-fr:volume
| |
| prop-fr:wikiPageUsesTemplate
| |
| prop-fr:éditeur
|
- Cambridge University Press (fr)
- Cambridge University Press (fr)
|
| dct:subject
| |
| rdfs:comment
|
- En informatique théorique, la machine de Krivine est une machine abstraite (on peut aussi dire une machine virtuelle) 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. À 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 avant d'en évaluer le paramètre, autrement dit dans une ex (fr)
- En informatique théorique, la machine de Krivine est une machine abstraite (on peut aussi dire une machine virtuelle) 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. À 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 avant d'en évaluer le paramètre, autrement dit dans une ex (fr)
|
| rdfs:label
|
- Krivine machine (en)
- Machine de Krivine (fr)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:depiction
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageWikiLink
of | |
| is oa:hasTarget
of | |
| is foaf:primaryTopic
of | |
