Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: A parametrized “application” function

view this post on Zulip Julius Hamilton (Nov 16 2024 at 19:45):

Here are some functions:

apply1:UnaryFunctionSymbol×Term→Term\text{apply}_1 : \text{UnaryFunctionSymbol} \times \text{Term} \to \text{Term}

apply2:BinaryFunctionSymbol×Term2→Term\text{apply}_2 : \text{BinaryFunctionSymbol} \times \text{Term}^2 \to \text{Term}

apply3:TernaryFunctionSymbol×Term3→Term\text{apply}_3 : \text{TernaryFunctionSymbol} \times \text{Term}^3 \to \text{Term}

And so on.

It appears this can be generalized to any natural number:

applyn:n-aryFunctionSymbol×Termn→Term\text{apply}_n : \text{n-aryFunctionSymbol} \times \text{Term}^n \to \text{Term}

Perhaps we can make this more formal by adding an equational constraint, for the function symbols. There could be a function select:N→FunctionSymbol\text{select} : \mathbb{N} \to \text{FunctionSymbol} and select(n)={x∈FunctionSymbol∣arity(x)=n}\text{select}(n) = \{ x \in \text{FunctionSymbol} | \text{arity}(x) = n\}. (arity:FunctionSymbol→N\text{arity} : \text{FunctionSymbol} \to \mathbb{N}).

I suppose we could also say that if we have an arity function, select(n)\text{select}(n) is the pre-image of arity\text{arity} at value nn.

Now it seems like the application function is “fully parametrized”, as applyn:select(n)×Termn→Term\text{apply}_n : \text{select}(n) \times \text{Term}^n \to \text{Term}. So I think it can be abstracted into Apply:N→{apply}\text{Apply} : \mathbb{N} \to \{ \text{apply} \}.

I imagine this is a very common, standard function, and I’m wondering what a standard, elegant way to define it is, in contrast to my own attempt.

view this post on Zulip Ryan Wisnesky (Nov 17 2024 at 03:32):

in languages with products, often all function applications are unary, and if you need n-ary arguments, you tuple them up. or, in e.g. Coq you could define a family of functions of varying arity by induction on the number of arguments.

view this post on Zulip Morgan Rogers (he/him) (Nov 23 2024 at 11:54):

The motif is that of algebra for an operad, in case that gives you some direction.