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?
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.
-->
<--
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.
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))
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. :-)
Lars Hellström
_______________________________________________
Om3 mailing list
[email protected]
http://openmath.org/mailman/listinfo/om3
