About: Subject reduction     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : owl:Thing, within Data Space : dbpedia.org associated with source document(s)
QRcode icon
http://dbpedia.org/describe/?url=http%3A%2F%2Fdbpedia.org%2Fresource%2FSubject_reduction&graph=http%3A%2F%2Fdbpedia.org&graph=http%3A%2F%2Fdbpedia.org

In type theory, a type system has the property of subject reduction (also subject evaluation, type preservation or simply preservation) if evaluation of expressions does not cause their type to change. Formally, if Γ ⊢ e1 : τ and e1 → e2 then Γ ⊢ e2 : τ. Intuitively, this means one would not like to write a expression, in say Haskell, of type Int, and have it evaluate to a value v, only to find out that v is a string. Together with , it is an important meta-theoretical property for establishing type soundness of a type system.

AttributesValues
rdfs:label
  • Subject reduction (en)
rdfs:comment
  • In type theory, a type system has the property of subject reduction (also subject evaluation, type preservation or simply preservation) if evaluation of expressions does not cause their type to change. Formally, if Γ ⊢ e1 : τ and e1 → e2 then Γ ⊢ e2 : τ. Intuitively, this means one would not like to write a expression, in say Haskell, of type Int, and have it evaluate to a value v, only to find out that v is a string. Together with , it is an important meta-theoretical property for establishing type soundness of a type system. (en)
dcterms:subject
Wikipage page ID
Wikipage revision ID
Link from a Wikipage to another Wikipage
sameAs
dbp:wikiPageUsesTemplate
has abstract
  • In type theory, a type system has the property of subject reduction (also subject evaluation, type preservation or simply preservation) if evaluation of expressions does not cause their type to change. Formally, if Γ ⊢ e1 : τ and e1 → e2 then Γ ⊢ e2 : τ. Intuitively, this means one would not like to write a expression, in say Haskell, of type Int, and have it evaluate to a value v, only to find out that v is a string. Together with , it is an important meta-theoretical property for establishing type soundness of a type system. The opposite property, if Γ ⊢ e2 : τ and e1 → e2 then Γ ⊢ e1 : τ, is called subject expansion. It often does not hold as evaluation can erase ill-typed sub-terms of an expression, resulting in a well-typed one. (en)
prov:wasDerivedFrom
page length (characters) of wiki page
foaf:isPrimaryTopicOf
is Link from a Wikipage to another Wikipage of
is Wikipage redirect of
is Wikipage disambiguates of
is foaf:primaryTopic of
Faceted Search & Find service v1.17_git139 as of Feb 29 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 08.03.3330 as of Mar 19 2024, on Linux (x86_64-generic-linux-glibc212), Single-Server Edition (378 GB total memory, 67 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software