The definition of a language is unclear.

Based on the comments in #4 and #5, I believe that what I have presented as the definition of a language in What is a Language? is not making a whole lot of sense.

My current working theory is that the problem is that it isn't clear how exactly the definition I have given is actually capable of expressing computation. I can talk about my overall perspective generally (and probably should), talking about how I'm really looking at the unfolding of computation over time, and in principle this would be enough information, but I wouldn't be surprised if people still didn't get it right away.

One of the things that I want to be possible is for existing languages to be represented in terms of my definition. In this way, we can talk about existing languages using the theory that is developed as part of this project.

One thing that I could do is try to pick a really simple language or two (a simple C-like, a trivial lambda-calculus), and define them in terms of my definition of a programming language. This would help me work out any kinks, and also establish an example mapping that almost anyone should be able to understand.

My current working theory is that the problem is that it isn't clear how exactly the definition I have given is actually capable of expressing computation

Unfortunately, I'd say that the problems arise even earlier than that:

the definitions are 'ungrounded', i.e. there are too many undefined terms
common words are re-used to mean something quite different than usual.

In particular, nodes, edges, sets of these, are all undefined. Furthermore, 'sets' are constructively very ill-behaved, so you have to be careful with them. Computing tends to use discrete, finite sets, which are just fine. And quite incompatible with interesting notions of polymorphism.

And then, yes, there is no notion of 'reduction', 'stepping', 'transition' or other time-directed entity that usual computations are made of. Of course, Prolog is a programming language too, and its semantics is not really defined in terms of any of those. Nevertheless, there is a still a notion of a "database of rules" and "queries" in Prolog, that give a separation, and then an implicit semantics of 'running' given by resolution. Datalog is another interesting such case.

For most programmers, Prolog and Datalog are extremely foreign and new - but there do exist tutorials for both that start with concrete, tiny examples, to get one acquainted with the basic ideas. Full-fledged Horn-clauses and backtracking with cut is not defined in the first 30 seconds of the introduction... even though they are the heart of Prolog.

Unfortunately, I'd say that the problems arise even earlier than that:

the definitions are 'ungrounded', i.e. there are too many undefined terms

common words are re-used to mean something quite different than usual.

In particular, nodes, edges, sets of these, are all undefined. Furthermore, 'sets' are constructively very ill-behaved, so you have to be careful with them. Computing tends to use discrete, finite sets, which are just fine. And quite incompatible with interesting notions of polymorphism.

This seems like a problem that could be fixed, if I were to provide the appropriate information. I have a pretty good idea of what I want these things to be, so what pieces do I need to add in order to ground my definitions? The rules seem to vary a bit from text to text if the things that I've read are anything to go by, which might be part of the problem here.

And then, yes, there is no notion of 'reduction', 'stepping', 'transition' or other time-directed entity that usual computations are made of. Of course, Prolog is a programming language too, and its semantics is not really defined in terms of any of those. Nevertheless, there is a still a notion of a "database of rules" and "queries" in Prolog, that give a separation, and then an implicit semantics of 'running' given by resolution. Datalog is another interesting such case.

I know that these parts are missing, but they're also not that important for the purpose of solving the analysis problem that I'm interested in here (as in, they're completely unnecessary). They will be needed for building real tools though, so I do plan on getting around to them at some point.

The exact notion of 'execution' will vary a bit from language to language, so my definition of a language would be extended with some abstract thing which a real language would provide some definition for in order to provide such semantics.

For most programmers, Prolog and Datalog are extremely foreign and new - but there do exist tutorials for both that start with concrete, tiny examples, to get one acquainted with the basic ideas.

This was the thinking behind trying to fill out the actual programming language's definitions. I can't really provide those concrete examples without a language to point to. I also can't rely on pre-existing knowledge of languages like predicate calculus or first-order logic like Prolog can.

if I were to provide the appropriate information. I have a pretty good idea of what I want these things to be, so what pieces do I need to add in order to ground my definitions?

Since graphs are so important to your work, you need to motivate why. I still don't really understand this! I have a decent idea of what you're trying to achieve, but then there's this big gap between that and your design decisions.

My guess (which could be entirely wrong!) is that you're trying to model states, sets-of-states and state transitions via some kind of graph. At least, that's not an unreasonable thing to do.

And then, yes, there is no notion of 'reduction', 'stepping', 'transition' or other time-directed entity that usual computations are made of. I know that these parts are missing, but they're also not that important for the purpose of solving the analysis problem that I'm interested in here (as in, they're completely unnecessary).

Which makes me think that I don't understand what you're trying to do after all. A program without any dynamic content is not much of a program.

I also can't rely on pre-existing knowledge of languages [...]

You might nevertheless explain the problem you're trying to solve based on analogies with existing languages. Explaining how they fail to express what you need is an excellent pedagogical way to introduce a brand new way of doing things.

In #3, you linked this paper: https://courses.engr.illinois.edu/cs522/sp2016/GeneralLogics.pdf

I haven't thought about category theory in a while, but I've thought about using it before. I don't think I understood how all the parts fit together well enough to see how I could use it, though.

I'm now reconsidering this. The way category theory specifically ignores internal structure in favor of modelling the relationships between things is perfect for this particular purpose. I wonder if I could do something like what that paper did, but including more about the structure of what a language actually is so that we can talk about design choices and their consequences. I actually have a rough idea of how I would make it work (I think I can see most of the parts), and the definition would support the definition of my entailment operator and the constraints that I've observed on language design so far. I don't yet see exactly how to define 'embedded language' or the cost of performing a particular query over programs, but I think that would be an easier problem to solve once the notion of a language is formalized at all.

My previous attempt was probably trying to be a bit too concrete. That, along with the fact that I'm trying to encode less information in various pieces than you seem to think I am makes it a bit confusing. If I made another attempt based in category theory, in the style of that paper, would it help? Would you be able to understand such a construction well enough that we can use it as a basis for further discussion?

I can see some benefits of having such a definition around, regardless of its value for communication - it is probably a necessary step in producing some of the proofs that I want out of this project. I think it would be quite a bit easier to construct than a definition for my specific language. I also suspect that I will not have a suitable way of talking about program entailment, and thus the motivation and content of this project, without such a language.

I absolutely love category theory - but this seems like a mistake to me. You may indeed eventually end up using category theory in a central way, but to me it would be much more fruitful to start from concrete examples to illustrate what you're trying to do, and then use category theory to show that some examples are in fact instances of the same pattern. Then you can grow your arsenal by using category theory to unveil new patterns that might have been hard to see without it.

Take for example https://arxiv.org/abs/2107.04663 as a good paper that defines a meta-language in which to analyze cost of object languages. The authors are extremely adept at category theory - and yet it doesn't really show up "for real" until p.22.

Note that the fact that the lambda calculus is the "internal language of cartesian closed categories", and concrete work of others on "compiling to categories", the result is that the lambda calculus is an excellent meta-language in which to express many ideas, because it is basically unavoidable.

but to me it would be much more fruitful to start from concrete examples to illustrate what you're trying to do, and then use category theory to show that some examples are in fact instances of the same pattern.

I'm currently interpreting this in this case as saying that I would show examples of things we can do or would like to do, and then show how they're fundamentally related to the query of interest using category theory. Am I correct here, or is that not what you mean?

Take for example https://arxiv.org/abs/2107.04663 as a good paper that defines a meta-language in which to analyze cost of object languages. The authors are extremely adept at category theory - and yet it doesn't really show up "for real" until p.22.

I can't help but notice that, while they don't use category theory too heavily until the end, they do still rely on existing languages for the definition of calf early on. The issue here is that I don't have even one such a language to lean on for the definition of the query of interest. I was thinking that I could use category theory to establish one.

Note that the fact that the lambda calculus is the "internal language of cartesian closed categories", and concrete work of others on "compiling to categories", the result is that the lambda calculus is an excellent meta-language in which to express many ideas, because it is basically unavoidable.

That's all well and good for most theories, but I don't think we'll be able to take advantage of this very much. The Cartesian closed property wouldn't really show up in the foundation that I have in mind. Many of the involved categories may be Cartesian closed but aren't guaranteed to be, and often aren't in practice.

I know I have a backlog of replies. I continue to be extremely interested, I just have too many balls in the air.

but to me it would be much more fruitful to start from concrete examples to illustrate what you're trying to do, and then use category theory to show that some examples are in fact instances of the same pattern.

I'm currently interpreting this in this case as saying that I would show examples of things we can do or would like to do, and then show how they're fundamentally related to the query of interest using category theory. Am I correct here, or is that not what you mean?

Yes, basically. Strong emphasis on both 'can do' and 'trying to do', illustrated concretely.

Take for example https://arxiv.org/abs/2107.04663 as a good paper that defines a meta-language in which to analyze cost of object languages. The authors are extremely adept at category theory - and yet it doesn't really show up "for real" until p.22.

I can't help but notice that, while they don't use category theory too heavily until the end, they do still rely on existing languages for the definition of calf early on. The issue here is that I don't have even one such a language to lean on for the definition of the query of interest. I was thinking that I could use category theory to establish one.

I continue to suggest incremental approaches to defining such a language. Start with an ad hoc language that borrows heavily from existing material. Use it to refine the goals. Show the inadequacy of the language, to motivate a new version of the language that's better. Rinse and repeat.

I have done this. I have indeed used category theory to help me in the process. But I started from an ad hoc language with a semi-formal semantics that seemed adequate, but was flawed. The flaws helped me hone in on what was wrong, the category theory on how to fix it (there was a semantics 'close by' that did work), which then told me how to redo the syntax to match the correct semantics.

I know I have a backlog of replies. I continue to be extremely interested, I just have too many balls in the air.

I also became busy, which is why I haven't replied in a while. I've been thinking about your previous comment (and our whole discussion in general) quite a bit over that time, though. I've pushed Problems With Existing Languages for some reference material for the discussion that follows.

I think we need to give up on the idea that I will be able to present this project in terms of any sort of meaningful contrast against established practice. The fundamental perspective that we are using to even think about established practice is the problem. I can't even clearly state the problem that I am actually trying to solve using the terminology of the existing paradigm, even though it is obviously well-defined - there just aren't words for what I'm doing.

I'm currently interpreting this in this case as saying that I would show examples of things we can do or would like to do, [...]

The problem with this is that we literally don't have the language necessary for me to explain the distinctions between what I want to do and don't want to do. The boundaries in the current paradigm are all misaligned. This is why I was proposing the use of category theory before. I figured that I could construct a completely new model of what programming languages are that would give me the boundaries that I need in order to even be able to talk about the query.

I know you're talking about giving examples, but since existing programming languages don't respect the required boundaries, it's hard to construct them in a way that actually makes sense. I understand at an abstract, high level what the query is doing and what it would mean for abstract objects that are called programs, but I cannot tell you what that operator would really mean in the context of a specific programming language, since there are distinctions that I need to make in order to do so that we don't have the words to make. Arguably, the abstract objects that I am calling programs and the abstract objects that you think of as programs are not actually quite the same thing at this point (I think it very likely that they are not!).

I continue to suggest incremental approaches to defining such a language. Start with an ad hoc language that borrows heavily from existing material. Use it to refine the goals. Show the inadequacy of the language, to motivate a new version of the language that's better. Rinse and repeat.

The problem is that most issues that existing languages can only be fixed by making some sort of fundamental shift in perspective on how we even think about things. This shift necessarily invalidates most or all of the language's actual parts, as well as the terminology that we would use to discuss the functionality and purpose of those parts. The section on structure defined by implementation rather than meaning is a pretty good example of this. Once we start looking at data structures as geometric compositions of fundamental types of relationships, pretty much everything we know about how to design languages is thrown out the window - and that's just one issue.

The fundamental unit of movement from one idea to the next here is happening on a totally different level from what is typical for these sorts of projects. Instead of trying out new language primitives, what I'm really doing is trying out new ways of looking at what it means to write a program. We need to identify the exact space in which the fundamental changes in perspective are being made in order to figure out where the common language still exists. It clearly isn't simply the language design space - it's something much more abstract than that. The shifts in that space are changing the very shape of the language design space itself.

As far as actually presenting what I'm doing, I think a clean-slate approach is going to be necessary on some level, though to exactly what degree is still unknown. I didn't realize before just how much of a language barrier (really a paradigm barrier) has grown between this project and the rest of the world before I started trying to explain things to you. I am thankful for your assistance in illuminating this problem.

Now to figure out what the hell to do about it.

I've been thinking a bit about how we might determine at what point in the conceptual stack our ideas about programming and programming languages diverge. I'm thinking maybe we can try to talk about what we think a program is starting at a very high level, and then add in more and more layers of detail until we find the disconnects.

I think when we talk about programs, we are speaking about roughly the same kind of thing at a high level of abstraction. We probably agree about the meaning of 'computation' on a basic level as well. The view that I am taking of programs more closely aligns with how people think about programs in declarative languages, but we diverge when we get to the parts where we talk about what data and relationships are. As far as I know, all existing declarative languages are based on some sort of variation of FOL, but mine clearly isn't.

So I think we should probably start by trying to find some sort of common understanding of what programs are (in a language-agnostic sense), both within the context of this project, and within the context of the dominant paradigm.

Zistack / program-modeling-language

The definition of a language is unclear. #7