/.//2 2

[Roger|Dyalog]

What should be the depth of a←/.//2 2? The question arrived in my in-box first thing in the morning. I responded as follows (lightly edited).

This is in the class of “what should it be” rather than something that urgently needs to be fixed, because I do not (can not) believe anybody is depending on the result. OK, fools rush in where angels fear to tread:

To figure out a←/.//2 2, we note that the two leftmost / are the replicate function and the rightmost / is reduction. That is, the expression should be equivalent to a←{⍺/⍵}.{⍺/⍵}/2 2. We have to figure out f/ and f.g.

f/, reduction, is defined as:

      f/vec ←→ ⊂ (0⊃vec) f (1⊃vec) f … f ((¯1+≢vec)⊃vec)    when 1<≢vec.

(A previous version of this text used an erroneous definition of reduction:

      f/vec ←→ (0⊃vec) f¨ (1⊃vec) f¨ … f¨ ((¯1+≢vec)⊃vec)    when 1<≢vec.

The erroneous definition does not change the conclusion but does require changes to some steps in the proof.)

Therefore,

      ⍝
/.//2 2 
{⍺/⍵}.{⍺/⍵}/2 2                   ⍝ assumption about / as hybrid
⊂ (0⊃2 2) ({⍺/⍵}.{⍺/⍵}) (1⊃2 2)   ⍝ definition of f/
⊂ 2 ({⍺/⍵}.{⍺/⍵}) 2               ⍝ ⊃

(Following [Iverson 1980], a proof consists of a list of expressions, each equivalent to its predecessor and annotated by evidence for the equivalence.)

Now we have to figure out what 2 {⍺/⍵}.{⍺/⍵} 2 is supposed to do. f.g, inner product, is defined as follows on vectors (or scalars).

      v0 f.g v1 ←→ f/ v0 g¨ v1

(Note: Inner product in Dyalog APL extends the the definition in ISO/IEC 13751:2001(E), page 121, which says v0 f.g v1 ↔ f/ v0 g v1. NARS2000 uses the same definition as Dyalog APL.)

Therefore,

      ⍝
/.//2 2 
⊂ 2 {⍺/⍵}.{⍺/⍵} 2                 ⍝ continued from above
⊂ {⍺/⍵}/ 2 {⍺/⍵}¨ 2               ⍝ definition of f.g
⊂ {⍺/⍵}/ ⊂ 2{⍺/⍵}2                ⍝ ¨
⊂ {⍺/⍵}/ ⊂ 2 2                    ⍝ /
⊂ ⊂ 2 2                           ⍝ reduction on a single

And what is ≡ ⊂ ⊂ 2 2 ? In Dyalog APL 17.1.35506.0 and also 16.0.33755.0:

      ≡ ⊂ ⊂ 2 2
3

Therefore, the depth of a←/.//2 2 is 3. Should be 3.

I am gonna have my breakfast now. I feel that I’ve earned it.☺