By a similar chain of logic, x f^:(0:`<'@.')) y ↔ [email protected] (independent of f) .
This argument is perhaps more compelling in the context of an algebra of programs. It is analogous to proving y = (x^K) * y by setting K=0 rather than forcing x to be 1, which feels a little uncomfortable. But hey, either works; matter of taste. But the fact that I can engage in this kind of abstract reasoning about programs, and post terse proofs of them, should tell you why I'm attracted to J, and tacit J in particular. Especially since I'm in a cab on my way to the airport. BTW, it's possible to operationalize these identities with a simple tacit adverb: id =: (g`) (f^:) with either f a (right) identity function or g a constant-zero function, or both. So now our proof is executable. Go ahead and try it: its input is the atomic representation of any verb or operator which accepts and produces nouns, and it derives a verb of the proper valence (or ambivalence) which produces the same results. I've got more ideas, but I'm pulling up to the terminal now. -Dan Please excuse typos; composed on a handheld device. On Jan 25, 2013, at 4:05 PM, "Dan Bron" <[email protected]> wrote: > x ]^:(1:`<'@.')) y ↔ [email protected] ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
