Finite-algebra operations allocate through BinaryOperation{N} fields

# Finite-algebra operations allocate through `BinaryOperation{N}` fields

I measured 64 allocated bytes for every finite-algebra operation when I reached the operation through its algebra field. I measured zero allocated bytes when I put the same table in concretely typed fields.

## Version and source

I cloned the repository read-only and ran the reproduction against commit `97a55e44f35a840cd992345107391308aa13fb9f` (merged as `Merge pull request #107 from aclai-lab/fix/106`). My checkout reported SoleLogics version `0.13.7`. I used Julia `1.12.7`, StaticArrays `1.9.19`, and SoleBase `0.13.4`.

I found these declarations in `src/many-valued-logics/finite-algebras.jl` at this commit:

- line 174 declares `CommutativeMonoid.operation::BinaryOperation{N}`;
- lines 728–731 declare the `FiniteFLewAlgebra` operation fields (`join`, `meet`, `monoid`, and `implication`), with `monoid.operation` using the declaration at line 174.

I noted that `BinaryOperation` has parameters `{N,M}`, so `BinaryOperation{N}` leaves `M` unspecified. I confirmed that Julia reports the resulting field type as a non-concrete `UnionAll`.

## Reproduction

I saved the following as `repro.jl` and ran it from the SoleLogics checkout with `julia --startup-file=no --project=. repro.jl`:

```julia
using SoleLogics
using SoleLogics.ManyValuedLogics
using InteractiveUtils

const G3 = SoleLogics.ManyValuedLogics.G3
const X = FiniteTruth(2)
const Y = FiniteTruth(2)

function native_loop(a::FiniteFLewAlgebra{3}, n::Int)
result = X
for _ in 1:n
result = a.monoid.operation(X, Y)
end
return result
end

struct ConcreteCommutativeMonoid{N,O<:BinaryOperation{N}}
operation::O
identityelement::FiniteTruth
end
struct ConcreteFLew{N,O<:BinaryOperation{N},M<:ConcreteCommutativeMonoid{N,O}}
join::O
meet::O
monoid::M
implication::O
bot::FiniteTruth
top::FiniteTruth
end
const O = typeof(G3.join)
const CM = ConcreteCommutativeMonoid{3,O}(G3.monoid.operation, G3.monoid.identityelement)
const CA = ConcreteFLew{3,O,typeof(CM)}(G3.join, G3.meet, CM, G3.implication, G3.bot, G3.top)
function concrete_loop(a::ConcreteFLew{3}, n::Int)
result = X
for _ in 1:n
result = a.monoid.operation(X, Y)
end
return result
end

native_loop(G3, 1)
concrete_loop(CA, 1)

println("Julia ", VERSION)
println("SoleLogics ", pkgversion(SoleLogics))
println("runtime operation type: ", typeof(G3.monoid.operation))
println("upstream field type: ", fieldtype(typeof(G3.monoid), :operation))
println("upstream field is concrete: ", isconcretetype(fieldtype(typeof(G3.monoid), :operation)))
println("counterfactual field type: ", fieldtype(typeof(CM), :operation))
println("counterfactual field is concrete: ", isconcretetype(fieldtype(typeof(CM), :operation)))
println("results: ", native_loop(G3, 1_000), " / ", concrete_loop(CA, 1_000))
println("native bytes for one call: ", @allocated native_loop(G3, 1))
println("counterfactual bytes for one call: ", @allocated concrete_loop(CA, 1))
println("native bytes for 1,000 calls: ", @allocated native_loop(G3, 1_000))
println("counterfactual bytes for 1,000 calls: ", @allocated concrete_loop(CA, 1_000))
println("native code_warntype:")
@code_warntype native_loop(G3, 1)
println("counterfactual code_warntype:")
@code_warntype concrete_loop(CA, 1)
```

I obtained this relevant output from my fresh run:

```
Julia 1.12.7
SoleLogics 0.13.7
runtime operation type: BinaryOperation{3, StaticArraysCore.SMatrix{3, 3, FiniteTruth, 9}}
upstream field type: BinaryOperation{3, M} where M<:(StaticArraysCore.SMatrix{3, 3, FiniteTruth})
upstream field is concrete: false
counterfactual field type: BinaryOperation{3, StaticArraysCore.SMatrix{3, 3, FiniteTruth, 9}}
counterfactual field is concrete: true
results: ⊥ / ⊥
native bytes for one call: 64
counterfactual bytes for one call: 0
native bytes for 1,000 calls: 64000
counterfactual bytes for 1,000 calls: 0
```

I also used `@code_warntype`. It showed this operation field load in `native_loop`:

```
%13 = Base.getproperty(%12, :operation)::BinaryOperation{3, M} where M<:(StaticArraysCore.SMatrix{3, 3, FiniteTruth})
```

I observed the concrete `BinaryOperation{3, StaticArraysCore.SMatrix{3, 3, FiniteTruth, 9}}` for the counterfactual load.

## Run conditions

I ran the command with `--startup-file=no` after compilation warm-up. `uptime` immediately before my Julia process reported:

```
09:05:08 up 1 day, 15:32, 1 user, load average: 4.46, 3.91, 2.63
```

Immediately afterward, `uptime` reported:

```
09:05:33 up 1 day, 15:32, 1 user, load average: 4.87, 4.05, 2.71
```

I observed the same truth value from both versions. I used allocated-byte measurements rather than timings for the comparison; I do not expect these byte counts to depend on machine load.

## What I established

- I confirmed that the cited declarations are present at the cited lines on the recorded commit.
- I confirmed that the operation field's declared type is non-concrete because the table type parameter is omitted.
- I measured allocated bytes through that field and zero allocated bytes through an otherwise equivalent concretely typed layout.
- I isolated the field typing as the explanation for the observed allocation difference.

## What I did not establish

- I did not establish the end-to-end impact on every SoleLogics workload or consumer.
- I did not establish whether changing these declarations is compatible with the intended type hierarchy or API. Is the abstract declaration intentional, and if so, is there another way to retain that intent without boxing? If not, would carrying the table type parameter be appropriate?
- I did not provide a broad timing benchmark. This evidence is allocation-focused; timings will depend on workload and machine conditions.
- I did not propose a specific patch. I would appreciate guidance on the intended representation and whether the maintainers would accept a concretely typed formulation.