This HTML5 document contains 61 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n17http://g.co/kg/g/
dcthttp://purl.org/dc/terms/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
n20http://www.pps.univ-paris-diderot.fr/~krivine/articles/
n9http://commons.dbpedia.org/resource/Category:
n19https://hal.inria.fr/
rdfshttp://www.w3.org/2000/01/rdf-schema#
category-frhttp://fr.dbpedia.org/resource/Catégorie:
n13http://fr.dbpedia.org/resource/Modèle:
n4http://fr.dbpedia.org/resource/Fichier:
n11http://commons.wikimedia.org/wiki/Special:FilePath/
wikipedia-frhttp://fr.wikipedia.org/wiki/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
dbpedia-frhttp://fr.dbpedia.org/resource/
prop-frhttp://fr.dbpedia.org/property/
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/

Statements

Subject Item
dbpedia-fr:Machine_de_Krivine
rdfs:label
Krivine machine Machine de Krivine
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
owl:sameAs
n9:Krivine_machine dbr:Krivine_machine wikidata:Q25380873 n17:11bwycb9tt
dbo:wikiPageID
9579033
dbo:wikiPageRevisionID
188656007
dbo:wikiPageWikiLink
n4:Machine_de_Krivine.jpg dbpedia-fr:Sémantique_des_langages_de_programmation dbpedia-fr:Informatique_théorique dbpedia-fr:Alan_Turing category-fr:Programmation_fonctionnelle category-fr:Machine_virtuelle category-fr:Modèles_de_calcul dbpedia-fr:Substitution_explicite dbpedia-fr:Olivier_Danvy category-fr:Calculabilité dbpedia-fr:Machine_SECD dbpedia-fr:Machine_abstraite dbpedia-fr:Jean-Louis_Krivine dbpedia-fr:Sémantique_opérationnelle dbpedia-fr:Programmation_fonctionnelle category-fr:Logique_mathématique dbpedia-fr:Fermeture_(informatique) dbpedia-fr:Évaluation_paresseuse dbpedia-fr:Machine_virtuelle dbpedia-fr:Réécriture_(informatique) dbpedia-fr:Machine_de_Turing_non_déterministe dbpedia-fr:Machine_de_Turing dbpedia-fr:Stratégie_d'évaluation_(informatique) category-fr:Théorie_des_automates dbpedia-fr:Lambda-calcul
dbo:wikiPageExternalLink
n19:inria-00198756 n20:lazymach.pdf
dbo:wikiPageLength
15088
dct:subject
category-fr:Machine_virtuelle category-fr:Théorie_des_automates category-fr:Modèles_de_calcul category-fr:Programmation_fonctionnelle category-fr:Calculabilité category-fr:Logique_mathématique
prop-fr:wikiPageUsesTemplate
n13:Loupe n13:Portail n13:Ouvrage n13:N° n13:Références n13:Palette
prov:wasDerivedFrom
wikipedia-fr:Machine_de_Krivine?oldid=188656007&ns=0
foaf:depiction
n11:Machine_de_Krivine.jpg
prop-fr:année
1998
prop-fr:auteur
Roberto Amadio Pierre-Louis Curien
prop-fr:collection
Cambridge Tracts in theoretical computer science
prop-fr:titre
Domains and Lambda-calculi
prop-fr:volume
45
prop-fr:éditeur
Cambridge University Press
dbo:thumbnail
n11:Machine_de_Krivine.jpg?width=300
foaf:isPrimaryTopicOf
wikipedia-fr:Machine_de_Krivine
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.