ctaipe
valsi
ctaipe
type
fu'ivla
creator
time entered
Sat Jun 14 08:31:40 2014
English
Definition #67782 - Preferred
definition
x1 is a value / proof of type / proposition x2 under context x3 in (type / logical) system x4.
notes
Types and propositions are considered equivalent due to the Curry-Howard correspondence. Compare to mathematical notation: " MATH
$x_3 \vdash x_1 : x_2$
x3 <img alt="$\vdash$" src="/jbovlaste_export/56MMWcQ56x/img1.png" style="height: 1.61ex; vertical-align: -0.12ex; "/> x1 : x2", with x4 implied by context. In proof-irrelevant work (e.g, classical logic), this is usually written " MATH
$x_3 \vdash x_2$
x3 <img alt="$\vdash$" src="/jbovlaste_export/56MMWcQ56x/img1.png" style="height: 1.61ex; vertical-align: -0.12ex; "/> x2". x1 is most likely to be filled by a li construct, or something that potentially reduces to a mathematical expression. Quoted arguments should be dereferenced with la'e or similar. x1 can be filled by zi'o, which means that the proposition is unprovable. x2 can be filled by a set of which the x1 value is a member. It may be convenient to interpret lo'i as the gadri for types. x3 will be a conjunction of du'u sumti, each possibly containing a bridi based on ctaipe. x4 need not be consistent. For example, almost every programming language has an inconsistent type system (by virtue of being Turing-equivalent).
jargon type
type theory (computer science) & proof theory (mathematics/philosophy)
gloss words
place keywords
1.
value/proof
2.
type/proposition
3.
context ; type theory/proof theory
4.
type system/logic
created by
vote information
3
time
Sun Sep 6 19:01:57 2015
Definition #56829
definition
x1 is an object/construct fulfilling grammatical role/of (syntactic) category x2 with (sub)typing/data type/of selma'o x3, having specific properties/features/definition x4
notes
Quote versus la'e+quote is important in x1; x2 can have arguments of "brivla", "sumti", "cmavo", etc.. Type error results from contextual abuse of x3. See also: klerctaipe, klesi
gloss words
created by
vote information
0
time
Sat Jun 14 08:31:40 2014
Examples
Definition #67525
definition
x1 is a value/proof of type/proposition x2 in (type/logical) system x3
notes
A better definition; proposed by la .mudri.
gloss words
created by
vote information
0
time
Sun Sep 6 19:04:20 2015
Examples