# Formalisation of Appendix A 'relcons'

Quote from dandl on May 29, 2020, 8:34 amHere is my attempt at a formal definition of a 'relcon' per App-A. It would serve as the definition for a 'function relation' and perhaps even an HHT 'algorithmic relation'.

## Monadic

Given a function f with the type signature Tx->Ty, the relcon S is defined as follows.

Hs = <X,Tx>, <Y,Ty> Bs = { ts | f(X) = Y }## Dyadic

Given a function f with the type signature Tx->Ty->Tz, the relcon S is defined as follows.

Hs = <X,Tx>, <Y,Ty>, <Z,Tz> Bs = { ts | f(X,Y) = Z }For the relcon PLUS in App-A, types Tx, Ty and Tz are all INTEGER, and the dyadic function f is the scalar operator "+".

Here is my attempt at a formal definition of a 'relcon' per App-A. It would serve as the definition for a 'function relation' and perhaps even an HHT 'algorithmic relation'.

### Monadic

Given a function f with the type signature Tx->Ty, the relcon S is defined as follows.

Hs = <X,Tx>, <Y,Ty> Bs = { ts | f(X) = Y }

### Dyadic

Given a function f with the type signature Tx->Ty->Tz, the relcon S is defined as follows.

Hs = <X,Tx>, <Y,Ty>, <Z,Tz> Bs = { ts | f(X,Y) = Z }

For the relcon PLUS in App-A, types Tx, Ty and Tz are all INTEGER, and the dyadic function f is the scalar operator "+".