op 05-06-14 18:46, Lars Hellström schreef: > Jan Willem Knopper skrev 2014-06-05 17.47: >> <!-- >> NOTATION: arith1.plus is<OMS cd='arith1' name='plus'/> >> >> This is a example description of an n-ary plus, defined based on a >> binary plus (for which I use homework2.plus2). >> >> homework1.function_with_arguments describes an n-ary function which >> can be defined by allowing access to the arguments in a single variable >> (by an OMBIND). > > OK, so that's essentially a sibling of fns1.lambda, which gives you the > list of the arguments as one object (that can then be decomposed), > instead of binding a separate variable to each argument. > > This will let you define many n-ary functions, so it's useful, but it > doesn't get very far with other forms of stating properties of them. > I.e., it lets you define a plus such that it will be n-associative, but > can you state as an FMP that it is n-associative? >
What do we want exactly, do we need a CD or maybe something more ? Also the question arises what will be the use case for this. For mathematicians it is often good enough to just vaguely say things. But some others want to formalize a lot. I saw this as an exercise for me to see what kind of things I would need to do such a definition (without creating a new symbol describing the associative expansion from binary to n-ary, what for some mathematicians might be enough of a definition). >> Several computer languages have a keyword or accessor to >> get to an array of arguments (Javascript, GAP). >> >> homework1.length returns the length of an argument sequence/list >> >> homework1.first returns the first argument of an argument >> sequence/list >> >> homework1.rest returns a new argument sequence/list containing all but >> the first argument. >> >> homework1.argument_sequence is implied (argument list) > > Duplicates stuff from list1 and list2. I wasn't aware of the experimental list2. It makes sense to use those functions here. > >> --> >> <-- >> real question >> >> is the idea that I describe an n-ary function with a new cd good >> enough for all applications ? > > I believe you can handle at least 98% of all such situations with just a > few new symbols, i.e., no change needed to the standard. The area where > this would get into trouble is saying things about binders that bind a > variable number of variables, since binding a variable is syntactically > special. > that was the idea I had. I did this exercise mostly, so that others can give me insight about the last 2% :) >> regardless of whether we need it for this definition it might be good >> to have some new kind of apply function that calls a function with the >> arguments in a list (list1.list ?). > > Yes. That is essentially my take on the subject. I intend to submit such > a CD for OM2014, so I'd like to polish it for a few days more. > >> will it be good enough to do this in a cd as well, >> >> homework1.apply_with_arguments: >> >> >> @(homework1.apply_with_arguments,arith1.plus,@(homework1.argument_sequence,1,2,3)) >> > > My preferred style is rather > > @(list4.eval,@(list1.list,arith1.plus,1,2,3)) For me arith1.plus is more an argument to list4.eval than to the list1.list, so I prefer having it out of the list. But this is open to discussion. > > >> is it possible to do correct types for this, or will this run into >> problems ? > > I don't really care. Types are overrated, and often thrown around in a > frighteningly naive manner. :-) > I don't use the typing system much, but I would prefer not to break it :) Jan Willem _______________________________________________ Om3 mailing list [email protected] http://openmath.org/mailman/listinfo/om3
