Learning Function Derivatives

It seems that there is a new feature that makes paragraphs all-caps??? WHAT? What-is-this-capitalization-scheme? Or is it just the first line ??

testing… 1, 2, 3… Okay, just first line of first paragraph. lovely!

Now then, having learned of causes for all the quirks in life, we should continue by introducing my own representation for talking about functions. Let the identity brane $P_f:<String, Type>_I$ be the functional association of types with a set of formal parameter names:

    {
        "first parameter"  : Integer
        "second parameter" : Boolean
    }

The actual parameters has a dependently typed I-Brane $P_a$ having instances that look like:

    {
        "first parameter"  : 1
        "second parameter" : False
    }

For convenience, we endow $P_f$ and $P_a$ with mutators: for some $P_f$ we can write $P_{f+\{"\textrm{third parameter}": String\}}$ to mean adding a parameter to the formal parameter specification, $P_{f-["\textrm{first parameter}"]}$ to mean removing a formal parameter. similarly: with $p:P_a$ the expression $p_{[-"\textrm{first paramter}"]}$ has type $P_{a-["\textrm{first parameter}"]}$ and can be used in the full invocation of any function typed $P_{f-["\textrm{first parameter}"]}\rightarrow\Psi$

Finally we type the type signature:

$\Game_b: \big(P_f\rightarrow\Psi\big)\rightarrow P_{f-[b]}\rightarrow(B,B)\rightarrow\Psi\rightarrow\Psi$

so, the type bounds would be able to stipulate that

$\partial_p <: \Game_p$

Note the $\Game_b f$ should mostly be defined for functions $f:P_f\rightarrow\Psi$ that has $b$ as a formal parameter: $b \in P_f$ .

{{{
   [ ] type up concrete example using ML
   [ ] dive into type definitions to be more rigorous.
}}}

The FAM Blog

Art Museum Collection F

Learning Function Derivatives

Leave a Reply Cancel reply

Share this:

Like this:

Related

Leave a Reply Cancel reply