I hear that Prolog is based in first-order logic. This makes me wonder, C/C++ are based on which higher order logics?
If this question is incorrect, please point out that.
and how are these logics related with grammers (like context sensitive and context free) and how with lambda calculus. Are these things inter-convertible or are totally separate concepts with disjoint application areas?.
On
Prolog is one of the main examples of a logic programming language. It is "based on first-order logic" in a very strong and precise sense.
Indeed, every (pure) prolog consists of nothing more than a list of Horn clauses, which are a restricted form of first-order formulas. In prolog, these take the form of facts such as
cat(Tom).
dog(Rex).
which says that the constant Tom has the satisfies the unary predicate cat and Rex satisfies dog, or rules such as
animal(X) :- cat(X).
animal(X) :- dog(X).
which says that everything which satisfies cat or dog also satisfies animal, and
chimera(X) :- cat(X), dog(X).
says that everything which satisfies both cat and dog satisfies chimera.
To "run" a prolog program, you ask one or more queries. For example, given the above program, the query
?- animal(Tom).
returns the simple answer yes. The query
?- animal(X).
will attempt to find all values of X which satisfy the predicate animal, in this case the prolog interpreter would return X = Tom and X = Rex. The way in which a prolog program works is via the resolution method. This is a very nice theorem proving technique which is especially well suited to work with Horn clauses. When you ask a query to the prolog interpreter, it simply tries to resolve the query using all the Horn clauses supplied by the program and spits out the answer.
As you can see, prolog has such strong ties to first-order logic that it is difficult to find any kind of direct parallel for other types of programming languages — prolog is nothing more and nothing less than a restricted subset of first-order logic.
Other than logic programming languages, Functional programming languages are rooted in the lambda-calculus, combinatory logic, and sometimes categorical logic. In general, the Curry–Howard Correspondence provides a way to relate programming and logic which transgresses programming paradigms. Loosely interpreted, this correspondence says that programming and logic are basically the same, but obviously some forms of programming and logic are more the same than others...
On
Both of the above are absolutely correct. In response to whether C/CPP are first or higher order in logic, I would say first. Remember, $Z_2$ - the formulation for second order logic - is actually a two-sorted first-order arithmetical logic. I don't think I've ever found a 'True' second- or higher-order logic. We know what they'll look like, but most of our language is first-order. [If anyone knows one, please let me know...]
Again, tuppence for the pot.
On
C++/C does not need higher order interpretation. Inheritance and overriding are simply modelled in first order. The modelling can be derived from John McCarthy's circumscription.
It has not yet much transpired that Prolog can be also used in a higher order fashion. But the most easiest way to do higher order programming is by way of the call/n predicates. Here you find a definition of a map predicate:
% map(+Function,+List,-List)
map(_,[],[]).
map(F,[X|Y],[Z|T]) :- call(F,X,Z), map(F,Y,T).
In the above example call/3 is used to add two additional arguments to the closure F and then invoke the resulting term. Yes F can be closure and not only a function symbol. In the simple case a non-function symbol is a compound that carries additional data:
% plus(+Number,+Number,-Number)
plus(X,Y,Z) :- Z is X+Y.
We can then do the following:
?- map(plus(4),[1,2,3],X).
X = [5, 6, 7]
?- map(plus(4.56),[1,2,3],X).
X = [5.56, 6.56, 7.56]
call/n are not yet part of the ISO core standard, but they might become in the near future [1]. A lot of Prolog systems already support them. The call/n is already quite old, it must have been invented around 1984 [2]. The closure can also be used to allow lambda abstraction.
There are a couple of proposals for lambda abstraction. We find the one from Ulrich Neumerkel which mainly uses a new operator +/2 [3], or as part of Logtalk Paulo Moura uses a syntax based on the operator >>/2 [4].
I started using the operator ^/2 in Jekejeke Prolog [5] with a slight different semantic than the one from Ulrich and Paulo, namely local variables need explicit quantification. On the other hand global variables are then automatically determined.
With the ^/2 operator we do not need to define closure predicates. In the above example we do not need to define plus/3 and can directly do:
?- map(A^B^(B is A+4),[1,2,3],X).
X = [5, 6, 7]
?- map(A^B^(B is A+4.56),[1,2,3],X).
X = [5.56, 6.56, 7.56]
The most closest logical interpretation is probably predicate abstraction and not function abstraction. Predicate abstraction is related to the comprehension axiom in set theory. But it can be also done with the lambda notation. An original source is for example [6].
Best Regards
[1] Draft Technical Corrigendum 2 http://www.complang.tuwien.ac.at/ulrich/iso-prolog/dtc2#call
[2] Mycroft, O'Keefe A polymorphic type system for Prolog, AI Journal, August 1984
[3] http://www.complang.tuwien.ac.at/ulrich/Prolog-inedit/ISO-Hiord.html
[4] http://blog.logtalk.org/2009/12/lambda-expressions-in-logtalk/
[6]
Dag Prawitz (1965), Natural Deduction, A Proof-Theoretical Study
See section V: Ramified 2nd Order Logic
When you write a program in any language, you need a machine to execute it. In case of a Prolog it is the interpreter (itself a program executing on some machine) and in case of C/C++ that is the combination of the compiler and computer.
Speaking very roughly, for Prolog programs the behaviour of the interpreter can also be defined in first order logic. That is probably what is meant by saying that Prolog is based on first order logic. C/C++ programs, as far as I know, lack such a theoretically simple description. That is to say that I don't think that C/C++ can be said to be based on a particular widely known logic.
The "behaviour" of the interpreter of some functional languages can be described in lambda calculus, so in a sense these languages are "based" on lambda calculus.
Hope this helps