Talk:Vocabulary/Unreadability
The page claims that 'For a right triangle, the square on the hypotenuse is equal to the sum of the squares on the other two sides' means the same as isRight=: ([: *: {:) = ([: +/ [: *: }:).
I disagree.
I think the former is a theorem which postulates a causal relationship (if a triangle is right, then the square of its hypotenuse...)
While the J snippet is a definition (to say 'a triangle is right' is to say 'the square of a triangle's hypotenuse...')
I am not sure how to better write the section, though.
You are right, Elijah, it is not "the same theorem expressed in J".
I am guilty of what WikiPedia:Nicolas_Bourbaki calls abus de notation (before using it anyway, for better understanding by the student). But it would badly complicate the treatment to detail the formal relationship between Pythagoras's Theorem [PT] and the J code [JC] I offer.
Mine is an informal treatment directed at the layperson (or at least the jobbing programmer). It would suffer from being too precise, when I am keen to address him in terms he/she would be familiar with.
But you raise interesting questions, which Ken and Roger deal with elsewhere (if memory serves): how to handle theorem proving in J. Had I the time, I'd love to expound my own ideas on the topic. I'd address myself to the discerning student, not to my peers – I no longer have an academic career or a professional reputation to defend. And I'm thirty years out of date with the terminology. (Or should that be: terminologies?)
But I fear I don't go with yours. I struggle to map your term causal relationship into any relevant category here, whether it's Logic, Geometry, Algebra or J. I'm aware of its use in Physics, but even physicists seem hazy about what they refer to as causality. Especially cosmologists, who have the biggest need for a sound definition.
And what exactly do you mean by definition? Clearly you can't mean it in the limited J sense, i.e. the functionality surrounding the primitive Define(:). In this article it would beg the question.
It's hard to pick on a terminology which geometers, algebraists (my PhD is in Finite Group Theory), logicians, historians of science and IT professionals can all understand, let alone agree on. Let's go with logicians' talk (at least, what an expert in switching logic might recognise)…
- The informal English statement of PT is a proposition. Other statements are possible, in ever-stricter formalisms. These formalisms can get very strict indeed: see the proof of the proposition 1+1=2 in Russell & Whitehead's Principia Mathematica.
- This particular proposition (PT) has been proven (using ruler and compass) by Euclid. So I'm justified in calling it a theorem.
- A proposition may be codified in terms of formulas. Codifications are never unique, and can be numerous. My formulas are equations, which bear comparison with J logical phrases using Equal(=). (Notice how I'm straining to avoid using the word "same" as in: "the same theorem expressed in J".)
- A codifications in Euclidean geometry is called a construction. Example: constructing a square on one of the sides of a triangle as a step in the proof of some proposition.
- A codifications in Algebra is called an expression, of which an equation is the most use here.
- JC codes a test. Typically a test implements a formula, for application to a given example (needing to be provided here as an ascending list of 3 lengths). I've chosen (following Turing) to compute a J Boolean value: 0|1. A sounder way is to use the stdlib verb: assert.
- A test is said to be based on a proposition.
Now based on is a creative activity, not a formal one, and it is seldom formally justified by the creators. AFAICT a typical published description of an algorithm just presents it in such a way as to look "obvious" to people in-the-know. The methodology is not standardised, and most algebraists and engineers cobble up their own. Indeed Iverson Notation (which gave rise to APL and J) was developed to address that very problem: i.e. validating algorithms to be implemented in switching logic. The first practical application of APL was validating the IBM 360 instruction set.
I say validating, not proving. The latter would be too strong a term here. I don't believe APL is strong enough for theorem proving because it lacks a formal metalanguage, such as provided for Algebra by Predicate Logic.
So for the present I'm going to let the wording stand, and let people guess what I mean by "the same theorem".