I'm not sure this counts as a proof, exactly, but here's a derivation of the quadratic formula in J.
https://github.com/tangentstorm/tangentlabs/blob/master/j/quadratic.ijs#L132 I also use this quite a bit on irc: https://github.com/tangentstorm/tangentlabs/blob/master/j/logic.ijs Most of that file is just assertions of the basic laws of propositional logic. The two most important lines are the definition of 'given' and some variables to represent every possible combination of 5 boolean values. 'p q r s t' =: |: #: ,. i. 2 ^ 5 given =: ,@([: _:^:(2=#)@ ~."1 [ #"1~ *./@]) These two lines, combined with J's logical connectives are all you need to experiment with many different problems in propositional logic and modal logic. p,q 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 p <: q NB. 'p implies q'. (Can also be written 'p ! q') 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 p +. q NB. 'p or q' 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 p *. q NB. 'p and q' 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 p *. -.q NB. 'p and not-q' 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 (-.p) *. q NB. 'not-p and q' 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -. p *. q NB. 'not (p and q)' 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 p *: q NB. 'p nand q' 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 p +. -.p NB. some things are always true 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 p *. -.p NB. some things are never true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 (p *. -.p) given '' NB. 'given' can summarize the results 0 p given '' NB. If it can't deduce an answer, it shows '_'. _ (p,q) given '' NB. You can query multiple variables. _ _ (p,q) given p NB. Given p, it knows p=1, but q is still unknown. 1 _ (p,q) given p,q NB. Commas on the right are treated as 'AND'. 1 1 (p,q) given p, p <: q NB. Given p=1 and p implies q, it can deduce q for you. 1 1 NB. But, it needn't be so simple: (p,q,r,s,t) given ((-.s) <: q), (q <: (r *. t)), (-.t), (p=r), q~:p 1 0 1 1 0 You can use these canned variables and the 'given' verb to solve many logic problems quite easily. For example, you can solve these "knights and knaves" puzzles, for example, simply by figuring out how to restate the facts in J: http://philosophy.hku.hk/think/logic/knight.php On Sun, Mar 2, 2014 at 12:16 AM, km <[email protected]> wrote: > Here's how I express the identity ([: f g) -: f@:g (admittedly the > following is not much use to a newcomer) > > comp =: 2 : ' ([: u v) -: u @: v ' > > *: comp % 1 2 3 > 1 > 1 2 3 *: comp % 4 5 6 > 1 > > --Kip > > Sent from my iPad > > > On Mar 1, 2014, at 11:16 PM, Roger Hui <[email protected]> > wrote: > > > > It's like asking where are the oxygen molecules in the air you breathe. > > > > f=: +/@i. = 2&! > > f"0 i.20 > > 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 > > > > See also *A Letter from Dijkstra on APL > > <http://archive.vector.org.uk/art10501260> .* > > > > > > > > > > > > > >> On Sat, Mar 1, 2014 at 7: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 > ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
