[Jprogramming] applying >1 gerunds to a set of items

[Dan Bron]

By a similar chain of logic, x f^:(0:`<'@.')) y ↔ x at .y (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" <j at bron.us> wrote:

> x ]^:(1:`<'@.')) y ↔ x at .y