- Home
- Get A Printable Dictionary
- Search Best Words
- Recent Changes
- How You Can Help
- valsi - All
- valsi - Preferred Only
- natlang - All
- natlang - Preferred Only
- Languages
- XML Export
- user Listing
- Report Bugs
- Utilities
- Status
- Help
- Admin Request
- Create Account
|
| valsi |
ctaipe |
| type |
fu'ivla |
| creator |
krtisfranks |
| time entered |
Sat Jun 14 08:31:40 2014 |
Examples
| |
|
English
|
|
Definition #67782
- Preferred
[edit]
| |
|
| 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: "
x3  x1 : x2", with x4 implied by context. In proof-irrelevant work (e.g, classical logic), this is usually written "
x3 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 |
mudri |
| vote information |
2
|
| time |
Sun Sep 6 19:01:57 2015 |
|
|
|
Examples
-
|
Example #1:
|
li no ctaipe lo'i kacna'u
|
(by mudri)
|
[edit]
|
-
|
Example #2:
|
li bai'ei xy. ctaipe lo'i kacna'u lo du'u li xy. ctaipe lo'i kacna'u
|
(by mudri)
|
[edit]
|
|
|
|
Definition #67525
[edit]
| |
|
| 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 |
krtisfranks |
| vote information |
1
|
| time |
Sun Sep 6 19:04:20 2015 |
|
|
|
Examples
|
|
|
Definition #56829
[edit]
| |
|
| 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 |
krtisfranks |
| vote information |
0
|
| time |
Sat Jun 14 08:31:40 2014 |
|
|
|
Examples
|
|
|
|
|