Rudolf Kaehr Dr.phil^{@}

Copyright ThinkArt Lab ISSN 2041-4358

Abstract

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)

**PROEMIAL**

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)

|equal__=false;

**Discussion**

PROEM: |equal

(ref(app((xrator,xrand),_,_)))

(ref(app((yrator,yrand),_,_))) =

(equal xrator yrator) andalso

(equal xrand 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)).

**Translation**

(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.” *(Mahler)

Thomas Mahler, pLISP: Parallel Functional Programming

http://www.thinkartlab.com/pkl/tm/plisp/ENGLISH.EPS

http://www.thinkartlab.com/pkl/tm/plisp/pr-java/index.htm

**General Scheme:**

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)

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*

http://memristors.memristics.com/Notes%20on%20Polycontextural%20Logics/Notes%20on%20Polycontextural%20Logics.html)

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)

http://www.thinkartlab.com/pkl/lola/poly-Lambda_Calculus.pdf

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 conﬂictive 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:

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*http://www.thinkartlab.com/pkl/media/DERRIDA/Proemial%20Relationship.html

**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."*

www.volitronics-institute.at/files/scanned31.pdf

Planet Haskell

#if 0

class BifunctorS (p :: Constraint -> Constraint -> Constraint) where

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

#endif

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

#ifdef POLYMORPHIC_KINDS

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

#endif

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)

#end

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)

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.

Multi-Processor-System for matrix-distribution of tableaux_forests =

(intra-process:{append, remove, leave}, inter-process: {send, receive}).

^{XXX}