About: Subject reduction

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.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.

Property Value
dbo: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)
dbo:wikiPageID
  • 33471233 (xsd:integer)
dbo:wikiPageLength
  • 1714 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1083665115 (xsd:integer)
dbo:wikiPageWikiLink
dbp:wikiPageUsesTemplate
dcterms:subject
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)
rdfs:label
  • Subject reduction (en)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License