Computer languages as examples in formal logic

[Stephen Tashi]

TL;DR Summary

For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?

A computer language is not a clear example of a formal language, a formal system, or a formal logic. Can we modify the rules for a computer language to create clear examples?

My non-authoritative classification of topics in mathematical logc is:

1. Formal languages. A formal language is defined by a set of rules that define which strings of symbols are "well formed formulas" (wffs). A wff has no semantic interpretation other than being syntactically correct according the rules of the formal language. Within the context of a formal language, a wff does not represent a statement that is True or False or a mathematical function.

2. Formal systems: A formal system is a formal language plus a set of "production rules". If we write down an initial wff, the production rules describe permissible operations for "deriving" other wffs from the initial wff. Within the context of a formal system, there is no interpretation that wffs involved are True (or False), so the "derivations" are not mathematical proofs that deduce True statements from some initial statement that is assumed to be True.

3. Formal logics: A consistent formal two-valued logic is a formal system with additional requirements. The wffs must each be assigned exactly one of two possible values, either True or False. (As a matter of vocabulary, in a specific formal language, the wffs are assigned specific values. Speaking of "formal language" as a generality, it is a set of specific formal languages. The value assigned to a wff may vary between two different laguages in that set.) The production rules must have the property that (for each specific language in the formal language) if the initial wff is True, all the wffs produced from it are True.

As to turning a computer language into examples, I have the following thoughts.

Consider the C programming language.

1. Formal language: The syntax of programming languages contains the concept of various types of wffs. For example, a legal variable name is a certain type of wff. A mathematical expression is a different type. The goal of defining these types is to define a syntactically correct program. So to use the whole language as an example of a formal system, we must consider a wff to be an entire program.

2. Formal system: I don't know how to view the C programming language as a set of production rules. Within the syntax of C, there are things resembling production rules that define particular types of wffs. For example a rule could be: If <expression A> and <expression B> are each legal mathematical expressions then "<expression A> + <expression B>" is a legal mathematical expression. However, if we are using entire programs as the examples for wffs, I don't see that C has rules that define how to begin with some initial program and derive other programs.

3. Formal logic: One thought is to define a subset of C programs in which all variables must be boolean and that, in each program, all variables must be defined in terms of a set of constants A,B,C,...,Z. Constants do not change their values within a program. A constant like "A" can be assigned to be 1 in one program and 0 in a different program. The requirement is that the specific set of constants must be declared and assigned values in each program

However, that doesn't fix the problem that C is not a good example of a Formal System. So restricting it to boolean variables doesn't give us production rules.

( Discussions of mathematical logic on the forum resemble discussions about interpretations of quantum mechanics. Experts disagree. It makes me think that the rules of the game are not standardized. Maybe they aren't! )

 

[Mark44]

However, if we are using entire programs as the examples for wffs, I don't see that C has rules that define how to begin with some initial program and derive other programs.

Right, I don't see that a complete C program could be considered a WFF, at least to the extent that it could be used to derive other programs.

 

[SSequence]

I don't quite understand what your question is about. Something that seems to be (loosely) related to the question:

Suppose we fix a finite alphabet $\Sigma$ [which would usually contain all english alphabet, spaces and few more characters depending on our need]. Then considering $\Sigma^*$ [1], the set of all finite strings over $\Sigma$. Suppose we define $S$ to be the subset of $\Sigma^*$ which represents "syntactically correct" programs (for any "reasonably described" programming language [2]). That is, a (finite) string $s \in S$ iff $s$ doesn't contain any "syntax errors".

Then the first thing to note is that $S$ is decidable (obviously). But more can be said (based on what I have read). Based on what I remember reading (it has been number of years now) is that essentially $S$ can be considered as a context free language. This is probably ignoring some exceptions [e.g. variable declarations (and perhaps more?), as I re-call reading]. More concretely, I think if you search for it you would probably find the grammar for a language like Pascal etc. I definitely remember seeing it quite some time ago. Probably, simpler examples would be more illustrative though.

My guess is that what I wrote in last paragraph is very well-known. Also note that collection of CFL's is a strict subset of the collection of r.e. (recursively enumerable) or even recursive/decidable languages. Another thing to mention is that lot of other things [subsets of strings over some finite characters] like strictly formed arithmetic expressions [3] (no missing brackets) and many other things fall into category of CFLs.[1]
In the case that you might not have encountered this symbol before:
https://en.wikipedia.org/wiki/Kleene_star

[2]
The phrase "reasonably described" is meant to be informal.

[3]
What that means exactly is ambiguous (without specification). To be more concrete, if we fix an alphabet like $\{a,b,c,+,∗,(,)\}$, then the following would be examples of it:
b
(a+b)
((a+b)*c)
(((a+b)*c)+a)
etc.

 

[Stephen Tashi]

I don't quite understand what your question is about.

The question is a general question about methods of teaching. How can we use computer languages to formulate examples of topics in mathematical logic?

How can I make the question clearer?

Something that seems to be (loosely) related to the question:

Suppose we fix a finite alphabet $\Sigma$ [which would usually contain all english alphabet, spaces and few more characters depending on our need]. Then considering $\Sigma^*$ [1], the set of all finite strings over $\Sigma$. Suppose we define $S$ to be the subset of $\Sigma^*$ which represents "syntactically correct" programs (for any "reasonably described" programming language [2]). That is, a (finite) string $s \in S$ iff $s$ doesn't contain any "syntax errors".

I agree that such an example is an example of a formal language where we have chosen to call a wff a "syntactically correct" program. The viewpoint of my question is in the other direction. How do we begin with a computer language and use it as an example of a formal language. The answer appears to be equivalent - namely to say that "syntactically correct" programs are examples of wffs.

Then the first thing to note is that $S$ is decidable (obviously). But more can be said (based on what I have read).

However, my question isn't about how to discuss arbitrary examples of topics in logic. The question is how to use computer languages and modifications of them to illustrate topics in logic. So the properties of your $S$ are only relevant if we can begin by saying that some computer language or modification of it is an example of $S$ and then show how the properties of the modified compute language illustrate the properties of $S$. For example, if you are using "decidable" in the sense of recursive (e.g. https://en.wikipedia.org/wiki/Recursive_language ) we could use examples of recursiveness in the modified computer language to illustrate the concept of decidability.

 

[SSequence]

The question is a general question about methods of teaching. How can we use computer languages to formulate examples of topics in mathematical logic?

Right, this can mean a lot of things.

Few things that might be of interest (these are just possible pointers ... I don't know much about these topics). Perhaps some of these may be relevant:
------ Something like a proof assistant. Would that be related to what you are saying?

------ Something like curry-howard isomorphism. I have seen this phrase many times. Though, honestly, I don't have an idea what it really means.

------ Basic reasoning about programs in rigorous manner. I know a few basic books on this topic (but haven't read any). But nevertheless, this is an interesting topic. If you search, you would probably find some material on this topic.

For example, if you are using "decidable" in the sense of recursive (e.g. https://en.wikipedia.org/wiki/Recursive_language ) we could use examples of recursiveness in the modified computer language to illustrate the concept of decidability.

Yes, I meant in that sense.

It is not difficult to use restrictive languages exclusively to illustrate a number of basic ideas (without any skipping) such as encoding (similar or same to godel encoding), simulation/universal program etc. But normally (for theory), beyond a certain point informal sketches seem to be quicker/easier.

But I don't know if this is along the lines of what you are seeking.

 

[Klystron]

For purposes of teaching formal logic consider limiting the C programming language to a minimal form that fulfills your didactic requirements while eliminating exceptions and possible contradictions. Whether this simplifed C language subset remains a realistic programming language might not matter depending on your teaching goals.

Ages ago I helped reduce a standard C language module to a significantly smaller version to meet size and run-time constraints in a dedicated environment. One modification I remember was to reduce allowed conditional and iterative (looping) constructs to the bare minimum along with limited included libraries. Data types were restricted to those required by the project eliminating, for examples, floating point and character string types.

We provided a programming manual including methods to reduce standard C routines to C-simple and to compile in this limited environment. To quote Joan Baez, "Take what you need and leave the rest.".

 

[SSequence]

One other example of using a more specific computation model (for a specific theoretical purpose) seems to be RAM model. I had never heard of it until very recently. It seems that it is meant to help formalize some notions w.r.t. time complexity (in cases where a finer distinction may be required).

 

[Paul Colby]

I've spent some time writing language front-ends using lex and yacc. Lex defines the tokens i.e. "int" is a keyword assigned an integer value and so on. The yacc input is a system of syntactic productions forming an LALR language in terms of terminals and and tokens. Each production has an action which one might view as wff rewrite?

 

[Stephen Tashi]

Each production has an action which one might view as wff rewrite?

That's a good idea. Can a parser for a computer language be regarded as defining the derrivation rules for a formal system?

Compared to a system of derrivation rules, I think a parser works in reverse. Instead of derriving new wffs from given wffs, it takes a given string (an attempted program) and tries to find a way that it can be analyzed as the result of applying production rules to a set of wffs. It must discover the wffs that are inputs.

For example, to determine "A+B" is a valid expression, it must discover that the inputs "A","B" can be used to form "A + B" according to the rule: Input: <variable 1>, <variable 2> Output: <variable 1> + <variable 2>.

I can think of a parser as implicitly defining a set of derrivation rules. As a teaching example, this still leaves the problem that a wff in a computer language must be a complete program. A parser does not analyze a complete program as being composed of other programs.

There might be a computer language (or a way of regarding a language) where wff can refer to some set of things that includes programs as a proper subset. Perhaps languages that have the philosophy "Everything is an object" can be regarded that way.

 

[Stephen Tashi]

One other example of using a more specific computation model (for a specific theoretical purpose) seems to be RAM model.

I read the brief descripton at https://www8.cs.umu.se/kurser/TDBA77/VT06/algorithms/BOOK/BOOK/NODE12.HTM. I don't know how to fit that into an example for a formal system.

Assuming we have a formal language of certain type, where a wff must be an algorithm, the RAM model assigns a number to such an wff. So it's an example of assigning numbers to wffs - not the way Godel did, but an illustration that the general idea is not crazy.

 

[SSequence]

I didn't understand your question so I thought you were asking for a computation language conceived specifically for any theoretical purpose (generic).

Given what you wrote in last post, I can only add two points:
(a) The type-0 grammars (there are few names for these or equally powerful grammars) can generate any recursively enumerable language. But I suppose that you might be looking for something more specific.

(b) Lambda calculus would be related to what you are asking, I think. I am not familiar with it well-enough though.

Here are few links I found with a quick search (that seem to be of some relevance to what you are saying in last post):
link1
link2

 

[Stephen Tashi]

(b) Lambda calculus would be related to what you are asking, I think. I am not familiar with it well-enough though.

link1

l don't see any relation to the question in my OP, but it's mind-expanding to read about a "non-extensional" approach to describing functions.

 

[Paul Colby]

Can a parser for a computer language be regarded as defining the derrivation rules for a formal system?

My understanding is a properly formed BNF system defines a computer language while a parser validates given inputs wrt the defined system. Can the valid set of wffs be considered such? If the rules are an LALR parsable set of strings then isn't the answer yes?

 

[Jarvis323]

Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?

Have you heard of Prolog?

Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily as a declarative programming language: the program logic is expressed in terms of relations, represented as facts and rules. A computation is initiated by running a query over these relations.

https://en.wikipedia.org/wiki/Prolog

 

[bhobba]

Can a modern computer language implement a (conceptual) Turing Machine? Can Turing Machines be used to deduce propositions in a formal logical system (eg the predicate calculus)?

Thanks
Bill

 

[Jarvis323]

Can a modern computer language implement a (conceptual) Turing Machine?

Yes. It doesn't take much for a language to be Turing complete.

https://en.m.wikipedia.org/wiki/Turing_completeness

Can Turing Machines be used to deduce propositions in a formal logical system (eg the predicate calculus)?

Yes, but Turing machines are not a practical choice.

https://en.m.wikipedia.org/wiki/Automated_theorem_proving

 

[bhobba]

Yes, but Turing machines are not a practical choice.
https://en.m.wikipedia.org/wiki/Automated_theorem_proving

I thought we were talking about matters of principle.

Thanks
Bill

 

[Stephen Tashi]

I think Turing introduced his machines to go beyond formal languages, formal systems, and formal logic and proceed to a model that gives us computers. However, I haven't seen Turing machines presented by giving a formal formal system or formal logic and then saying "here's the assumptions we add to get a Turing machine". If that were the case, a Turing machine would be an example of those formal structures.

The usual presentation of a Turing machine begins informally (by the standards of mathematical logic) and speaks of a "tape" that contains symbols and a machine that can move along and write and erase on that tape. Although the motivation may be to extend formal systems, formal logic etc, the presentation sidesteps any mention of these topics. So there is no obvious way to see that Turing machine is a specific example of any of them.

As far as the question in the OP goes, it makes sense to consider Turing machines since the OP asks about computer languages and a Turing machine is a model of a computer. However, just as in the case of a specific computer language, we need some way to fix-up a Turing machine or look at it in special way to make it into a clear example.

 

[Stephen Tashi]

Have you heard of Prolog?
https://en.wikipedia.org/wiki/Prolog

Does that imply Prolog an obvious answer to the OP? - or is this a suggestion for further investigation?

Yes, I've heard of prolog and the concept of declarative programming languages, but I haven't used them. Can Prolog be used as an example of a formal language, formal system, or formal logic? How would that be done? The link say Prolog "has its roots" in first-order logic. But is Prolog or some aspect of it identical to a first-order logic?

 

[SSequence]

Can a modern computer language implement a (conceptual) Turing Machine? Can Turing Machines be used to deduce propositions in a formal logical system (eg the predicate calculus)?

Thanks
Bill

It would depend on specific case. But under "reasonable" circumstances, the answer is "generally" (but not always) yes [1]. Also, I am assuming that you are asking in principle. In practice, the time complexity of enumerating all proofs of certain length (provable in a given system) would be quite high practically [on the very least, no general efficient way is known I think].

For example, the theorems of PA are r.e. (recursively enumerable). Similar is the case of set theory (as formalized in ZFC as an example). The reason for theorems being r.e. here is a bit more complicated and I don't know it well enough [2]. Same is true for a lot of theories that are weaker than set theory (for example, (i) the five systems of reverse math (ii) likely some weaker fragments of set theory too ... and what not).

[1] Taking the assumption of infinite memory available as given (I am guessing this is implicitly assumed or allowed?).

[2] Generically, in first-order-logic, there seem to few lemmas/theorems which help guarantee the recursive enumerability of theorems (if certain given conditions/pre-requisites are satisfied).

Although the motivation may be to extend formal systems, formal logic etc, the presentation sidesteps any mention of these topics. So there is no obvious way to see that Turing machine is a specific example of any of them.

This is true but there are still lot of interesting aspects that logic can provide.

As one example (among others), description of more complicated sets (than decidable) often seem to have multiple equivalent notions [including intrinsically logical descriptions] associated with them. Actually, often there seem to be two or more complementing descriptions!

Lets think about computable sets in following two ways (admittedly quite coarsely):
(1) computability (as in by a program)
(2) general recursive function (primitive recursive functions with minimalization operator)

But mathematics is not only about computable sets or c.e. sets. Many more complicated sets (even ones whose elements are only natural numbers) seem to have a number of intrinsic and equivalent descriptions: recursion based [suitable generalisation of primitive recursive functions], logic based [first-order-definitions over a structure] and infinite time computation based which complement each other. In some specific cases (specific collections of sets), some notions don't directly fall into category of either of above.

Anyway, this isn't directly related to the question, but I felt it is interesting to point this out (since this point came up).

 

[Stephen Tashi]

My understanding is a properly formed BNF system defines a computer language while a parser validates given inputs wrt the defined system.

I like the idea of focusing on a Backus-Naur specification of language instead of focusing on a parser of those specifications. How can I relate BNF specifications to the mathematical idea of formal language- as opposed to the computer science idea of a computer language?

 

[Paul Colby]

How can I relate BNF specifications to the mathematical idea of formal language- as opposed to the computer science idea of a computer language?

I haven't seen the definition of a formal language you're using. If I've missed it I apologize.
Just guessing I assume a "formal language" is a set of symbols with a set of rules to form valid strings of symbols or sentences. It's likely I'm missing something.

 

[Jarvis323]

Does that imply Prolog an obvious answer to the OP? - or is this a suggestion for further investigation?

Yes, I've heard of prolog and the concept of declarative programming languages, but I haven't used them. Can Prolog be used as an example of a formal language, formal system, or formal logic? How would that be done? The link say Prolog "has its roots" in first-order logic. But is Prolog or some aspect of it identical to a first-order logic?

I wasn't sure exactly what the goal is, but thought Prolog seemed to be the closest language I know that fits. So I guess this is a suggestion for further investigation.

Maybe this example can help.
https://www.cpp.edu/~jrfisher/www/prolog_tutorial/logic_topics/normal_forms/normal_form.html

 

[Hornbein]

Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?

A computer language is not a clear example of a formal language, a formal system, or a formal logic. Can we modify the rules for a computer language to create clear examples?

My non-authoritative classification of topics in mathematical logc is:

1. Formal languages. A formal language is defined by a set of rules that define which strings of symbols are "well formed formulas" (wffs). A wff has no semantic interpretation other than being syntactically correct according the rules of the formal language. Within the context of a formal language, a wff does not represent a statement that is True or False or a mathematical function.

2. Formal systems: A formal system is a formal language plus a set of "production rules". If we write down an initial wff, the production rules describe permissible operations for "deriving" other wffs from the initial wff. Within the context of a formal system, there is no interpretation that wffs involved are True (or False), so the "derivations" are not mathematical proofs that deduce True statements from some initial statement that is assumed to be True.

3. Formal logics: A consistent formal two-valued logic is a formal system with additional requirements. The wffs must each be assigned exactly one of two possible values, either True or False. (As a matter of vocabulary, in a specific formal language, the wffs are assigned specific values. Speaking of "formal language" as a generality, it is a set of specific formal languages. The value assigned to a wff may vary between two different laguages in that set.) The production rules must have the property that (for each specific language in the formal language) if the initial wff is True, all the wffs produced from it are True.

As to turning a computer language into examples, I have the following thoughts.

Consider the C programming language.

1. Formal language: The syntax of programming languages contains the concept of various types of wffs. For example, a legal variable name is a certain type of wff. A mathematical expression is a different type. The goal of defining these types is to define a syntactically correct program. So to use the whole language as an example of a formal system, we must consider a wff to be an entire program.

2. Formal system: I don't know how to view the C programming language as a set of production rules. Within the syntax of C, there are things resembling production rules that define particular types of wffs. For example a rule could be: If <expression A> and <expression B> are each legal mathematical expressions then "<expression A> + <expression B>" is a legal mathematical expression. However, if we are using entire programs as the examples for wffs, I don't see that C has rules that define how to begin with some initial program and derive other programs.

3. Formal logic: One thought is to define a subset of C programs in which all variables must be boolean and that, in each program, all variables must be defined in terms of a set of constants A,B,C,...,Z. Constants do not change their values within a program. A constant like "A" can be assigned to be 1 in one program and 0 in a different program. The requirement is that the specific set of constants must be declared and assigned values in each program

However, that doesn't fix the problem that C is not a good example of a Formal System. So restricting it to boolean variables doesn't give us production rules.

( Discussions of mathematical logic on the forum resemble discussions about interpretations of quantum mechanics. Experts disagree. It makes me think that the rules of the game are not standardized. Maybe they aren't! )

There's the lambda calculus, a formal language that can in theory be used to compute. There are the various styles of Turing Machine. These were formalisms used in proofs of what is and isn't computable.

There are also non-procedural languages dedicated to solving problems in logic. You tell the system what the problem is and it computes the solutions. Prolog! That's the name. Surely it is obsolete by now.

There's Backus' FP, a functional programming language. FP has no variables and actually runs on a computer. Or at least did at one time.

My thinking is that the big difference between these and an actual programming language is that there are NO variables. Once something is given a value it never changes its value. I programmed this way insofar as is practical and found it very helpful for writing reliable programs. The only essential reason to have variables is to save memory. Theoreticians don't need to worry about that.

 

[Stephen Tashi]

I haven't seen the definition of a formal language you're using. If I've missed it I apologize.
Just guessing I assume a "formal language" is a set of symbols with a set of rules to form valid strings of symbols or sentences. It's likely I'm missing something.

We need expert commentary on whether my definition of formal language is correct!. In my definition, a formal language agrees with what you said. The rules for wffs aren't necessarily stated as rules for deriving new wffs from given wffs. When we have rules for derriving new wffs from given wffs, I call that case a "formal system".

 

[Paul Colby]

Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?

I don't see that C has rules that define how to begin with some initial program and derive other programs.

What about code optimizers? Granted, these are typically applied after the code has been translated into some intermediate form. For example changing, "a = b + c + e;", into a series of machine op codes acting on selected registers. Basically, a different wff in a different language. During this process the optimizer may note that a previously computed sum, say c + e, is used in 20 other expressions and decides reusing this computed value is cheaper. It then changes the code using rules that guarantee the result of the new code doesn't change.

 

[Stephen Tashi]

What about code optimizers?

That is a good idea!

 

[SSequence]

When we have rules for derriving new wffs from given wffs, I call that case a "formal system".

What about these:
https://en.wikipedia.org/wiki/Unrestricted_grammar

I already mentioned them in post#11. Wouldn't these closely correspond to what you are calling formal system.P.S.
I have also been a bit vague about the term "formal system" in the past. Normally when I have used the term in the past I have meant it in the following sense: a program which prints a recursively enumerable subset (say S) of following set:
0, 0', 1, 1', 2,', 3, 3', 4, 4', 5, 5', 6, 6', 7, 7', 8, 8', 9, 9', 10, 10',......

Each number x in the set {0,1,2,3,4,5,6,...} is supposed to correspond to some question/statement [from a selected/agreed domain of problems]. The number x' is supposed to correspond to negation of the statement (which corresponds to number x). So when x∈S, it means that S proves the sentence corresponding to x. When x'∈S, it means S disproves the sentence corresponding to x (i.e. proves sentence corresponding to x'). When x∉S, it means the sentence corresponding to x is independent of S (i.e. S neither proves nor disproves it).In some sense, it would make sense to call the set S (along with the statements encoded) as a "logical theory". But that would be an overloading of similar terms (and cause some confusion).

Nevertheless, while this kind of representation has many limitations [some which I understand, and many which I don't], it is reasonably useful an initial guide (and sometimes later too).

It does help understand some aspects like consistency and numbering of sentences. [it also helps a bit in seeing (the outline) how halting problem would imply the first incompleteness theorem (soundness version) ... though the specific corollary of incompleteness theorem is different]

 

[Stephen Tashi]

What about these:
https://en.wikipedia.org/wiki/Unrestricted_grammar

I already mentioned them in post#11. Wouldn't these closely correspond to what you are calling formal system.

I'll have to think about that. But this widens the topic. My main question is how to form examples in mathematical logic based on things familiar to people who program computers, but have not necessarily taken courses in Computer Science.

People who take theoretical courses in computer science know about Turing machines and other abstract structures. That type of person can appreciate an example where a Turing machine or an abstract model of computation is involved.

 

[SSequence]

My main question is how to form examples in mathematical logic based on things familiar to people who program computers, but have not necessarily taken courses in Computer Science.

As I mentioned in post#5, just having some familiarity with notion of a "program" is enough to understand elementary (but also important) theorems in recursion theory.

I don't know whether this helps or not, but here is an implementation of a universal program I wrote four years ago or so (the upload date is about two years later). Maybe someone would find it useful. For example, I have seen some discussions whether a full implementation should be used in a basic course or not. I don't know about that. However one thing to mention is that even though it looks quite long, but it didn't take me more than two weeks or so to write all of this (because if you read it carefully, you will notice that it is simple).

Now it doesn't seem to me that this teaches any "real world programming" of course [or at least, I am no good at it in any case], but that wouldn't be the purpose either. Now one might say, why not have lists already included in basic constructs? Well it is arguable of course.

Please note that there are probably a few (minor quite likely) mistakes in the detailed implementation. I did check and correct a lot of mistakes (a few still remain I think), but I haven't taken a look at it for few years now.

description
implementation

==============================

The computational model for which universal program is written is defined by following commands:
temporary variables: t1,t2,t3,t4,...
input variables: x1,x2,x3,x4,...
output variable: y

commands (v,w below are variables):
v=0
v=v+1
while(v!=w)
End

!= simply means "not equal". End is just a replacement for (ending) brackets. Also = means assignment (":=" that is).

==============================

Now the program model above is sufficiently strong to calculate any partial computable k-ary function $\mathbb{N}^k \rightarrow \mathbb{N}$. The reason why further features can be simulated in this basic program is simply due to variable re-naming [along with an understanding what segment of commands will be enough to replace every occurrence of some new construct ... I went through it quite briefly for most additional constructs].

There are some conventions I used implicitly (without explaining). Every variable is assumed to be local to the specific function it used in by default (so there is no possibility of a variable referring to anything else outside the specific function it is used in). Initial declaration for variables are skipped i.e. not required/allowed. Default initial values for variables are 0. The naming conventions for input and output variables remain the same for every function [x,x1,x2,... etc. for input and y for output]. Also, in the "description" document (in A3), I used the phrase "call hierarchy". But a more suitable description one would be "call dependence in text of program".

The universal program was written in a computation model with facility of sub-routines/functions added (along with conditionals and one or two more additions) [the constructs in A7 aren't used in the implementation]. One difference is that instead of prime-factorization for encoding, I used repeated applications of an "encode" function [of course this is also a well-known alternative method].

For example, the encode function (of two variables) can be visualized as follows:

90	91	92	93	94	95	96	97	98	99
72	73	74	75	76	77	78	79	80	89
56	57	58	59	60	61	62	63	71	88
42	43	44	45	46	47	48	55	70	87
30	31	32	33	34	35	41	54	69	86
20	21	22	23	24	29	40	53	68	85
12	13	14	15	19	28	49	52	67	84
6	7	8	11	18	27	38	51	66	83
2	3	5	10	17	26	37	50	65	82
0	1	4	9	16	25	36	49	64	81

e.g. we have:
encode(0,0)=0, first(0)=0, second(0)=0
encode(1,0)=1, first(1)=1, second(1)=0
encode(0,1)=2, first(2)=0, second(2)=1
encode(1,1)=3, first(3)=1, second(3)=1
encode(2,4)=22, first(22)=2, second(22)=4
and so on...
Note:
If we choose to, we can also work with strings (with the character set being the same as one in which we write our programs). Then if we think of an arbitrary program as calculating a function $S^n \rightarrow S$ [$S$ is set of all finite strings over the given characters and $n$ is a positive natural number] then a universal program for program computing functions of one variable has a very natural definition.

The universal program (from $S^2$ to $S$) simply takes the text of any program computing a unary function (from $S$ to $S$) along with the input string and simulates it exactly. So it halts iff the original program halts on same input and gives the same output upon halting.

It could also work in the same way as above (as described for natural numbers). We first define a very basic model with few commands. And then the universal program can be built using a computational model with few basic features added (for ease and to avoid repetition) on top of the primitive one.

 

[sbrothy]

Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?

I more than suspect that I'm way out of my league here, but did you consider functional languages like for instance Miranda? I'd expect such languages to convey mathematics and logic better than a messy "structured" language like C.
Regards.

 

[Stephen Tashi]

I don't know whether this helps or not, but here is an implementation of a universal program

I'm not familiar with the terminology "universal program". Does that mean an implementation of a "universal Turing machine"?

 

[SSequence]

Yes, pretty much. So, for example, I considered the universal program for the "primitive model" I described (with four basic commands) [described in a model where few extra things like macros/conditionals were added for better readability and to avoid too much repetition].

 

[strangerep]

Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?

A computer language is not a clear example of a formal language, a formal system, or a formal logic. Can we modify the rules for a computer language to create clear examples?

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.

 

[.Scott]

Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?

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".

A computer language is not a clear example of a formal language, a formal system, or a formal logic. Can we modify the rules for a computer language to create clear examples?

My non-authoritative classification of topics in mathematical logic is:

1. Formal languages. A formal language is defined by a set of rules that define which strings of symbols are "well formed formulas" (wffs). A wff has no semantic interpretation other than being syntactically correct according the rules of the formal language. Within the context of a formal language, a wff does not represent a statement that is True or False or a mathematical function.

It seems to me that by this definition, computer programming languages are "wffs". 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.

2. Formal systems: A formal system is a formal language plus a set of "production rules". If we write down an initial wff, the production rules describe permissible operations for "deriving" other wffs from the initial wff. Within the context of a formal system, there is no interpretation that wffs involved are True (or False), so the "derivations" are not mathematical proofs that deduce True statements from some initial statement that is assumed to be True.

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".
As I said before, computer programs are not declarative - they are imperative. When applied to a machine, they cause that machine to yield a result. Starting with a specific computer program (a wff), we can apply specific rules to transform that program into equivalent programs (other wff symbol sets) that will yield those same results. So given that a specific wff is "true", it can be transformed into other wffs that are also "true".

In fact, this operation is routinely performed on computer programs. If you start with a C program and compile it, several operations of this type are performed. First, the programming logic is parsed, categorically tabulated, and analyzed - a process which involves a major change in syntax and potentially changes to the wff imperatives themselves. Then optimizations are applied. This is a very explicit process of transforming the wff into a different but equivalent set of instructions - so a different wff has been formed with rules that assure that this new wff is just as "true" as the original. This optimized code is then provided in a variety of syntactical renditions - a buildable object module, an executable, and perhaps marco-assembly source.

So I would suggest that a computer language - especially in conjunction with functional compilers - could be considered a "Formal System" by your definition.

3. Formal logics: A consistent formal two-valued logic is a formal system with additional requirements. The wffs must each be assigned exactly one of two possible values, either True or False. (As a matter of vocabulary, in a specific formal language, the wffs are assigned specific values. Speaking of "formal language" as a generality, it is a set of specific formal languages. The value assigned to a wff may vary between two different languages in that set.) The production rules must have the property that (for each specific language in the formal language) if the initial wff is True, all the wffs produced from it are True.

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".

However, that doesn't fix the problem that C is not a good example of a Formal System. So restricting it to boolean variables doesn't give us production rules.

I agree. C is not a Formal System. It is only a syntax.