The set of all compositions of given multivariate functions

Stream: new members

[Justus Willbad]

Could you please help me formulating the set below?

I couldn't install LeanCopilot under Windows WSL, and GitHub Copilot's solutions always resulted in some syntax/type errors, even if I replaced the Lean 3 commands with the Lean 4 commands.

Let
$n\in\mathbb{N}_+$,
$a_1,...,a_n\in\mathbb{N}_0$,
$X$ a set,
$\forall i\in\{1,...,n\}\colon f_i\colon X^{a_i}\to X$,
$F_0=\{f_1,...f_n\}$,
$F$ the set of all compositions of elements of $F_0$.

[Ilmārs Cīrulis]

Have you tried writing the code on https://live.lean-lang.org/ ?

[Justus Willbad]

How could that help? I used VSCode without LeanCopilot.

[Ilmārs Cīrulis]

Sorry, I can't read. :sweat:

[Ilmārs Cīrulis]

I will try to formulate your definition.

[Ilmārs Cīrulis]

What's that $X^{a_i}$?

[Edward van de Meent]

i'd say something like Fin a_i -> X

[Ilmārs Cīrulis]

"given multivariate functions" - i believe that's like Cartesian product of $a_i$ copies of $X$.

[Ilmārs Cīrulis]

It's the same, sorry.

[Ilmārs Cīrulis]

import Mathlib

def problem (n: ℕ) (Hn: 0 < n) (a: Fin n → ℕ) {A} (X: A → Prop) (F0: ∀ (i: Fin n), Fin (a i) → X): sorry := sorry

Got stuck at "set of all compositions of elements of F0". Brains too low powered today, it seems. :(

[Edward van de Meent]

yea, that's not a trivial thing at all

[Justus Willbad]

$X^{a_i}$ is the $a_i$-th cross product of $X$. If we assume $X=\mathbb{C}$ for example, we have $X^{a_i}=\mathbb{C}^{a_i}$.

GitHub Copilot made good suggestions, but something was wrong with it.

[Eric Wieser]

What exactly do you mean by your definition of $F_0$? Is the set $\{x\ y \mapsto x + y, x\ y \mapsto x - y\}$ allowed? Or is there at most one function of each arity? nevermind

[Edward van de Meent]

even writing out "a direct composition of fixed-arity functions" is nontrivial... and using it would be difficult and/or awful, due to the dependency of its type on the precise arity of the inputs...

[Eric Wieser]

Here's a prototype:

import Mathlib

variable {α : Type*}

def Fin.mvComp (F₁ : (Fin m₁ → α) → α) (i : Fin m₁) (F₂ : (Fin m₂ → α) → α) : (Fin (m₁ + m₂ - 1) → α) → α :=
  fun args =>
    let outerArgs : Fin (m₁ - 1) → α := sorry
    let innerArgs : Fin m₂ → α := sorry
    F₁ (Fin.insertNth i (F₂ innerArgs) outerArgs ∘ Fin.cast sorry)

inductive IsMvCompositionOf {ι} {n : ι → Nat} (F0 : ∀ i, (Fin (n i) → α) → α) : {m : ℕ} → ((Fin m → α) → α) → Prop where
  | f0 (i) : IsMvCompositionOf F0 (F0 i)
  | comp {m₁ m₂} {F₁ : (Fin m₁ → α) → α} (i : Fin m₁) {F₂ : (Fin m₂ → α) → α} :
    IsMvCompositionOf F0 F₁ → IsMvCompositionOf F0 F →  IsMvCompositionOf F0 (Fin.mvComp F₁ i F₂)

[Edward van de Meent]

i feel like there should be better ways to go about this than this inductive prop...

[Edward van de Meent]

using something like this:

def Set.closure {α : Type*} (s : Set α) (f : α → Set α) : Set α :=
  ⋂ (s'∈ {s':Set α | ∀ a ∈ s', s ∪ f a ⊆ s'}), s'

[Edward van de Meent]

i guess that doesn't quite work in this case since the function we're using is 2-ary w/r/t α

[Eric Wieser]

I would guess that there is a ModelTheory way to write this

[Edward van de Meent]

how so?

[Eric Wieser]

docs#FirstOrder.Language.Term is the type of expressions built from variables and compositions of functions

[Eric Wieser]

Though I guess this allows argument permutation and repetition, which doesn't seem permitted in the context of this thread

[Kyle Miller]

Without model theory:

1. Define a type for multivariate functions. You need a sigma type to record the arity, and it would let you talk about sets of them.
2. Define the composition operation. (Eric's nearly done that.)
3. Define a predicate that means "this set is closed under composition"
4. Take the infimum over all sets that satisfy the predicate and which contain the subset $\{f_1,...,f_n\}$

This is how generating a set closed under an operation works normally in the literature, and it's possible to do it in Lean too.

[Kyle Miller]

This might be a good excuse to formalize operads. This happens to be one of the basic examples of an operad, and the object in question would be the suboperad generated by $\{f_1,\dots,f_n\}$ I think. (Edit: actually, this would be operad algebras and operad subalgebras.)

[Edward van de Meent]

once you have your composition operator, i think it should be easy to use what i suggested above to finish the construction...

[Edward van de Meent]

because then you can simply use fun F1 F2 => (Fin.mvComp F1 . F2) '' Set.univ as f

[Edward van de Meent]

using the following closure construction

def Set.closure₂ {α : Type*} (s : Set α) (f : α → α → Set α) : Set α :=
  ⋂ (s' ∈ {s' : Set α | s ⊆ s' ∧ (∀ a ∈ s', ∀ b ∈ s', f a b ⊆ s')}), s'

lemma Set.closure₂_subset {α : Type*} {s : Set α} {f : α → α → Set α} {s' : Set α}
  (base : s ⊆ s') (step : ∀ a ∈ s',∀ b ∈ s', f a b ⊆ s') : s.closure₂ f ⊆ s' := by
  dsimp [closure₂]
  refine iInter₂_subset s' ?_
  use base

lemma Set.closure₂_induction {α : Type*} {s : Set α} {f : α → α → Set α} {motive : α → Prop}
  (mem : ∀ a ∈ s, motive a) (step : ∀ a b, motive a → motive b → ∀ c ∈ (f a b),motive c) : ∀ a ∈ s.closure₂ f, motive a := s.closure₂_subset f motive mem (by intro a b ha hb; exact step a ha b hb)

[Justus Willbad]

Addition: In fact, I want $\forall i\in\{1,...,n\}\colon f_i\colon X^{a_i}\supseteq D_i\to Y_i\subseteq X$.

[Edward van de Meent]

what even???

[Ilmārs Cīrulis]

$Y_i$ one can ignore, I believe. :thinking:

About $D_i$ - if there different domains (?) the compositions falls appart, imho.

[Ilmārs Cīrulis]

Partial functions are evil, anyway

[Edward van de Meent]

can we just work with X -> Option X or something?

[Justus Willbad]

GitHub Copilot gives:

import Mathlib
-- Define n as a natural number greater than zero
variable (n : ℕ)
variable (n_pos : 0 < n)
-- Define a_i as a sequence of natural numbers
variable (a : Fin n → ℕ)
-- Define X as a set
variable (X : Type)
-- Define Y_i as a codomain
variable (Y : Fin n → Type)
-- Define D_i as the domain subset of X^{a_i}
variable (D : Fin n → set (X ^ (a i)))
-- Define f_i as functions from X^{a_i} to Y_i
variable (f : Π i, D i → Y i)
-- Define F_0 as the set of functions {f_1, ..., f_n}
def F_0 : set (Π (i : Fin n), D i → Y i) := {f}
-- Define F as the set of all compositions of elements in F_0
def compositions {α : Type} (s : set (α → α)) : set (α → α) :=
  {g | ∃ l : list (α → α), (∀ f ∈ l, f ∈ s) ∧ l.prod = g}
def F : set (X → X) := compositions F_0

But Lean prints the error below for
variable (D : Fin n → set (X ^ (a i))) :

application type mismatch
a i
argument
i
has type
?m.1294 : Sort ?u.1293
but is expected to have type
Fin n : Type

[Justus Willbad]

There are only total functions, no partial functions.

When composing mutivariate/multiary functions, we can think of the composition of relations.

[Ilmārs Cīrulis]

I would suggest variable (D : ∀ (i: Fin n), Set (Fin (a i) → X))

[Justus Willbad]

I exchanged this, but now Lean prints:

type expected, got
(set ((i : Fin n) → ↑(D i) → Y i) : ?m.441 PUnit.{2})
All Messages (3)
Funktionskomposition.lean:26:10
type expected, got
(set ((i : Fin n) → ↑(D i) → Y i) : ?m.441 PUnit.{2})
Funktionskomposition.lean:29:33
type expected, got
(set (α → α) : ?m.754 PUnit.{2})```
Funktionskomposition.lean:32:8
type expected, got
(set (X → X) : ?m.1042 PUnit.{2})

[Matt Diamond]

it looks like you wrote set in lowercase instead of Set

[Matt Diamond]

you may want to add set_option autoImplicit false at the top of the file, as the auto-implicit feature can sometimes make these errors more confusing by introducing unintended variables

[Justus Willbad]

Now Lean prints

failed to synthesize
Mul (α → α)
Additional diagnostic information may be available using the set_option diagnostics true command.

for

def compositions {α : Type} (s : Set (α → α)) : Set (α → α) :=
  {g | ∃ l : List (α → α), (∀ f ∈ l, f ∈ s) ∧ l.prod = g}

def F : Set (X → X) := compositions F_0

[Edward van de Meent]

That's because composition of functions is not written with * in lean

[Eric Wieser]

docs#Function.End makes it so that it _is_ written with * :)

[Justus Willbad]

How can the code def compositions above be written correctly?

[Justus Willbad]

What is wrong with the following code?

variable (X : Type*) (n : ℕ) (f : Fin n → X → X)
-- Define F₀ as the set of these functions
def F₀ : Set (X → X) := {f i | i : Fin n}
-- Define F as the set of all compositions of finite numbers of elements of F₀
def F₁ : Set (X → X) := {g | ∃ m : ℕ, ∃ (h : Fin m → X → X), (∀ i, h i ∈ F₀) ∧ g = (List.ofFn h).foldr (· ∘ ·) id}

Lean prints:

failed to synthesize
Membership (X → X) ((X : Type ?u.607) → (Fin n → X → X) → Set (X → X))

for the last row.

[Eric Wieser]

Fin n → X → X is not a multivariate function

[Eric Wieser]

It's a family of n univariate functions

[Eric Wieser]

Maybe you intended that though, and this is a simplified version

[Eric Wieser]

You need to change F₀ to F₀ X f above

[Edward van de Meent]

(Fin n -> X) -> X is tho

[Justus Willbad]

Yes, I tried univariate functions now.

Could you please write the whole code? Otherwise I don't know what exactly I should replace.