Defining functions: types and names

Given

let multiplication_table =
      0 -> 0 -> 0
    + 0 -> 1 -> 0
    + 1 -> 0 -> 0
    + 1 -> 1 -> 1
    + 0 -> 2 -> 0
    + 2 -> 0 -> 0
    + 2 -> 1 -> 2
    + 1 -> 2 -> 2
    + 2 -> 2 -> 4

then these two funs

fun mul_product_style: Int -> Int -> Int {
    multiplication_table
}

fun mul_dereference_style[x, y: Int]: Int{
    y::(x::(multiplication_table))
}

work exactly the same way at the call site,

run {
    all x, y: {i: Int | 0 <= i && i < 2} | {
             mul_product_style[x,y]  =        mul_dereference_style[x,y]
             mul_product_style[x][y] =        mul_dereference_style[x][y]
          x::mul_product_style[y]    =     x::mul_dereference_style[y]
      y::(x::mul_product_style)      = y::(x::mul_dereference_style)
        y.(x.mul_product_style)      =   y.(x.mul_dereference_style) 
    }
}

which suggests that they are the same relation. Questions:

  1. Why does mul_dereference_style not create a relation that may be interrogated in the evaluator when mul_product_style does?
  2. Why does not mul_product_style = mul_dereference_style compile?
    2.1 The error suggests that mul_dereference_style can only be applied and not used as a name, as mul_product_style apparently can be, why this difference?
  3. fun mul_product_style: Int -> Int -> Int {multiplication_table} does compile but fun mul_dereference_style[x, y: Int]: Int{ multiplication_table} does not. It seems that the two functions in fact of dissimilar types, even though they work identically in the run paragraph. Why so?