[Om3] homework, describing a definition for n-ary plus

[Jan Willem Knopper]

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