[ivan.moony]

I've been working on a formal language specification for a while, and it finally took a shape I'm satisfied with. If you like, you can take a look at Logos specification in the link below (some twenty minutes read). Logos stands for a (l)anguage (o)f (g)eneral (o)perational (s)emantics. The language represents all of the following:

• Metatheory language formalization
• Theorem prover
• Term rewriting system
• Data computing environment

It reminds of a Lisp (lisp is a usual choice for AI development), and brings some extension on s-expressions. Logos has completely flexible syntax, ready to host *any* theory language, from logic, to lambda calculus, to different embodiments of industry programming languages.

Its syntax is very simple, but it represents a Turing complete language:

Code

a-expr ::= ()
         | identifier
         | a-expr a-expr
         | ‹a-expr›
         | «a-expr»
         | (a-expr)

Some of implementation is already done in a form of context free grammar parser. Further development has something to do with Turing completeness of unrestricted grammar from Chomsky hierarchy, which is an extension of context free grammar. Logos should be a form of a higher order unrestricted grammar metalanguage.

If you are into symbolic AI, Logos could be a place to start with to collect some useful info about knowledge mining. It is aimed to be a language for manipulating formal knowledge.

Read about the project here.

[Zero]

Congratulations. 

Code

«(a ‹⋅› b) ‹+› (a ‹⋅› c)»

(higher (a (lower â‹…) b) (lower +) (a (lower â‹…) b) )

Why did you choose to extend the S-expression syntax?

Also, another question: are parenthesis impacted by the « » and ‹ › ? or identifiers are the only things impacted? For example,

Code

«(f ‹[› x ‹:=› «x» ‹]›) ‹->› f»

Here square brackets are part of the expression, clearly: they are "constantified" 
But aren't the outer « » enough to group the left-hand side?

Sorry, I swear I'm trying real hard to get my head around it all...

[ivan.moony]

Thank you, Zero for a kind word

Code

«(a ‹⋅› b) ‹+› (a ‹⋅› c)»

(higher (a (lower â‹…) b) (lower +) (a (lower â‹…) b) )

actually it is:

Code

«(a ‹⋅› b) ‹+› (a ‹⋅› c)»

higher((a (lower â‹…) b) (lower +) (a (lower â‹…) b) )

Why did you choose to extend the S-expression syntax?

To introduce a clear distinction between variables and constants. And to relate (as an implication) constants and variables denoted by the same symbol. Note that there are no keywords. Only parenthesis and single or double angle quotes.

Also, another question: are parenthesis impacted by the « » and ‹ › ? or identifiers are the only things impacted? For example,

Parenthesis and double angle quotes can be nested, but within nests they have to be both opened and closed. It is not possible to have  `« ... ( ... » ... )`, like it is not possible to have ( ... « ... ) ». The same goes with all combinations of single and double angle quotes and round parenthesis.

 

Code

«(f ‹[› x ‹:=› «x» ‹]›) ‹->› f»

Here square brackets are part of the expression, clearly: they are "constantified" 
But aren't the outer « » enough to group the left-hand side?

The purpose of outer double angle quotes is to connect the left `f` and the right `f`. `‹->›` in between (the operator is defined earlier in the specification) allows us to automatically rewrite the left side with the right side in the context of the expression.

[Zero]

Code

higher((a (lower â‹…) b) (lower +) (a (lower â‹…) b) )

Weird, it feels like jumping from (f x) notation to f(x) notation. I don't get it.

And to relate (as an implication) constants and variables denoted by the same symbol.

z and «z» are related because the identifier is the same, am I correct?

[ivan.moony]

z and «z» are related because the identifier is the same, am I correct?

yes 

[LOCKSUIT]

Is the idea to make many languages speak/translate to the same thing? Like hello & ko-ni-chi-wa = bonjour ?

It appears as if, like Zero's, you use a Tree that builds bigger parts,

But to truly translate languages, you need to master Context. It's not always as simple as hello=bonjour.

I see you say, in replace of context, we can use truth proving to clarify hello=bonjour. Like the frequencies of things that imply/etc. However it is the same thing, using data (context) to show what is what.

?

If we have:
"can you stick this over here"
stick doesn't mean branch, but put

[ivan.moony]

Logos represents merely a translator from whatever to whatever. That's a definition of a term rewriting system. You can imagine translating natural language commands to sequences that output electricity of proper strength at proper wires, needed to move eyes, head, limbs, ... Moreover, if a logic is involved, we can detect contradictions (usually derivations of a form of `A /\ ~ A`) indicating what we translate is a falsehood / lie.

[goaty]

logo is a cool name,  trademark it! 

.

[ivan.moony]

https://en.wikipedia.org/wiki/Logo_(programming_language)

[Zero]

Remaking Logo in Logos would be cool. I love Logo.

[Zero]

Thank you, Zero for a kind word

Code

«(a ‹⋅› b) ‹+› (a ‹⋅› c)»

(higher (a (lower â‹…) b) (lower +) (a (lower â‹…) b) )

actually it is:

Code

«(a ‹⋅› b) ‹+› (a ‹⋅› c)»

higher((a (lower â‹…) b) (lower +) (a (lower â‹…) b) )

Sorry Ivan, can we go over this again please, I didn't understand. I'm interesting in the potential s-expression translation one could make of an a-expression. Why is "higher" outside of parens?

[ivan.moony]

We introduced `higher` and `lower` keywords to demistify double and single angle quotes (these keywords are not included in the language by default). I assume these keywords are of the form

Code

higher (...)
lower (...)

so the expressions inside braces don't get polluted by our new keywords. This example should represent the following (respectively):

Code

«...»
‹...›

braces after our new keywords may be left out if expression inside them stands for a single identifier.

[Zero]

I get it, thx.

Then how would you represent a-expressions in s-expressions?

[ivan.moony]

Then how would you represent a-expressions in s-expressions?

Exactly how you proposed.

[edit]
What's more interesting is internal representation of atoms. By the definition, it is based on implication and a negation, and those two are functionally complete combination. To draw a parallel, implicational logic is based only on these two.

[ivan.moony]

About logic, types and universes

Types of value are a great invention in programming. They are a tool for programmers that report errors in programs before errors are generated in a runtime. As Curry-Howard correspondence teaches us that programs are equal to proofs, type properties may be applied to different theories. For example, some theory may have its syntax and semantics that compose a type. If a theory problem does not conform this type, we may report a syntax or semantic error in the problem setup.
There is a pattern in logic I find particularly interesting regarding to types. Suppose we have a program as a whole in this form:

`((((A -> B) -> C) -> D) -> E) -> ...`,

where `A`, `B`, `C`, ... are logic expressions, and `B` a is subtype of `A`, `C` is a subtype of `B`, `D` is a subtype of `C`, and so on. The idea is that the whole expression should evaluate to true if all the elements are really subtypes each to other, respectively. Let's see how the whole expression behaves:

1. Assume `A` is a top type.
1.1. If there exist an `A` element, then we have a case for typechecking `B -> C` alone, possibly evaluating it to true
1.2. If `A -> B` evaluates to true, then we have a case for typechecking `C -> D` alone, possibly evaluating it to true
1.3. If `B -> C` evaluates to true, then we have a case for typechecking `D -> E` alone, possibly evaluating it to true
1.4. If `C -> D` evaluates to true, then we have a case for typechecking `E -> ...` alone, possibly evaluating it to true
1.5. ...

If `1.1`, `1.2`, ..., onwards all evaluate to true, then the whole `((((A -> B) -> C) -> D) -> E) -> ...` expression is tautology only under one questionable assumption: there has to exist an element of the top type `A`. But does that element really exist without explicitly stating it? Is this a place where we should apply `cogito ergo sum` point from phylosophy?
However, there is a workaround of this problem. In the topmost definition, If `B` follows from `A` by its content, and `C` follows from `A -> B` by its content, then we have a starting tautology spark that lights up the whole Universe of typed expressions without compromising to explicitly state anything outside of this Universe. Hence, we have a self sufficient Universe that evaluates to `true` at its boundary extent if the typing fits correctly each leaf in a sequence from `A` to `true`.