In theoretical computer science, the Krivine machine is an abstract machine (sometimes called virtual machine). As an abstract machine, it shares features with Turing machines and the SECD machine. The Krivine machine explains how to compute a recursive function. More specifically it aims to define rigorously head normal form reduction of a lambda term using call-by-name reduction. Thanks to its formalism, it tells in details how a kind of reduction works and sets the theoretical foundation of the operational semantics of functional programming languages. On the other hand, Krivine machine implements call-by-name because it evaluates the body of a β-redex before it applies the body to its parameter. In other words, in an expression (λ x. t) u it evaluates first λ x. t before applying it to
| Attributes | Values |
|---|
| rdfs:label
| - Machine de Krivine (fr)
- Krivine machine (en)
|
| rdfs:comment
| - In theoretical computer science, the Krivine machine is an abstract machine (sometimes called virtual machine). As an abstract machine, it shares features with Turing machines and the SECD machine. The Krivine machine explains how to compute a recursive function. More specifically it aims to define rigorously head normal form reduction of a lambda term using call-by-name reduction. Thanks to its formalism, it tells in details how a kind of reduction works and sets the theoretical foundation of the operational semantics of functional programming languages. On the other hand, Krivine machine implements call-by-name because it evaluates the body of a β-redex before it applies the body to its parameter. In other words, in an expression (λ x. t) u it evaluates first λ x. t before applying it to (en)
- 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)
|
| foaf:depiction
| |
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| thumbnail
| |
| has abstract
| - In theoretical computer science, the Krivine machine is an abstract machine (sometimes called virtual machine). As an abstract machine, it shares features with Turing machines and the SECD machine. The Krivine machine explains how to compute a recursive function. More specifically it aims to define rigorously head normal form reduction of a lambda term using call-by-name reduction. Thanks to its formalism, it tells in details how a kind of reduction works and sets the theoretical foundation of the operational semantics of functional programming languages. On the other hand, Krivine machine implements call-by-name because it evaluates the body of a β-redex before it applies the body to its parameter. In other words, in an expression (λ x. t) u it evaluates first λ x. t before applying it to u. In functional programming, this would mean that in order to evaluate a function applied to a parameter, it evaluates first the function before applying it to the parameter. The Krivine machine has been designed by the French logician Jean-Louis Krivine at the beginning of the 1980s. (en)
- 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)
|
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
| is Wikipage disambiguates
of | |
| is foaf:primaryTopic
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)
