Changes between Version 8 and Version 9 of KindFact


Ignore:
Timestamp:
Aug 19, 2011 4:18:12 PM (4 years ago)
Author:
illissius
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • KindFact

    v8 v9  
    8181 
    8282{{{Fact}}} is the working name for the new kind. {{{Constraint}}} is an obvious contender, but long. {{{Prop}}} should ''not'' be used, as any analogy to Prop in the Calculus of Constructions would be bogus: proofs of a Prop are computationally irrelevant and discarded by program extraction, but witnesses to a Fact are material and computationally crucial. Another thought: 'Constraint' sounds more like a requirement than a guarantee, whereas 'Fact' is neutral. On the other hand, the kinding {{{F :: Fact}}} might be misleadingly suggestive of {{{F}}}'s truth, over and above its well-formedness. 
     83 
     84[illissius] I checked thesaurus.com for (even remotely) plausible names, and this is what I found: 
     85 * Fact, Knowledge, Information, Data, Evidence, Proof 
     86 * Requirement, Constraint, Guarantee, Promise, Contract 
     87 * Characteristic, Attribute, Property, Trait, Capability 
     88 * Axiom, Lemma, Theorem, Proposition, Postulate, Premise, Claim, Posit