[ivan.moony]

Can feature constraints replace the need for variables?

[infurl]

Can feature constraints replace the need for variables?

That depends on what you're using variables for. I'm certainly not using any variables for parsing.

[ivan.moony]

Can feature constraints replace the need for variables?

That depends on what you're using variables for. I'm certainly not using any variables for parsing.

For example, to calculate factorial or Fibonacci numbers (happens in recursion)?

[infurl]

It sounds to me like you're searching for The One True Hammer(tm) when you should just be using the best tool for any given job.

[ivan.moony]

Yeah, the mother of all the hammers sounds just about right! 

[ivan.moony]

I tidied up the parser output a bit and introduced `expected: ... at position ...` type of syntax error messages. Syntax will loose a clear distinction from semantics in later project phases, when the parser will be able to detect i.e. if a variable is declared before assignment using only exp-log patterns.

[ivan.moony]

Current project status:
Still working on logical programming language for describing other formal languages, based on extension of original parsing technology. Anytime soon, there will be completely functional general CFG parser which then has to be extended in two steps, first to be Turing complete, then to include appropriate logical operators (I observe productions as implications).

Last insights about program synthesis:
It should be possible to send arbitrary input and output pairs along the lambda calculus definition. From just that, the system could construct a set of possible specific lambda functions that turn provided inputs to provided outputs. If instead of lambda calculus we provide a definition of some other language, other kinds of source code may be synthesized. I'm still wondering about troubles with speed that may pop up, mostly around recursive functions. Anyway, simply typed LC should work well if I'm not mistaken.

Last insights about AI:
The same procedure for program synthesis should work as a replacement for what artificial neural networks provide. NNs are trained by pairing inputs to outputs, and in between, neuron set does all the future magic of firing outputs upon recognized inputs. With completely formalizing a Turing complete environment, instead of general neuron set, we may put 100% accurate synthesized pieces of code. Although the general idea should work, I'm afraid that details about AI would be pretty tricky to grasp.

What competition has to show on this subject:
Here is interesting video about business use - very insightful - https://www.microsoft.com/en-us/research/group/prose/

[ivan.moony]

I composed an example for visualizing natural deduction logical proofs: http://ocog.atspace.cc/.

As exp-log heavily relies on natural deduction, this kind of visualization may be very relevant to it. I put the example online, and offered the whole library for use in OpenCog foundation (they also deal with natural deduction). This is still far away from concrete AI advancement I'm trying to do with exp-log, but beter something than nothing.

Natural deduction comprises rules of the form:

Code

  premises  
------------
 conclusion

Suppose we have a natural deduction proof composition:

Code

  ---   ---   ---     ---   ---   ---     ---   ---   ---
   I     J     K       L     M     N       P     Q     R
 -----------------   -----------------   -----------------
         A                   B                   C
-----------------------------------------------------------
                             X

We can already see the tree-like composition, but as it may span over a very wide and tall area, it may be required to represent it within an on-demand scaling system. The online example roughly shows what I have imagined for proof representation. In the example you can play with ovals, dragging them around and in or out the central area, zooming proof parts of the current interest. Notice how it is possible to represent and navigate nearly infinite length proofs, assuming enough memory space.

I already had possible plans for fusing exp-log and fract-exp in the future, and noted example shows one of the possibilities. But I'm still actively developing exp-log, so it is a long road before reaching the visualization state.

[ivan.moony]

I decided to change the direction of the project exp-log.

In fact, it will change its name and it will be degraded to support only Prolog like rules in Lisp-ish disguise, applied to string parsing and term rewriting, focusing to provide a form of server side scripting technology. It will still remain to be applicable to logic problem solving, only in a form of server side scripting language, and with the main focus on delivering web contents. If one wants to implement exp-log, one will be able to define it within this new scripting language more-or-less with ease.

The existing project code remains actual, as the new project direction follows a subset of the previously planned goal project. I'm thinking learning Go to program native server when the time comes. Until then, I'm trying to keep js code below 500 LOC. As for the current project iteration, I plan to finally pack up exp-log draft document and put it aside as a curiosity content. New draft is coming soon.

To get a glimpse of the new project attire, visit this link.

[ivan.moony]

A story about contradiction (or: "blah, that boring logic stuff", if you are not crazy)

What I'm dealing here as building blocks in my language is a kind of Horn clause form of formulas. Horn clauses are of the form `a /\ b /\ c /\ ... -> u` while I deal with their extended form `a /\ b /\ c /\ ... -> u \/ v \/ w \/ ...`, which is equivalent of conjunctive normal form `¬a \/ ¬b \/ ¬c \/ ... \/ u \/ v \/ w \/...` of general logical formulas.

An interesting story comes when doing a proof construction. We start from origin multiple axioms in a form `true -> axiom`, then come assumptions in a form `a -> b` in between, and we try to connect it to `goal -> false` at the other end. One may ask: "Why the goal implies false? If the goal is false, then the whole formula conglomerate is false!" The answer may lay in the fact that one of the proving methods in logic is proof-by-contradiction. we state axioms and assumptions, we state the negated goal (`¬goal` is the same as `goal -> false`), and we try to derive a general contradiction. That means that if we prove that "`¬goal` yields contradiction", the same proof is read as: "non-negated `goal` is true" because of dual properties of the logic itself.

I find this story interesting because if we keep the whole formula conglomerate in `true -> axioms`, `a -> b`, `goal -> false` form, the whole conglomerate evaluates to false. Under proof of `axioms -> goal`, it is like we directly write `true -> false` - this is a contradiction. This kind of reminds me of imaginary numbers in math - (square root of -1) - although they are non-existent, we can do math with them, dragging them through all kinds of usual formulas, ultimately producing actually useful results at the end, when imaginary numbers are reduced in the previous process. Likewise, in this like logical systems (Prolog also accounts to this kind), we are manipulating contradictory form of clauses to produce a result that is actually true.

Funny, isn't it? Like we are trying to say a truth by stating a bunch of lies. And it all works at the end!

[Zero]

You know, I have trouble handling negation as failure. I just can't get my head around it yet. A few days ago, I was working on... wait. Ok, done uploaded here. It's a knowledge base-structure thing, in French sorry, but it doesn't matter. Here is the problem:

In the list, there is a "is an instance of" relation. It was super easy to represent in Prolog, no problem. Then, the plan was to also have a "is not an instance of" relation. Dang. I could never get it to work properly.

How do you say that something does not hold, in logic? How does this mind-skkkrrrr****ing negation as failure work? Can your current system handle this kind of... non-relation? The idea would be something like:
- If I say it is true, then it is true
- If I say it is false, then it is false
- If I say nothing about it, then we don't know yet, and we should be able to "work" with the fact that we don't know it

I know it's about open-world vs closed world assumption, but I just don't get it.

[ivan.moony]

I think your reasoning in three bullets stands for open world logic.

I also had problems with negation. I had some attempts to treat everything as a closed world, i.e. if something is not defined, then it is false, but it didn't sound consistent to me. I also struggled with self-definition, as I didn't have a way to express a query that returns true if I have a proof for a formula, otherwise it returns false. I mean I had idea about a dirty hack, but it looked like a perpetuum mobile thing, totally out of harmony with the Universe.

But I managed to avoid all that story about constants true / false. I completely expelled constants from my theoretical language. First level theory manages to define the next level theory, which again may hold another level theory, and so on, even if theories at all levels are the same. And there seems to be a restriction that any level theory can't define itself in the same level (see Tarski's undefinability theorem), assuming the theory is consistent, but it seems OK for the next level to hold anything we want, restricted by previous level.

So the road led me here: the thing is, all the formulas I care about, may be considered as stored in format: `~a \/ ~b \/ ~c \/ ... \/ u \/ v \/ w ...`. When converted to super-horn clause (hehe, what a name), negated atoms go to the conjunction on the left, and non-negated to the disjunction on the right of implication symbol. If the left side is an empty conjunction, then the left side is true. If the right side is an empty disjunction, then the right side is false. Empty conjunction and empty disjunction is the furthest I go when it comes to constants. That means I can't even store the truth on the right side (because it yields a tautology) or the falsehood on the left side (also yields tautology) of the implication.

See, this might be of your interest: I figured (Wikipedia and co.), negation of an atom is the same as we write `atom -> false`. Now, I don't have `false` defined internally, but it could be a user defined atom as any other. So, when I enter rules for it in a form like:

Code

            (       (~ 'true') -> 'false' ) /\
            (      (~ 'false') -> 'true'  ) /\

            (    (@a /\ ~ @a ) -> 'false' ) /\
            (  (@a /\ 'true' ) -> @a      ) /\
            ( (@a /\ 'false' ) -> 'false' ) /\
            
            (    (@a \/ ~ @a ) -> 'true'  ) /\
            (  (@a \/ 'true' ) -> 'true'  ) /\
            ( (@a \/ 'false' ) -> @a      )

and when I run organic-mind-proving-engine, things line up neatly: if the whole formula is contradictory, alone `false` is deduced; if the whole formula is tautology, alone `true` is deduced. This user-defined mechanism persuaded me to stop chasing built-in negation, and I thought - the best thing is to avoid explicit negation when it comes to exposing it to end users. All I have are empty left side conjunctions and empty right side disjunctions for my internal interpretations - only for noting axioms and goals. Otherwise, it is up to users to introduce negation, or not, it is all about user defined theories that may or may not depend on negations. As for internal interpretation, things are getting pretty weird (see the previous post): right side empty disjunction - falsehood - is interpreted as a success, following the proof by contradiction.

Anyway, there's a parser I'm dragging now for years which I plan to extend by left side conjunctions and right side disjunctions (had that version also, but things changed so I have to re-do it for the new version). I'm planing not to tell the computer a thing about truth / falsehood, yet to leave to the algorithm to interpret empty sides just like any other element filled sides, but in empty `for` loops, by the same code, and see what happens. If the whole thing would work OK, that would be it, I would be out of the need for constants `true` and `false`, even internally.

And to develop things further, why these two constants: true / false? why not a probability range between 0 and 1, with 0 being false and 1 being true? And why to restrict ourselves to logic, why not 3 elements fractionals like red / green / blue combinations? There should be a numerous interpretations, as there are a numerous theories about everything else but logic. Now it made sense to me to leave out binary constants like true and false out of equation: users can define whatever they want, providing specific rules to handle those constants. Thus, I opted out for no built-in constants. I exploited logic as a food for thought to form the core language in my mind, but it happens to apply to any area, not only logic, and that should work without built-in constants, if I'm not mistaken.

[Zero]

But, wouldn't you say that conjunction, disjunction, implication and negation of atoms are anyway implicitly "carrying" the notions of true/false/anyConstant? I mean, if we use some many-valued logic, we need to rewrite the tables of these operators ok, but there are still tables, which hold "things" in their cells! How can we have operators without having constants?

[ivan.moony]

But, wouldn't you say that conjunction, disjunction, implication and negation of atoms are anyway implicitly "carrying" the notions of true/false/anyConstant? I mean, if we use some many-valued logic, we need to rewrite the tables of these operators ok, but there are still tables, which hold "things" in their cells! How can we have operators without having constants?

What I'm trying to articulate is that I want to leave constants out of the system, meaning there is no built-in constants. Of course there is a notion of a constant, but users choose what constant they would use, provided interrelations between them by stating user defined formulas. Those formulas reason about the constants, but all of them are user-defined, not hard-coded.

I wouldn't want to intimidate you, but there is a stream in computing science that goes even further than I go when it comes to constants. For example, combinatory logic that relates to lambda calculus, is composed only of functions. Even constants like `true` and `false` are defined as functions like `λx.λy.x` and `λx.λy.y`. There are also Church numerals that map all the numbers to lambda functions, without introducing a single constant, only combinators (combinators are functions that use no constants, only variables and previously defined combinators). But I'm not going that far because I want to achieve a clear distinction between the input/output constants (user defined and exposed to outer world) and internal rule system (also user defined, but not exposed to outer world).

[ivan.moony]

You know, I have trouble handling negation as failure. I just can't get my head around it yet. A few days ago, I was working on... wait. Ok, done uploaded here. It's a knowledge base-structure thing, in French sorry, but it doesn't matter. Here is the problem:

In the list, there is a "is an instance of" relation. It was super easy to represent in Prolog, no problem. Then, the plan was to also have a "is not an instance of" relation. Dang. I could never get it to work properly.

How do you say that something does not hold, in logic? How does this mind-skkkrrrr****ing negation as failure work? Can your current system handle this kind of... non-relation? The idea would be something like:
- If I say it is true, then it is true
- If I say it is false, then it is false
- If I say nothing about it, then we don't know yet, and we should be able to "work" with the fact that we don't know it

I know it's about open-world vs closed world assumption, but I just don't get it.

I had the same problem, but classical logic gave me only a half-solution - If something is true or false, or it can be proven true or false, then we can detect it. But if we don't know that something, or there is no proof of that something, then we can't detect its current non-existence.

• when it does exist:
  Let's say we write axioms and a bunch of assumptions. Then, if we want to detect if a formula is true, we can write: `formula -> something-to-assert-if-the-formula-is-true`. We can also detect proofs: if these are existing formulas: `A -> whatever-comes-in-between` and `whatever-comes-in-between -> B`), then we can write something like: `(A -> B) -> something-to-assert-if-A-entails-B`.
  
  
• when it does not exist:
  Detection if a formula is *not* asserted, or a proof is *not* available, has given me some fair trouble. My initial solution was to include a dirty hack in the language, completely out of phase with classical logic. Maybe the reason why it is out of phase could be found from extrapolating result of Tarski's undefinability theorem (you can't define what is the truth of a theory within that theory). There may be also a connection to Gödel's incompleteness theorems (if a theory is consistent, then it can't be complete - to be complete it has to be inconsistent).
  
  

My final solution was to break theories to sub-levels - the first level defines what is true or not in the second level, the second level defines what is true or not in the third level, and so on. That way I kept consistency. And it somehow sounded like a right solution.

Prolog? You should be able to detect element of set existence in Prolog, you just have to be explicit. First you define a set with its elements. Then you loop through all the elements, reporting true if you find the element, or false if the loop falls through. You just have to deal with equality comparison, which I guess is a Prolog's dirty hack (or defined in a previous level theory, if you like). In classical logic, equality can't be defined as a user defined predicate because you *can* detect if something is equal, but you *can not* detect if something is not equal (the same problem - you can detect a proof of `A = B`, but you can't detect non-existence of proof of `A = B`. Nevertheless, you can separately define a proof of `A != B`, but it may be that story of closed worlds, i.e. `digit != 1 <-> digit = 0 \/ digit = 2 \/ digit = 3 \/ ... \/ digit = 9`). I guess this is why *logic with equality* is a separate chapter in logic books.