Computer languages as examples in formal logic

[Stephen Tashi]

I'm not sure. But let's start out with the recognition that the statements at the core of computer programs are imperative. In contrast, logical statements are declarative. Thus the C statement "A = A && B;" specifies an operation on variable A. Whereas the logical statement "A = A ^ B" is either true or false and is equivalent to "B -> A".

I agree that the nature of imperative statements sets computer languages apart from the types of formal systems that were invented before computers were common.

It seems to me that by this definition, computer programming languages are "wffs".

We have to distinguish between parsers of computer languages versus things related to the execution of their instructions. The terminology "computer language" usually includes both.

When the compiler or interpreter processes the symbol string, it will recognize proper syntax or issue an error message. There might be some wiggle room for interpreted languages - because the interpreter might never attempt to fully parse some sections of the code. But in the case of a compiled language, the compiler will either generate object code or issue error messages - an unambiguous indication of whether the syntax has been followed.

This brings up the distinction between interpreters and compliers. Parsers for compilers recognize only one version of a wff. That version is a complete program. On the way to parsing code for a program they may check that segments of code form special kinds of wffs, such a variable declarations. However, it's hard to make a correspondence between the notion of the many special types of wffs used in parsers with the notion of a single type of wff that is used in formal systems.

The parsing used by interpreters uses a definition of wff that is a more interesting analogy to a formal language than the parsing used by a compiler. I'm glad you brought up interpreters.

I won't claim to be entirely clear on what you are describing, but I believe that we can describe a computer program this way. The notion of true or false is being introduced - it was not mentioned in your definition of "Formal Languages".

Yes, formal languages do not contain any definitions related to the "states" of wffs. There is no requirement that wff can be evaluated as being True or False - or as being 37.6 or the declaration of object.

Formal Systems also don't contain any rules about the "states" of wffs. They contain rules for producing new wffs from given wffs, but they don't contain rules saying how to use a given a"True" wff to produce another "True" wff. The concept of a "True" wff doesn't apply. The notion of "True" has to do with the state of a wff, which is not defined.

Given how I applied "Formal System" to a computer programing (above), all that needs to be done to meet your "Formal Logic" standard is to introduce the notion of whether a program is "true" or "false".
In the case above, I simply presumed the original program (wff) to be True or False. But I believe that extending this to your definition of a "Formal System" leads to the introduction of the concept of "requirements". Given a set of requirements, a computer program can be said to be true (produces the required results) or false (fails to produce the required results). So if the required result is to produce the sequence of numbers that are the first 10,000 prime numbers, then a formal system is defined where any wff can be determined to be either true or false. Similarly, any other well-formed requirements would constitute a new "Formal System".

I'll state the analogy differently.

A parser for a computer language can be regarded as implicitly defining a formal language. I suppose it's the technical documentation for a parser that actually defines the formal language - not the executable code for the parser. In a parser for a compiler, a wff is a valid program. In a parser for an interpreter, a wff is any text that defines an operation the interpreter can execute.

An optimizer for code implicitly defines rules for deriving one valid program in machine code from another valid program in machine code. So the technical description of an optimizer is an example of a Formal System. Similary, a code "clean-up" program that converts valid text for a program in some computer language to valid text for it in the same language implicitly defines a formal system.

If we define a computer program to be "True" if it's execution satisfies some requirements and "False" otherwise, then optimizers and code clean-up programs implicitly define Formal Logics.

 

[Stephen Tashi]

But let's start out with the recognition that the statements at the core of computer programs are imperative. In contrast, logical statements are declarative.

What about this for an aphorism?:

Abstract math deals with "may" and computer programs deal with "must".

Which is to say that mathematics offers many possible ways to proceed from some given inputs. (e.g. from a given wff we may produce another wff, from a given premise we may deduce a particular conclusion.) The executable for a computer program defines how a machine must proceed from a given input. This is true even for computer programs that use pseudo-randomness.

 

[Stephen Tashi]

Are you familiar with Z and Object-Z? They are formal specification languages, built upon the mathematical concepts of sets and mappings. But they're not executable, afaik.

I'm not familiar with Z - or with specification languages in general. Can we make analogy between specification languages and topics that arise in the foundations of math, such as formal logics?

 

[strangerep]

I'm not familiar with Z - or with specification languages in general. Can we make analogy between specification languages and topics that arise in the foundations of math, such as formal logics?

That's not something I can answer in a short post. Probably best if you google "Introduction to Z".

 

[sbrothy]

FYI: https://arxiv.org/abs/2008.08923

Regards.

 

[.Scott]

What about this for an aphorism?:

Abstract math deals with "may" and computer programs deal with "must".

Which is to say that mathematics offers many possible ways to proceed from some given inputs. (e.g. from a given wff we may produce another wff, from a given premise we may deduce a particular conclusion.) The executable for a computer program defines how a machine must proceed from a given input. This is true even for computer programs that use pseudo-randomness.

No. Both "may" and "must" are declaratives. Computer programs are "do". They are inherently goal-oriented. It's the difference between me suggesting that a restaurant is good and me telling the restaurant to do a good job.

Or me telling you to work at the restaurant.
Once we define what constitutes "working at a restaurant", then we can determined whether you have achieved the "working at a restaurant" state.