Received: from 173-13-139-235-sfba.hfc.comcastbusiness.net ([173.13.139.235]:60968 helo=jukni.digitalkingdom.org) by stodi.digitalkingdom.org with smtp (Exim 4.85) (envelope-from ) id 1ZYfCQ-0008KR-Hp; Sun, 06 Sep 2015 12:02:04 -0700 Received: by jukni.digitalkingdom.org (sSMTP sendmail emulation); Sun, 06 Sep 2015 12:01:58 -0700 From: "Apache" Date: Sun, 06 Sep 2015 12:01:58 -0700 To: webmaster@lojban.org, curtis289@att.net, jammyatjammy@gmail.com Subject: [jvsw] Definition Edited At Word ctaipe -- By mudri Bcc: jbovlaste-admin@lojban.org Message-ID: <55ec8da6.Lm8tLJoTjAAQ8am2%webmaster@lojban.org> User-Agent: Heirloom mailx 12.5 7/5/10 MIME-Version: 1.0 Content-Type: application/octet-stream Content-Transfer-Encoding: 8bit X-Spam-Score: 3.2 (+++) X-Spam_score: 3.2 X-Spam_score_int: 32 X-Spam_bar: +++ X-Spam-Report: Spam detection software, running on the system "stodi.digitalkingdom.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see @@CONTACT_ADDRESS@@ for details. Content preview: [...] Content analysis details: (3.2 points, 5.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 1.4 RCVD_IN_BRBL_LASTEXT RBL: No description available. [173.13.139.235 listed in bb.barracudacentral.org] 0.8 BAYES_50 BODY: Bayes spam probability is 40 to 60% [score: 0.4956] 1.0 RDNS_DYNAMIC Delivered to internal network by host with dynamic-looking rDNS In jbovlaste, the user mudri has edited a definition of "ctaipe" in the language "English". Differences: 5,5c5,5 < Types and propositions are considered equivalent due to the Curry-Howard correspondence. Compare to mathematical notation: “$x_3 \vdash x_1 : x_2$”, with $x_4$ implied by context. In proof-irrelevant work (e.g, classical logic), this is usually written “$x_3$ ⊢ $x_2$”. $x_1$ 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. $x_1$ can be filled by {zi'o}, which means that the proposition is unprovable. $x_2$ can be filled by a set of which the $x_1$ value is a member. It may be convenient to interpret {lo'i} as the gadri for types. $x_3$ will be a conjunction of {du'u} sumti, each possibly containing a bridi based on {ctaipe}. $x_4$ need not be consistent. For example, almost every programming language has an inconsistent type system (by virtue of being Turing-equivalent). --- > Types and propositions are considered equivalent due to the Curry-Howard correspondence. Compare to mathematical notation: "$x_3 \vdash x_1 : x_2$", with $x_4$ implied by context. In proof-irrelevant work (e.g, classical logic), this is usually written "$x_3 \vdash x_2$". $x_1$ 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. $x_1$ can be filled by {zi'o}, which means that the proposition is unprovable. $x_2$ can be filled by a set of which the $x_1$ value is a member. It may be convenient to interpret {lo'i} as the gadri for types. $x_3$ will be a conjunction of {du'u} sumti, each possibly containing a bridi based on {ctaipe}. $x_4$ need not be consistent. For example, almost every programming language has an inconsistent type system (by virtue of being Turing-equivalent). 11,11d10 < Word: typed, In Sense: type theory, programming \n12a12,12 \n> Word: typed, In Sense: type theory, programming Old Data: Definition: $x_1$ is a value / proof of type / proposition $x_2$ under context $x_3$ in (type / logical) system $x_4$. Notes: Types and propositions are considered equivalent due to the Curry-Howard correspondence. Compare to mathematical notation: “$x_3 \vdash x_1 : x_2$”, with $x_4$ implied by context. In proof-irrelevant work (e.g, classical logic), this is usually written “$x_3$ ⊢ $x_2$”. $x_1$ 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. $x_1$ can be filled by {zi'o}, which means that the proposition is unprovable. $x_2$ can be filled by a set of which the $x_1$ value is a member. It may be convenient to interpret {lo'i} as the gadri for types. $x_3$ will be a conjunction of {du'u} sumti, each possibly containing a bridi based on {ctaipe}. $x_4$ need not be consistent. For example, almost every programming language has an inconsistent type system (by virtue of being Turing-equivalent). Jargon: type theory (computer science) & proof theory (mathematics/philosophy) Gloss Keywords: Word: typed, In Sense: type theory, programming Word: proof, In Sense: proof theory, general mathematics Place Keywords: Word: value/proof, In Sense: , For Place: 1 Word: type/proposition, In Sense: , For Place: 2 Word: context, In Sense: type theory/proof theory, For Place: 3 Word: type system/logic, In Sense: , For Place: 4 New Data: Definition: $x_1$ is a value / proof of type / proposition $x_2$ under context $x_3$ in (type / logical) system $x_4$. Notes: Types and propositions are considered equivalent due to the Curry-Howard correspondence. Compare to mathematical notation: "$x_3 \vdash x_1 : x_2$", with $x_4$ implied by context. In proof-irrelevant work (e.g, classical logic), this is usually written "$x_3 \vdash x_2$". $x_1$ 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. $x_1$ can be filled by {zi'o}, which means that the proposition is unprovable. $x_2$ can be filled by a set of which the $x_1$ value is a member. It may be convenient to interpret {lo'i} as the gadri for types. $x_3$ will be a conjunction of {du'u} sumti, each possibly containing a bridi based on {ctaipe}. $x_4$ need not be consistent. For example, almost every programming language has an inconsistent type system (by virtue of being Turing-equivalent). Jargon: type theory (computer science) & proof theory (mathematics/philosophy) Gloss Keywords: Word: proof, In Sense: proof theory, general mathematics Word: typed, In Sense: type theory, programming Place Keywords: Word: value/proof, In Sense: , For Place: 1 Word: type/proposition, In Sense: , For Place: 2 Word: context, In Sense: type theory/proof theory, For Place: 3 Word: type system/logic, In Sense: , For Place: 4 You can go to to see it.