Click here to Skip to main content
Click here to Skip to main content

Primec.h:Curry-Howard Style 1st Order Predicate

, 8 Aug 2014 BSD
Rate this:
Please Sign up or sign in to vote.
Curry-Howard style 1st order predicate logic library in C++. Templates support the policy based choices.

Introduction

I am a reader of the book 'MODERN C++ DESIGN' written by ALEXANDRESCU, ANDREI. This is written about 'Policy based design'. I am also a reader of the book 'Lambda-Calculus and Combinators, an Introduction' written by J. Roger Hindley and Jonathan P. Seldin. In practice this is the only book written about Lambda-cube etc. If you want to learn the topics deeper than this article, it's not a bad idea that you buy this book, but its theories are very complicated. Anyway what does 'Concurrently' means? Matrix calculations are executed background and you play a game in the foreground are not thought concurrently because these programs are irrelevant each other. Strictly speaking concurrently is the executions of the independent parts of a big proof. We have been aware of the existence of a certain proof when we have wrote the concurrent code either intentionally or not. The correspondence between the proof and the code is called Curry-Howard correspondence. Primec.h library is the policy based design template corresponding to the primitive aggregation proofs. Also the functional programming style is supported for the concurrent programming.

Background

It is strange enough that Curry-Howard correspondence is not so famous although it became public in 50'. One reason is that old computers are too slow to avoid the assembler programing so programmers tended to start from hardware structures rather than generic theories. Consequently a good hardware work thought as no bug software and no bug software thought as the implication of the proof perfection and the explicit proving was omitted. Now the multithread era comes and we prepare many locks, mutexes, and schedulers functions. Coding many lock() calls make me sense that I don't want to write stopping codes but running codes and coding except locks make me sense that I don't want to ignore lock() calls because it cause difficult bugs when you write lock() in another line. Which is more significant, locking or locked? Neither. It always depends on every algorithm. The assumption in the proof translated to the data dependency appears wherever the proof used so the program must have the expression power saying here is a race condition is called 'atomic'. But atomics make a order when their timestamps are observed and if no bug is in the program, the variety of its order is restricted. The restriction is called 'monoid'. Primec.h offers primitive atomics and is considered in monoid semantics.

Using the code

First, the concept of 'closed term' in the typed lambda calculus is explained. It is a function dose not include free variables are for the data passing through 'side effect'. But instances such like ones in a C++ child class are allowed because all natural numbers are expressed as functions in the lambda calculus so those are used to define its including function. Function type (functor) is also allowed in this semantics so the pure virtual function is correspond to the closed term. In primec.h the template class is defined as follows.

template <class A,class R> 
class PrimecInhabited ...
virtual class PrimecInhabited *Clone() const =0;
virtual R Inhabit(A &as)=0;
...
template<class C,typename P,typename A,typename R>
class PrimecDerived : public PrimecInhabited<A,R>
{
...

class A is a data type to pass the assumption data to 'closed term' function. class R is a data type to receive the result data from 'closed term' function. Function Inhabited is used in functional programming so Function Clone() is the deep copy function must be prepared. Second,the concept of 'proposition-as-types' in the typed lambda calculus is explained. The type of the function is called 'inhabited' and is the provable proposition formulas. The function instance itself is the called 'inhabit' and is the program code correspond to the proof of the inhabited class. Then the predicate logic supported in primec.c is different style from the mathematical propositional logic and its translation follows. propositional (a==b) <-> predicate equal(a,b) Moreover the used function in the predicate returns not the boolean but the inhabit function (functor) executes the concernment because 'a is equal to b'. Class C is the container class that the concept of predicate implies. Class P is the parameters of the predicate function and the example follows.

class P{
  int a;
int b;
};

A predicate function truly expresses the aggregation such like the tuple (a,b) is a member when the code is written equal(a,b). Thus class Primec in primec.h is the container class of the defined functions in the class parameter L.

template <template <class> class Primec2,template <class> class Primec3,
template <class> class Primec5,class L> 
class Primec : public Primec2<L>,public Primec3<L>,public L
...

In class L some definitions is mandatory as follows

class L{...
   class Parameter {
   ...
   };
   class Assumption {
   ...
   };
   class Result {
   ...
   };
   typedef class PrimecInhabited<Assumption,Result> Inhabited;
   typedef class PrimecDerived<L,Parameter,Assumption,Result> Derived;
   class DomainXXX : public Inhabited
   {
   ...
   };
...
};  
Inhabited *Predicate(const class Parameter &prm) { //(or)
   Inhabited *Include(const class Parameter &prm) { //(or none which depends on its Primec3<class> policy)   ...
   };
   Inhabited *Complement(const class Parameter &prm) { //(or none which depends on its Primec5<class> policy)
   ...
   };
   Inhabited *False() {
   ...
   };
};

Function Predicate(etc.) takes a class Parameter value as input and returns a class Inhabited * pointer value is a pointer to the inhabit instance with pure virtual function Inhabit(). If Parameter value is not in the aggregation, the function returns pointer value that is returned when function False() or Complement() is called. Class Inhabited * pointer is used to call function Inhabit() taking a class Assumption value as input and returning a class Result value. The descendant function Inhabit() internal is arbitrary as far as semantically meaningful.

//Policy choices (in detail) - Primec2 product:(u->u):*  

(If you don't know lambda cube, ignore it.) If you choose Bind, class Parameter value is passed to Predicate() (etc.) without modification. If you choose Free, class Parameter value is ignored and in scope constant that have set by function Variable() is passed to Predicate() instead. In terms of functional programmings this is the side effect, but even when in lambda calculus free variable is used for outer lambda binding so it is only said "Use carefully".

//Primec3 product:
(u->*):[]

If you choose Through, class Parameter value is class Inhabited * pointer value itself so nothing is checked. This is mainly for invalidate the security domain while debug. If you choose Truth,to return the inhabit object function Predicate() is called. If NULL pointer is returned, the return value of the once negated case function defined Primec5 policy is substituted for NULL pointer. If you choose Include,function Inclusion() is called instead of Predicate() and behave quite the same as Predicate() but this keyword is prepared for when all members of the aggregation is included in another aggregation so such like 'inlucdedPredicate-> Predicate()' should be coded.

Primec5 rule:
!!a==a 

If you choose Intuition, rule is ignored and when once or more times negated, the inhabit object is function False() returned data. The inhabit of the rest of policy choices are in the table follows.

choice odd times negated even times negated
VoidTrue False() same as no negated
VoidException False() Exception()
ComplementTrue Complement() same as no negated
ComplementException Complement() Exception()

Function False() takes no input parameter so no aggregation information involved. Function Complement() takes quite the same parameter as function Predicate()(etc.) so the information of the complementary aggregation is expected.

Set and Map are in STL(standard template library) so the lapping library using class primec is also in Primec.h. PrimecSet is remade of Set;

template <typename Key_,typename Compare,typename Alloc=std::allocator<Key_> >
class PrimecSet : public Primec<Bind,Truth,ComplementTrue,PrimecSetLogic<Key_,Compare,Alloc> >   {
   ...
   typedef class Primec<Bind,Truth,ComplementTrue,PrimecSetLogic<Key_,Compare,Alloc> > Logic;
   ...
   class Iterator
   {
   ...
      class Iterator &operator=(Inhabited *trm) {
      ...
      class Iterator &operator=(const class Iterator &itr) {
      ...
      operator Inhabited *() const {
      ...
      class Iterator operator!() {
      ...
      const class Logic::Parameter &Condition() {
      ...
      int Less(class Iterator &big) {
      ...
      int Iterate(int isErase) {
      ...
      int SkipLess(class Logic::Keys &ks,int isErase) {
      ...
      int Value(class Logic::Keys &ks) {
      ...
      int IsIterative() {
      ...
      int IsAll(class Iterator &big) {
      ...
      int IsExist(class Iterator &big) {
      ...
   };
   class Iterator Find(class Logic::Keys *ks) {
   ...
   int Insert(class Logic::Keys *ks) {
...
};

Key_,Compare and Alloc are equivalent to ones in Set<Key_,Compare,Alloc>. Class Iterator is defined to return the inhabit of the element of the aggregation in the lapped shape Iterator when function Find called. Operator=(Inhabited *trm) is object shallow copy with ownership passing, Operator=(const class Iterator &itr) is deep copy, operator Inhabited *() is deep copy and passed in pointer style, operator! is negate and deep copy (original in not negated), function Condition returns the parameter that has used to create Inhabited class object, function Iterate(0) is Iterate, function Iterate(1) is erase the current position element and Iterate, function Value(ks) returns 1 and write the current position element to to ks when the iterator points the valid element or returns 0, and function IsIterative() returns 1 when the Iterator points the element or returns 0 means iterating completes and no element is pointed.

Less(&big) returns 1 when its iterator points earlier than the big or return 0.SkipLess(class Logic::Keys &ks,int isErase) moves the elment position same or later than ks. If the iterator reach to the end, returns 0 means 'not iterative' or return 1. These functions accelerate making the conjunction of two aggregations but only these primitive funciotns is supported because second(or higher) order predicate supports traditionally. IsAll(class Iterator &big) returns 1 when all elements appear through iterate are also appears in iterating big or returns 0. IsExist(class Iterator &big) return 1 when one or more elements appear through iterate are also appears in iterating big or returns 0.

Function Insert(ks) returns 1 when inserting *ks successes, or returns 0 when the error(IN USE) occurred.

If method functions are called with pointer value '*XXX', the ownership of the pointed object is passed and 'delete XXX' is avoided except these error return. If method functions are called with referrenced value 'XXX', the ownership of the referrenced object is not affected and its object delete etc. owes the caller program code.


Class PrimecSetLogic is the class parameter L of the class parameter and in L class Keys is defined as follows.

template <typename Key_,typename Compare,typename Alloc>
class PrimecSetLogic{
    ...
    class Keys {
       public:
          int isWild_;
          Key_ k_;
    };
    ...
};

This class is 'typedef'ed to Logic:: in class PrimecSet. When class PrimecSet::Logic::Keys ks is declared, ks.isWild_==0 doesn't means wild card finding, ks.isWild==1 means wild card finding, and ks.isWlid_==2 means wild card but except ks.k_ finding. Its ks.k_ is typename Key_ and is the element of the container class PrimcSet called key.

Key_ is the same class as set or map in STL except method function void Destruct(). If Key_ is the value type, nothing should do in Desturct(). If Key_ includes the pointer type, its deep delete should be implemented in the function.

PimecMap is remade of Map;

template <class Branch,typename Compare,typename Alloc=std::allocator<std::pair<const typename Branch::Key,Branch *> > >
class PrimecMap : public Primec<Bind,Inclusion,ComplementTrue,PrimecMapLogic<Branch,Compare,Alloc> >

Class Iterator, its methods and class PrimecMap methods are quite the same as class PrimecSet except typename Branch and class Logic::Keys *. Branch is set to class PrmecSet, another class PrimecMap, or a class has the same structure of the methods creating a series number lazyly etc. Of course this class relation means the aggregation inclusion. And the pointer class Logic::Keys * is incremented to pass the key pointer to the child(Branch) aggregation so you must declare class Logic::Keys keylist[(depth of the Branch to the PrimecSet (or never has Branch nest class))] and enter the finding conditions in it.

The sample program main.c is a 4-tuple concurrent database accessed through telnet. First main.c is executed with local port No. Then 'Telnet localhost <local port no.>' is executed. Through telnet,you can enter these commands;

Input Meaning
(x,y,z,a) insert tuple
:(x,y,z,a) list matching tuple
:!(x,y,z,a) list not matching tuple
~(x,y,z,a) delete matching tuple
~!(x,y,z,a) delete not matching tuple
key can be set to wild card as follows.
:(x,y,z,*) list matching tuple ignoring 4th key
:(x,y,z,!a) list matching tuple excpet (4th key)==a

Points of Interest

First of all, class PrimecSet and class PrimecMap have a performance trouble because these consist of STL codes. STL library is not designed for mutlithread uses then the container level mutex must be added although codes in Primec.h obtain the element level iterator reference counter. But decomposing any standard is risky so performance tuning is suspended. Second of all, please use this version of library in the multithread program and inform me how slow or not. API is probably stable and performance tuning is completely library internal so what you only have to do in the future is change the Primec.h version and recompile once. Moreover this codes must be the fastest because the concurrent scheduler which examine the race condition in the way of checking the aggregations runs so sequentially(before concurrently) that occurs the performance bottleneck.

The biggest issue is that a inhabit is always a iterator. Strictly speaking, it's no. If you use two inhabits of the flexible proofs, there is a chance of the reduction(compile time optimization which is calculating constant valuables) so inhabits are solely considered as closed terms. But the grammar of C++ can't make these static problems express coolly. And also the expression power of the template parameter is another issue. It can express the most primitive semantics about the 1st order logic. Naturally it is no discover that template parameters which are higher order logic express 1st order logic. What we must check is this library force the programmers to use only 1st order logic or causes the compile time error. In terms of C++ grammar these are very useful if these can as fellows.

sizeof(union TYPELIST(descendantsOf class 'base'))
TYPELIST(union 'u')
TYPELIST(haveAMembersOf class 'c')

In short, it might be better to merge the grammar types into the predicate logic but not.

Object ownership problem is serious. In Ver 0.1 deep copy semantics is adpoted, but 'deep copy and delete' behaviour is observed. It is slow, then in Ver 0.2 ownership passing with
pointer type semantics is introdueced. This is similar to 'std::auto_ptr' in STL but is not
class type but semantics. Use of the pointer type at a function call is restricted to the ownership passing. Two semantics are considerable.

sem1()
{
        class X abc;
        class Y *obj;
        ...
        obj=new Y(1,2,3);
        if((obj=abc.func1(obj))==NULL) {
                printf("Success\n");
                ...
        } else {
                pirntf("Rejected\n");
                ...
                delete obj;
        }
}

sem2()
{
        class X abc;
        class Y *obj;
        ...
        obj=new Y(1,2,3);
        if(abc.fun2(obj)==ERROR) {
                printf("Rejected\n");
                ...
                delete obj;
        } else {
        printf("Success\n");
        ...
        /* 'obj=NULL;' If you want compatibility to std::auto_ptr */
    }    
}

Someone feels strange that reference counting pointers are not adopted, but in many cases reference count can be proved a constant at compile time so we have better reconsider these algorithms.

History

Ver 0.1 Mar. 2014

Ver 0.2 Aug. 2014 (source code updated.) 

License

This article, along with any associated source code and files, is licensed under The BSD License

Share

About the Author

T. Ogawa 2012
Software Developer
Japan Japan
I'm an old programer. My Skill starts from i8085 assembler
coding. The Object oriented programing is over 20 years
and I achived the Policy based programing. Latest interests
are pthreads and pararell programings.

Comments and Discussions

 
-- There are no messages in this forum --
| Advertise | Privacy | Terms of Use | Mobile
Web01 | 2.8.150331.1 | Last Updated 8 Aug 2014
Article Copyright 2014 by T. Ogawa 2012
Everything else Copyright © CodeProject, 1999-2015
Layout: fixed | fluid