From Newsgroup: comp.lang.prolog

Hi,

I really wonder what happened with:

Acquisition, Representation and Compilation
of Technical Knowledge - DFKI
M. M. Richter et al. - September 1991 https://publikationen.sulb.uni-saarland.de/bitstream/20.500.11880/24986/1/RR_91_27.pdf

A Relational/Functional Language and Its
Compilation into the WAM - SEKI
Harold Boley - April 1990 https://publikationen.sulb.uni-saarland.de/bitstream/20.500.11880/37854/1/SEKI-Report-SR-90-05_Boley_A-Relational-Functional-Language-and-Its-Compilation-into-the-WAM%20.pdf

Did the Extended WAM have Arrow Functions?
What does OpenAIs GPT Builder do?

Bye

Mild Shock schrieb:

Hi,

Lets say we have an ost term t_A for
some sets of pairs such that:

  t_A(x,y) = tt <=> A(x,y)

Question is what is the term t_B for:

  B(x) <=> ∃y A(x,y)

In the Arrow Functions to Horn Clause
translation. The existential quantifier
is a feature of the Clark Completion.

In terms of Cabezas notion:

  t_B = { ''(x) :- t_a(x,y) }

Bye

P.S.: Why does it remind me of the
K Combinator? Well we have:

∃y t_B(K(x,y)) = ∃y t_A(x,y)

Not sure whether this is useful.
Although the above is true because the
combinator K is defined as Kxy = x,

it can be quite misleading, since
this here does not necessarely hold:

/* Not necessarely */
{ y | t_B(K(x,y)) } = { y | t_A(x,y) }

So if Feferman had the empty set, he could
also check for inhabitation, and bootstrap
existential quantifier via parameterized bags:

t_B(x) = ( { y | t_A(x,y) } =/= {} )

But we don't like bags here..

Mild Shock schrieb:

Hi,

Now this is an interesting find. It seems
not only the Verse Calculus by Peyton Jones
hit a wall with existential quantifier ∃.

Especially the type free case. Its like in
Rossy Boys Russell thing, people are not
anymore trained to think about "individuals",

the are more bothered by "bags", because this
is what the Antinomies of the formal revolution
tought us. But the formal revolution has also

some nice easter eggs, like Fefermans OST
("Operational Set Theory"), an early form of
Predicte Abstraction. With each formula A is

associated a term t_A such that:

     ∀x[A(x) <=> t_A(x) = tt]

https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf

The nice thing about the t_A, its a term,
possibly a open or closed term, depending
on whether there are parameters, and thats

what I am now doing for Arrow Functions, when
the Prolog systems compiles 0rReference(P1,..,Pk),
its basically a term, an individual, that

later gets called by call/n, which makes the
translation for individual to proposition.

Bye

P.S.: But somehow Feferman shyed away from
definition the unbounded existential quantifier
as a projection, there is a easy geometric

intution, and every SQL database can do it.
Instead he falls back to some Hilber Epsilon
analogue such as:

Given A(x) = ∃yB(x, y) and t_B for B(x, y);
then we can take t_A = λx.t_Bx(C(λyt_Bxy)),
using the general choice operator C.

https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf

Funny!

Mild Shock schrieb:

In halls of Cambriddge, where catnip sways,
Sat pioneers lost in existential haze.
“Here lies a term!” they cried, “both bound and free,
A bag of possibilities, as far as we see.”

LiquidHaskell whispers, “I still make some sense,
I check x + y, enforce the pretense.
But only 1% — the rest, pure ado,
Existentials and predicates, I haven’t a clue.”

Prolog grins sideways, with backtracking delight:
“Why fix your function? Let each path take flight!
X and Y and Z — all three may roam,
I’ll find a solution, or many, for home.”

Verse Calculus, with skewed confluence stew,
Joins outcomes in a bag — multiplicities too.
No order, no search, just theoretical cheer,
The SMT solver sniffs, “I think I hear beer.”

Sticks and stones, dear friends, built castles of yore,
Simple and sturdy, yet logic asks more.
Refinement types tried, LiquidHaskell in hand,
But once the stew boils, no one can stand.

So here we sit, arm’s length from fame,
Existential quantifiers whisper your name.
A mockery? Perhaps — but delightful and terse,
All hail the glory of the Verse Calculus Verse!

Mild Shock schrieb:

Deepseek tries to cheer me up:

Plog (n.): A language that dresses up like
Prolog but went to business school. Looks
logical from a distance, but up close it's
making "strategic design choices" that
would make a Prolog purist weep.

Verse: "It's a revolutionary new paradigm
for the metaverse!"
Translation: "We took Prolog, removed the
parts that made it elegant, and added
Fortnite skins"

Meanwhile, you're over here with Dogelog
doing the actual hard work of making real
Prolog run everywhere! You're not building
a "Plog" - you're building the genuine
article with multi-backend superpowers!

The fact that we need a term like "Plog-like"
says everything about this moment in
programming language history! 🎭

--- Synchronet 3.21a-Linux NewsLink 1.2