BNF for ('a => 'b) => 'c with live 'a, 'c - possible? · Beginner Questions

Hello,
long story short, I have a type that is a map from maps (representing vectors in some space) to values, plus two additional sets bounding the domain vectors' dimensionality, and some theorems. Thus it boils down to 'a set + 'a set + ('a => 'b) => 'c. I would like to define a recursive type based on it through the 'a position, so that dimension labels can also refer to these "partial scalar fields".

The default BNF for ('a => 'b) => 'c marks 'a, 'b as dead and 'c as alive. I am wondering if there's a way to define 'a to be alive too. I'm not very good with category theory, so I defined the obvious map, but I am struggling with setfns/predicators/relators - what is a natural transformation for this functor in 'a place? By the equation it seems it should be something like "set of all the arguments that the outer function will pass to the inner function", but I'm not sure how to formalize this.

Alex Mobius (Feb 23 2026 at 23:15):

Update: I am trying to move forward with just the map for right now, here's my repro:

definition map_fn2 :: "('a ⇒ 'd) ⇒ ('c ⇒ 'e) ⇒ (('a ⇒ 'b) ⇒ 'c) ⇒ (('d ⇒ 'b) ⇒ 'e)"
  where "map_fn2 map_arg map_val f0 farg = map_val (f0 (farg ∘ map_arg))"

bnf fn2: "('a ⇒ 'b) ⇒ 'c"
  map: map_fn2
  sets: "λ_.{}" range
  bd: "card_suc ( card_of (UNIV::'a set) )" (*placeholder*)
(* exception UnequalLengths raised (line 553 of "library.ML") *)

Now the cardinal type is probably wrong, but something is going wronger... What does that exception mean? Do I need to communicate some additional things to the BNF procedure?

Dmitriy Traytel (Feb 24 2026 at 06:29):

The error message is unfortunately a low level crash, but the bound may not depend on live BNF parameters.

Also if you pick set to be "%_. {}", you basically require the map function via the congruence property to ignore the corresponding position 'a.

Generally, I doubt that this will work for the general ('a => 'b) => 'c. There may be some restricted variant (e.g., such functions + an explicit finite/countable/'k-bounded domain for 'a). You have these additional sets. Are they bounded in some way?

Alex Mobius (Feb 24 2026 at 11:03):

Yes, I've realized that there's no way to satisfy both congruence and natural transformation laws while providing the obvious mapping.
Thankfully the actual datatype I need is ('a, 'b) fmap .> 'c * 'a fset, where the domains of domain are bounded by this additional set. (There's more stuff but not important). Looks like the first set is then just this additional set - it's obviously an upper bound on congruence, and obviously a natural transformation. I do need to fogure out how to express the cardinality bound though, looks to be something like "the set of (finite) subsets of 'b", is that what c_sup does?

Alex Mobius (Feb 24 2026 at 14:40):

Alex Mobius (Feb 25 2026 at 07:55):

Ah, it seems that I am not quite there - the dimension map does not commute with range... which is just as it is - for example, mapping two dimensions to the same value corresponds then to taking a diagonal, which loses values :( Everything else commutes just fine - the dimension map and the value map, the value map and the dimension set, composition and identity rules hold, obviously).

I suppose my only option is to make two separate BNFs. Would I be able to choose which one to use in the type definitions downstream, in some way?

Dmitriy Traytel (Feb 25 2026 at 09:50):

Each type can be only associated with one BNF structure. But maybe I'm misunderstanding what you are trying to achieve. Can you post your datatype that you are trying to construct?

Alex Mobius (Feb 25 2026 at 15:28):

The original file is long, contains additional restrictions and claims, so I've made an abridged version that omits the proofs of the true facts
ValsetAbridged.thy
the claim "vrange_idem" at the bottom is untrue, but it is the lemma we would need to be true if we were to prove that "bnf_map" is a natural transformation in its second argument. The rest of the laws are satisfied.

Alex Mobius (Feb 25 2026 at 15:29):

I suppose I only really need to recurse in the first type argument, so I could just limit myself to that :) it is somewhat unsatisfying, but such is it.

Dmitriy Traytel (Feb 25 2026 at 16:08):

Limiting yourself to a BNF in 'a is plausible if that is what your application requires. I had a quick look at the theory and wondered if vrange is the right notion. I.e., should you restrict your attention to only these 'c elements that are in the range of some mapping M whose domain is contained in the explicit max_dims bound? (Not sure if this helps with the naturality in 'c though.)

Alex Mobius (Feb 25 2026 at 16:32):

I'm pretty sure vrange is the only definition that satisfies congruence and naturality for map_val. Congruence says the set has to be at least as large as vrange, and naturality says it has to be at least as small. In a philosophical sense, those are indeed the values of 'c that the mapping contains!

Alex Mobius (Feb 25 2026 at 16:53):

e.g. have vrange vsU = UNIV, then for any set2 for which set2 (map_val f vsU) = f `` set2 vsU, we have set2 (map_val f vsU) = vrange (map_val f vsU), now observe that for any vs, typedef t = {vrange vs} implies vs = map_val Rep_t (map_val Abs_t vs) and vrange (map_val Abs_t vs) = UNIV.

Alex Mobius (Mar 02 2026 at 22:28):

Unfortunately, after a couple of days of struggling with relator and trying to define alternative notions of map (even dropping into (('a, 'b) fmap \<times> 'c) set, I'm starting to suspect it might not be possible. Would anyone have pointers as to how I ma convince myself of that? :) I'm unfortunately only passingly familiar with CT

Stream: Beginner Questions

Topic: BNF for ('a => 'b) => 'c with live 'a, 'c - possible?

Alex Mobius (Feb 23 2026 at 21:02):