'P' is for Predicate

Hey, all, 'P' day.

'P' should be for π, but that's redundant, right? since π (pronounced 'pee' in math circles) is just the letter 'p' in Greek.

And it's 3.141592653589793238462643383279502884196939937510582097494459230

Yeah, ... I memorized that in high school. For real. People didn't believe me. Every time. So I'd recite it for them, after I wrote it down on a piece of paper so they could verify that I wasn't just spouting digits.

Yeah.

That.

So, but, this post is not about π.

No. Wait. Stop using 22/7 to represent π. That's, like, way off. Way. Use 355/113 instead. And thank Chuck Moore whenever you do.

Okay, done with that aside. Onto this post. This post is about the predicate.

So, what's a predicate?

A predicate is a statement of truth, that you arrive at from other predicates.

Yeah, math and logic are like that: a thing is a thing from other things just like it. Take 'number' for example, any number, x, is just all the previous numbers before x with some starter seed (usually zero or some other representation of null).

Well, that's what a predicate is.

First of all, a predicate is more than a proposition. A proposition is something that you've been seeing already in the alphabet-soup I've been writing, so the proposition for the type of the continuation function is:

(p → r) → r

So, this says, 'given a function that takes a p and gives an r, I can get you an r,' right? Remember that?

Well, a predicate is of this form:

p |- q

Or, if you're feeling your Prolog:

p :- q

A p is true, depending on whether q is true.

(Here we go again with dependent types).

So, what's the difference? I mean, if you just reverse the arrows you could say you have:

q → p

And you could say that, but there is a difference, in that the propositional logic of

p → r

Is all very deterministic whereas the predicate logic of

p :- q

is all very non-deterministic. Predicate logic allows you to base the truth of your consequence on none, one, or several conditions.

So, you could have:

p :- q, r, s.

Which means that p is true if q and r and s are all true, as well.

These are universals, but you can get specific with it, too:

p(x) :- q(x, y), r(y, z).

Which says that there is some x in p, giving a truth, dependent upon the same x in q (associated with some y) being true, along with the same y in r being true with some z.

And, to prove that statement you have to find the (x, y, z) values that satisfy the conditions of that statement. And you keep looking until you find it.

What does that sound like? ... We'll get back to that in a moment.

The neater thing about predicate logic is that the clauses of a predicate can, themselves, be consequences of other predicates:

q(x, y) :- s(y), t(x)
r(a, b) :- t(a), w(b)

And predicates can have multiple statements to arrive at that truth:

q(1, 2).
q(2, 4).
q(3, 6).

The above is saying: "q(1, 2) is true, regardless of anything." And you can take that truth (that fact) and plug it in anywhere. The fact propagates throughout the system.

So, those three facts, along with the relation, q(x, y) :- s(y), t(x), form a predicate. A statement of truth throughout the system, covering all possibilities.

A predicate is a program.

Yeah. Wow.

In Java or Haskell or Ruby a program is thousands, tens of thousands of lines, but in a logic programming languages, like Prolog, for example, a program could be one line or several ... more than a few lines, actually, and you're going off the deep end. And how you program in Prolog is that you string these predicates, these programs, together to create an Universe of related truths, an ontology, in which you can ... play, by which I mean, you can query the system, get an answer (if there is one) or get back several answers, and explore this Universe you've created, or that someone has created for you, as an inquiry into truth.

*Sigh* I miss coding in Prolog. When done neatly, it was so neat to use.

But I don't miss coding in Prolog. It was all dynamically typed, so you could put in anything for your inquiry, and it would try it out, looking for the string "Mama meetzaballs!" even though this particular predicate is about arithmoquines. And I don't miss it for the fact that statements of fact were easy to formulate, but the functional constructs ... ugh, they were terrible.

I need me a programming language that does logic typefully and handles functional logic beautifully, like Haskell does. Maybe ... Idris? ... but Idris doesn't work on my decade-old laptop. Birthday present for moi, then?

Hm.