Logos (experimental version) formal language specification

  • 14 Replies
  • 4199 Views
*

ivan.moony

  • Trusty Member
  • ************
  • Bishop
  • *
  • 1722
    • mind-child
Logos (experimental version) formal language specification
« on: June 24, 2019, 12:10:44 pm »
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.
« Last Edit: November 10, 2022, 08:57:05 am by ivan.moony »

*

Zero

  • Eve
  • ***********
  • 1287
Re: Logos formal language specification
« Reply #1 on: June 24, 2019, 01:31:56 pm »
Congratulations.  O0

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

  • Trusty Member
  • ************
  • Bishop
  • *
  • 1722
    • mind-child
Re: Logos formal language specification
« Reply #2 on: June 24, 2019, 01:57:35 pm »
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

  • Eve
  • ***********
  • 1287
Re: Logos formal language specification
« Reply #3 on: June 24, 2019, 02:47:51 pm »
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.

Quote
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

  • Trusty Member
  • ************
  • Bishop
  • *
  • 1722
    • mind-child
Re: Logos formal language specification
« Reply #4 on: June 24, 2019, 03:05:03 pm »
z and «z» are related because the identifier is the same, am I correct?

yes  ::)

*

LOCKSUIT

  • Emerged from nothing
  • Trusty Member
  • *******************
  • Prometheus
  • *
  • 4659
  • First it wiggles, then it is rewarded.
    • Main Project Thread
Re: Logos formal language specification
« Reply #5 on: June 24, 2019, 11:21:10 pm »
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
Emergent          https://openai.com/blog/

*

ivan.moony

  • Trusty Member
  • ************
  • Bishop
  • *
  • 1722
    • mind-child
Re: Logos formal language specification
« Reply #6 on: June 25, 2019, 08:05:09 am »
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

  • Trusty Member
  • ********
  • Replicant
  • *
  • 552
Re: Logos formal language specification
« Reply #7 on: June 25, 2019, 09:47:00 am »
logo is a cool name,  trademark it!  :D

.

*

ivan.moony

  • Trusty Member
  • ************
  • Bishop
  • *
  • 1722
    • mind-child

*

Zero

  • Eve
  • ***********
  • 1287
Re: Logos formal language specification
« Reply #9 on: June 25, 2019, 09:26:59 pm »
Remaking Logo in Logos would be cool. I love Logo.

*

Zero

  • Eve
  • ***********
  • 1287
Re: Logos formal language specification
« Reply #10 on: June 27, 2019, 09:38:00 am »
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

  • Trusty Member
  • ************
  • Bishop
  • *
  • 1722
    • mind-child
Re: Logos formal language specification
« Reply #11 on: June 27, 2019, 10:23:26 am »
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

  • Eve
  • ***********
  • 1287
Re: Logos formal language specification
« Reply #12 on: June 27, 2019, 10:37:12 am »
I get it, thx.

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

*

ivan.moony

  • Trusty Member
  • ************
  • Bishop
  • *
  • 1722
    • mind-child
Re: Logos formal language specification
« Reply #13 on: June 27, 2019, 11:19:20 am »
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.
« Last Edit: June 27, 2019, 11:44:45 am by ivan.moony »

*

ivan.moony

  • Trusty Member
  • ************
  • Bishop
  • *
  • 1722
    • mind-child
Re: Logos formal language specification
« Reply #14 on: December 28, 2019, 01:36:50 pm »
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`.
« Last Edit: December 28, 2019, 02:52:54 pm by ivan.moony »

 


Say good-bye to GPUs...
by MikeB (AI News )
March 23, 2024, 09:23:52 am
OpenAI Speech-to-Speech Reasoning Demo
by MikeB (AI News )
March 15, 2024, 08:14:02 am
Google Bard report
by ivan.moony (AI News )
February 14, 2024, 04:42:23 pm
Elon Musk's xAI Grok Chatbot
by MikeB (AI News )
December 11, 2023, 06:26:33 am
Nvidia Hype
by 8pla.net (AI News )
December 06, 2023, 10:04:52 pm
How will the OpenAI CEO being Fired affect ChatGPT?
by 8pla.net (AI News )
December 06, 2023, 09:54:25 pm
Independent AI sovereignties
by WriterOfMinds (AI News )
November 08, 2023, 04:51:21 am
LLaMA2 Meta's chatbot released
by 8pla.net (AI News )
October 18, 2023, 11:41:21 pm

Users Online

297 Guests, 1 User
Users active in past 15 minutes:
squarebear
[Trusty Member]

Most Online Today: 335. Most Online Ever: 2369 (November 21, 2020, 04:08:13 pm)

Articles