Category theory and Computer Science

[enigmahunter]

There is a similar thread below, but I think it is more appropriate to make a new thread because it asks totally different questions.

I am new to category theory and thinking about its possible application to computer science.
Deductive systems based on first order logic (sound and complete) have been successfully applied to A.I knowledge based systems and a wide variety of inference systems so far.

My questions are
1. Do you think category theory, especially categorical logic, can be successfully applicable to deductive reasoning systems?
2. If we use a categorical logic for a possible deductive system, what advantages we can expect from it over traditional First Order Logic (FOL) based deductive systems?
3. What might be the possible theoretical limits for categorical logic?

Any opinions will be appreciated.

 

[fresh_42]

My questions are
1. Do you think category theory, especially categorical logic, can be successfully applicable to deductive reasoning systems?

I think OO programming and relational databases are already close.

2. If we use a categorical logic for a possible deductive system, what advantages we can expect from it over traditional First Order Logic (FOL) based deductive systems?

As in my examples, I think the advantages are a clear defined structure and therewith better maintenance. FOL allows spaghetti code, OO does not.

3. What might be the possible theoretical limits for categorical logic?

I don't think there are limits. Usually if something which looks like a limit appears, the theory will be adapted and developed.

 

[Mark44]

FOL allows spaghetti code, OO does not.

Regarding the latter statement, it depends on what OO language you mean. C++'s and C#'s classes make them object-oriented languages, but you can use their goto statement to make fairly convoluted spaghetti code. In contrast, Java and Python don't support goto, but in the case of Python, you can write a function that transfers control to an arbitrary line in the program.

 

[fresh_42]

One can code C++ like fortran, but then it is not OO. It is the style which makes it OO, the language not so much, although C++ definitely supports OO better than COBOL does. However, objects and morphisms seems like made for classes and methods.

 

[Mark44]

One can code C++ like fortran, but then it is not OO.

Sure, that's true, but I'm talking about C++ code that defines objects as instances of classes, but the implementation of methods on those objects includes code with goto's. Admittedly, this is unusual, but it is allowed, and doesn't contravene OOD.