Playing Chiasms, Proemiality and Bifunctoriality

From Conceptual Graphs to Formulas and Procedures

Rudolf Kaehr Dr.phil@

Copyright ThinkArt Lab ISSN 2041-4358



The recent paper about the Tabularity of Polycontextural Logics gets a complementary reflection of the mechanism of dissemination, i.e. distribution and mediation, by focusing on the conditions of mediation of distributed formal systems. In focus are some programming strategies, like bifunctoriality. Historical background information of implementations of polycontextural logics and attempts to formalize Gunther’ s proemial relationship are sketched.
(Work in progress, v. 0.2, 25.July 2012)

1.  Bifunctoriality in Programming

1.1.  Dortmunder Trials in the early 1990s

1.1.1.  Programming Proemiality in SML

fun copy (ref(atom(x,ref Emark,ref wq))) =
        ref(atom(x,ref Emark,ref wq))
   |copy (ref(comb(x,ref Emark,ref wq))) =
        ref(comb(x,ref Emark,ref wq))
   |copy (ref(app((rator,rand),ref Emark,ref wq))) =
        ref(app((copy rator,copy rand),ref Emark,ref wq));

fun equal (ref(atom(x,_,_))) (ref(atom(y,_,_))) = (x=y)
   |equal (ref(comb(x,_,_))) (ref(comb(y,_,_))) = (x=y)
   |equal (ref(app((xrator,xrand),_,_)))
          (ref(app((yrator,yrand),_,_))) =
        (equal xrator yrator) andalso (equal xrand yrand)

PROEM:   |equal
         (ref(app((yrator,yrand),_,_))) =

         (equal xrator yrator) andalso
         (equal xrand yrand)

Diagram : <br /> xrator --> xrand         ↕   ... or) andalso (equal xrand yrand) . <br /> yrator --> yrand       

In combinatory logic terms this construction of Mahler corresponds to the transition from the cominatory logical Sxyz = xz(yz) to the ‘bifunctorial’ construction of proemiality: PR S xy fg = fx(gy). Bifunctoriality was clearly realized in the description and the implementation of the model. But its mathmatical construct of bifunctoriality that would probabily have been of help for the academics to accept the ingeniosity of the model.

"The type of proemial relationship which applies to the parallel evaluation of two combinator expressions (f x) and (g y) cannot be determined from the term structure; instead it can only be found out by looking at the structure of pointer equality z and pointer difference (!≡z) of f, x, g and y.” (Mahler, pLISP, 1992)

In ML terms: P (app1 rator1) (app2 rator2) --> (quote parEval(app1 rator1) parEval(app2 rator2)).

(a :- b): app (xrator,xrand)
(c :- d): app (yrator,yrand)
p a c   :  (equal xrator yrator)     
p b d   :  (equal xrand yrand)

The proposed strategy shall be to start a programming language with bifunctoriality (interchangeability, metamorphosis, chiasm and proemiality) at the very beginning and to show that the common patterns of ordinary programming are just a case of a specific reduction of proemiality.

(P (f x) (g y)) =>    (P parEval(f x) parEval(g y))
"The P-Combinator is not a classical Termtransformation. On the term level it does not change anything. But it produces two asynchronous Tasks (f x) and (g y) that are left on their own.
This Combinator is used to produce explicit parallelity. If both processes work with equal variables, the processes are linked like in (P (f x)(g x)).
With the P-Combinator it is possible to create interesting topologies like (P (f x) (x y)). In the first process x functions as the operand, in the second it is the operator. And this categorical exchange is performed simultaneously!
Such computational topologies are found in Polycontextural Logics (where they are formalized as "Proemial Relations"), meta-level architectures, computational reflection with causal connection and in simulations of self-referential, paradoxical and autopoietic systems.”

Thomas Mahler, pLISP: Parallel Functional Programming

General Scheme: typeset structure

As a simple model I take the 2-domain bifunctoriality as it is implemented in Haskell for a bifunctor.

HASKELL: bimapS :: (a :- b) -> (c :- d) -> p a c :- p b d

Trivially, we get the fundamental transitivity of uni-versal programming (and math) as a reduction of bifunctoriality:

TRANS: (a :- b) -> (b :- c) -> (a :- c)

1.1.2.  Implementing transjunctions

In a first step, the tableaux rules for transjunctions had been established and the distribution over different subsystems had been recognized and formalized. Nevertheless, the tableaux didn’t offer much heuristic guidance to proceed properly a proof of a formula with transjunctions and negations included.

The developed tableaux proof system LOLA, by Bashford and Joemann, applied a rule that properly separates junctional from transjunctional parts of a proof. This was the crucial step for a reasonable heuristics for polycontextural tableaux proofs, supporting both, the machine and the human victim.

I wasn’t aware that the term rule R1 “(α simul δ) et (β simul γ) = (α et β) simul (γ et δ)" is build on the base of the principle of bifunctoriality of the functions “simul” and “par" (Bob Coecke)

The similarity of the logical term rule to the programming strategy for an implementation of the proemial relationship by Mahler wasn’t obvious either.

Nevertheless, the theorem prover LOLA implemented in SML/NJ is properly working albeit the matrix approach to the architecture of polycontextural logics, especially the difference of transpositional (for transjunctions) and replicational 'dimensions’ (for implications), wasn’t conceived in full. Unfortunately, the so called system-changes forced by the sub-system permutations of the negation operations which had been formalized properly years before (early 1970s) didn’t got a direct and full implementation in LOLA-SML/NJ.

Today it has become more clear that a singular theorem prover that is simulating the different contextures generated by transjunctions and replications has to be replaced by a polycontextural theorem prover that is running simultaneously at each contexture autonomically and that are connected by the super-operators.

A first step to a conservative implementation of such a simultaneity might be achieved with the application of parallelism in programming, like the “spawn” concept for ML or HASKELL (GHC).
(cf. A Note on the Tabularity Polycontextural Logics

1.1.3.  Interchange of sorts and universes

Years before the SML adventures, I sketched a proemial relationship between logical universes and sorts as an attempt to extend the conceptual framework of many-sorted predicate logics, a logical system of fundamental relevance for the theoretical study of programming (Joseph Goguen).

"The modeling strategy for chiastic types in polycontextural situations is similar to the modeling strategy for chiasms in many-sorted logics. There, the chiasm is between uni-verse(s) and sorts of disseminated logics. Sorts in one logic can change to become uni-verses in other mediated logics. And in reverse, universes can change to sorts. Thus, chiasms are equally operating on many-sorted algebras as on typed calculi.” (Kaehr, 2006)

Looking back, it turned out that the mathematics of the complex structures of bifunctors in 2-categories had been at hand with the “Doppelkategorien” of Hasse/Michler at least from 1966 on.

I never got a hint emphasizing this direction of thought from any of the academics who had been sceptical to the project of a formalization and implementation of polycontextural logics. The East-German mathematician  Horst Reichel offered me some help but I didn’t see my project mature enough to enter a collaboration with his highly complex category-theoretic formalizations. Jochen Pfalzgraf’s successful formalizations of some aspects of polycontextural logics in the framework of category theory didn't consider the topics of interchangeability and bifunctoriality.

Quite obviously, the concept of bifunctoriality also wasn’t implemented explicitly by any (functional) programming languages at that time (1990). This has changed, outside of academic interests, only recently.

Chiasms of terms and types

"Thus, a type has two functionalities at once, a type as a type and a type as a term. Therefore, this double meaning has to be distributed over different localization of the complex constellation. Otherwise it simply would produce unnecessary conflictive overlapping. The matrix shows clearly the kind of distribution, the diagram is visualizing the process of the chiasm.” (2006)

Today I shall continue:
“and the formula ‘finally’ formalizes the bifunctorial interchangeability of types and terms in the framework of a polycontextural diamond category theory.”

At the ‘end’ of the research program, suddenly stopped by the administration, it turned out that the main advances had been structured by the formula:

 Proemiator    <br /> PR S xy fg = fx (gy)    <br />

<br /> PR S xy fg = ((f --> x <br />        ∐)/g --> ...                                              S3 : (f , g)    -->    (x , y)

Hence, from Gunther’s relational formula of the proemial relaionship to my own diagrammatic formulations, to a proemial LISP and more, the journey got as a next step some academic disguise with the polycontextural subversion of the category-theoretic concept of bifunctoriality.

Dissemination: Introducing the proemial relationship

Early applications of the proemial relationship

Bernhard J. Mitterauer, The proemial synapse. Consciousness generating glial-neuronal units
"This type of relation may be an inevitable prerequisite for any theory of consciousness. Its formal description is as follows: Glia (G) dominate the neuronal components (N) by modifying them. Therefore, G play the role of a relator and N is the relatum. If this relationship changes inversely, N becomes the relator and G the relatum. Since the proemial relationship is cyclically organized, glial-neuronal synapses are capable of changing their relational positions in the sense of an iterative self-reflection mechanism. Hence, it seems to be legitimate to speak of proemial synapses."

1.2.  Functional Programming and Bifunctoriality

1.2.1.  A collection of attempts

Planet Haskell

#if 0
class BifunctorS (p :: Constraint -> Constraint -> Constraint) where
  bimapS :: (a :- b) -> (c :- d) -> p a c :- p b d

In an even more ideal world, it would be enriched using something like

class Category (k :: x -> x -> *) where
  id :: k a a
  (.) :: k b c -> k a b -> k a c
instance Category (:-) where
  id = refl
  (.) = trans

where x is a kind variable, then we could obtain a more baroque and admittedly far less thought-out bifunctor class like:

#if 0
class Bifunctor (p :: x -> y -> z) where
  type Left p :: x -> x -> *
  type Left p = (->)
  type Right p :: y -> y -> *
  type Right p = (->)
  type Cod p :: z -> z -> *
  type Cod p = (->)
  bimap :: Left p a b -> Right p c d -> Cod p (p a c) (p b d)

[Graphics:HTMLFiles/Playing Chiasms and Bifunctoriality_5.gif]

[Graphics:HTMLFiles/Playing Chiasms and Bifunctoriality_6.gif]

1.3.  Bifunctoriality with Combinatory Logic

1.3.1.  Transitivity

Quite obviously, there is no bifunctoriality neither in Combinatory logic nor in Category theory on a basic and first-order level of the primary definitions of the formal languages (systems, calculi, scriptures).

Bifunctoriality enters category theory as a secondary construct on the base of a product. The same happens with combinatory logic and its application in functional programming. Bifunctoriality in functional programming is based on types and their multiplicity on a secure singular ground.

Transjunctions in the sense of polycontextural logic are breaking the linearity of transitivity.

Transjunctions are the primary “functions” or operations of polycontextural logics, both in respect of their conceptual and their numerical relevance.

S functor
fun S f g x = f x (g x)
(* val S = ('a -> ('b -> 'c)) -> (('a -> 'b) -> ('a -> 'c)) *)

BIF: S1, S2, S3 :
S1: S f g x = f x (g x)
S2: S f g x = f x (g x)

<br /> BIF (S1, S2) = ((S1 : f g x = f x (g x) <br />       &nbs ...                                                                                                  3

1.3.2.  Operator/operand chiasm

<br /> bi - fun ∐ : <br /> fun    equal (fst ^1 ( a, _) = a ^1 ... ; -->              snd ^3

<br /> <br /> fst ^3 ( a, _) =    fst ^1 ( a, _) --> snd  ... nbsp; ↕ <br /> snd ^3 ( _, b) = snd ^2 ( _, b) <-- fst ^2 ( a, _)

<br /> fun equal (ref (atom (x, _, _))) (ref (atom (y, _, _))) = (x = y) <br />   &n ... ndalso (equal xrand yrand) <br />     | equal__ = false ; <br />    

Diagram : <br /> xrator --> xrand         ↕   ...       : (equal xrator yrator) andalso (equal xrand yrand) yrator --> yrand

1.3.3.  Distributed buildins

<br /> <br /> (*    ** ** * @ is builtin ** ** *        ... nbsp;                *)

<br /> Multiprocessor system <br /> <br /> (*    ** ** * @ is builtin ** ** *   ... bsp;               *) <br />

val ^(3, 1) @ ^(3, 1) = fn ^(3, 1) : <br /> ' a list -> ' a list -& ...                                                                                                 3

<br /> <br />             (3, 1)           (3, 1)                     (3, 1)                   ... br /> | @ (x :: xs, ys) = <br />          x :: @ (xs, ys)

<br />   Dissemination of the builtin @ ^(3, 1) <br />   <br />  fun @ ^1 <br  ... 3                                                                                                3

2.  Distributed processors

<br /> @  _ (i . j) : Processor active at (i, j) <br /> Ϟ  _ (i . j) :  ...                          3             1.3                                 2.3                 3.3

The super-operators SOPS are the programming strategies, the distributed processor on the kenomic matrix are the programmed machines to be programmed firstly, contexturally, i.e. depending on the loci/places of the processors and secondly, by the types of operations involved. The involved operations then are the localized junctional, transpositional, replicational and reflectional logico-arithmetic operations.

The super-operators are activating or deactivating the disseminated processors according to their operational structure.

Because of the exchange mechanism of operator and operand on the level of the hardware processors, a feature that is not realizable within the possibilities of classical processors and architectures, it is proposed that by taking into account the new possibilities of memristive approaches to realize such mechanisms of interchangeability with a successive application of devices based on memristors and memristive systems, such limits of traditional computation might be, in principle, overcome.

It is understood that the main novelty of memristors is not in the domain of quantities, like speed and storage, but in the functionality of the exchangeability of “processor” and “memory” functions of the “same” computing device at the “same” place.

Hence, the dissemination, defined by distrubution and mediation, of the activity, i.e. inter- and trans-activity of the processors of the grid, is managed by the interchangeability of the main features of computability, computation and memorization, and realized by the application of memristors and their distribution in crossbar systems.

Logical and symbolic processes are distributed over the kenomic matrix. But this distribution is not a static architectonic fact but is involved in the process of interactions between different processors. In this sense, the relization of a transpositional distribution is seen as an interaction between different processors. The ‘main’ processor of a transjunctional operation is ‘sending’ an activation messige to the transpositioned processor to realize the transjunction addressed by the main processor. The main processors in the design are the ‘diagonal’ processors of the grid. This is not a restriction to a mxm-matrix. Other configurations are easily produced, and each processor might play the role of a ‘main’ processor.

typeset structure

<br />

OPER ^(3, 1)  _ [oto] = (Ϟ    --> @         &nbs ...           3.1                                                             3.3                  3.3

<br />         oto : <br /> true1, 3 ?                                                         ... ;                <br />

<br /> Question : true1 .3 (oto) ? <br /> t1 .1 | t2 .1 | t3 .1 <br /> t3 .3 <br />  &nbs ...                          3             1.3                                 2.3                 3.3

<br /> Multi - pr ocessor   model   for   f1H5 : <br />     <br />       H5   =   (X laa Y)   iij   (X laa Y )       <br />

Multi-Processor-System for matrix-distribution of tableaux_forests =
(intra-process:{append, remove, leave}, inter-process: {send, receive}).

(                                                                                              ...                                                                                                  -

<br /> The matrix development as a concurrent procedure with spawn <br />    spawn & ... sp;       | stop2 .1        | stop1 .2