8
$\begingroup$

HiLog is described as a logic programming language with higher-order syntax, but first-order model theory.

For example, it allows you to define a map over lists:

maplist(F)([],[]).
maplist(F)([X|R],[Y|Z]) <- F(X,Y), maplist(F)(R,Z).

On the second line, F is a predicate, because it's used in F(X, Y), and ∀F is implied, because F is capitalized.

I'm trying to develop an intuition for what's missing here. What would an actual second-order logic programming language let me do that HiLog does not?

It's worth noting that the limitations of first-order logic do not necessarily apply to first-order logic programming languages. For example, Prolog can express the ancestor relation easily, while it's impossible in the standard first-order logic.

This question is about the limitations of HiLog, as a programming language.

$\endgroup$
14
  • $\begingroup$ the easiest way to see the difference between Second Order logic and First Order logic (like set theory) is that in the SO the second sort is semantically required to be really subsets of the first sort, and all of them; where in FO that is not true. E.g. in FO there is no way to define the set of natural numbers N, as there are always nonstandard models. In SO, it is easy to define N and the minimal inductive set. In FO this doesn't hold since the second sort might be interpreted to in nonstandard ways. $\endgroup$
    – Kaveh
    Commented Mar 30 at 17:54
  • $\begingroup$ See also en.wikipedia.org/wiki/System_F $\endgroup$
    – Kaveh
    Commented Mar 30 at 17:55
  • $\begingroup$ @Kaveh It's my understanding that ZFC axioms are FO. If you add them, this lets you express all (or almost all?) of mathematics (Not really my area of expertise) $\endgroup$
    – MWB
    Commented Mar 31 at 15:24
  • $\begingroup$ ZFC has nonstandard models, the set of natural numbers N is not definable in ZFC. Any formula you use to define natural numbers in ZFC will have models which contains nonstandard members that are not in N. You even have countable models for ZFC. In SO because the quantifier for the second order must be the actual power set of N, you can define N. $\endgroup$
    – Kaveh
    Commented Mar 31 at 18:47
  • $\begingroup$ @Kaveh: Some people "require" SO semantics to be a certain thing, but SO kicks & screams and wants to be freed. Henkin understood that, and so do categorical logicians. $\endgroup$ Commented Mar 31 at 21:57

1 Answer 1

3
+50
$\begingroup$

An actual second-order logic programming language would allow you to use second-order quantifiers in a computationally meaningful way. Second-order logic without quantifiers ranging over second-order symbols is conservative over first-order logic (if I remember correctly, someone please correct me if I am wrong).

HiLog seems to be an old language, which to me it just looks like a precursor of λ-prolog, a modern way of adding higher-order features to prolog. I wouldn't spend too much time worrying about what someone thought about its semantics in 1989.

$\endgroup$
13
  • $\begingroup$ Logic programming is not really logic: math.stackexchange.com/questions/3894192 . This is why I find appeals to properties of various logics rather unconvincing (and, but this is my fault, occasionally incomprehensible, as I never studied SOL). I'm hoping to see answers that illustrate what's missing in HiLog, from the programming language perspective. $\endgroup$
    – MWB
    Commented Apr 1 at 20:44
  • 1
    $\begingroup$ Haskell/Lisp/Scheme/ML let you define a map function over singly-linked lists. Is maplist in the question more limited in any way, and if so, how? Is there anything else that's conveniently done in functional programming languages, but cannot be done in HiLog? $\endgroup$
    – MWB
    Commented Apr 1 at 20:53
  • $\begingroup$ You have never studied second-order logic, and you're asking about it on a forum that is meant to be for research-level questions? I think your question is better suited for cs.stackexchange.com. $\endgroup$ Commented Apr 3 at 23:33
  • $\begingroup$ "a precursor of λ-prolog" λ-prolog predates HiLog by 2 years. $\endgroup$
    – MWB
    Commented Apr 4 at 6:46
  • $\begingroup$ "allow you to use second-order quantifiers in a computationally meaningful way." But HiLog allows you to use second-order quantifiers, and it's computationally meaningful (no other way to define maplist in pure Prolog) $\endgroup$
    – MWB
    Commented Apr 4 at 16:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.