To "close" a little, let's say a J identity has the form f -: g and always returns 1. An example is
*:@+ -: *:@[ + (2 * *) + *:@] which is J's form of algebra's (a+b)^2 = a^2 + 2ab + b^2 . But I would be especially interested in identities like ([: f g) -: f @: g which describe how J works. --Kip Sent from my iPad > On Mar 1, 2014, at 10:13 PM, Raul Miller <[email protected]> wrote: > > That's... something of an open ended question. > > Consider, for example: www.jsoftware.com/jwiki/Essays/Euler's_Identity > > Or, for that matter: > +/*:1 2 o.o.^:8 ?0 > 1 > > -- > Raul > > >> On Sat, Mar 1, 2014 at 10:55 PM, km <[email protected]> wrote: >> >> One "identity" in J is that ([: f g) -: f@:g (always returns 1). What >> are some others? >> >> --Kip Murray >> >> Sent from my iPad >> >>> On Mar 1, 2014, at 8:41 PM, Raul Miller <[email protected]> wrote: >>> >>> Two languages which go even more heavily into "proof" territory are (if I >>> recall correctly) Agda, and Coq. >>> >>> They also have some interesting aspects that I would like to see in a "J >>> subset compiler". >>> >>> Thanks, >>> >>> -- >>> Raul >>> >>> >>> On Sat, Mar 1, 2014 at 8:30 PM, David Lambert <[email protected] >>> wrote: >>> >>>> Mentioning "proof" in j conversation rolls easily off the pen. Not so >>>> with other computer languages I've used. >>>> >>>> (,&#~.) HASHES NB. prove the hashes are unique. (tallies agree) >>>> 6 6 >>>> >>>> http://forums.devshed.com/showpost.php?p=2927271&postcount=4 >>>> ---------------------------------------------------------------------- >>>> For information about J forums see http://www.jsoftware.com/forums.htm >>> ---------------------------------------------------------------------- >>> For information about J forums see http://www.jsoftware.com/forums.htm >> ---------------------------------------------------------------------- >> For information about J forums see http://www.jsoftware.com/forums.htm > ---------------------------------------------------------------------- > For information about J forums see http://www.jsoftware.com/forums.htm ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
