Parentheses Are Just Typechecking(adam.nels.onl)
adam.nels.onl
Parentheses Are Just Typechecking
https://adam.nels.onl/blog/parentheses-are-just-typechecking/
46 comments
> I think I’ve heard that the APL semantics is commonly described right to left so might be related?
Not particularly related. It's just that every function is either monadic (operand on the right) or dyadic (infix). That makes it a case of not needing to explicitly specify where the function arguments start and end, still without using a stack; it is purely syntactic, and obvious (although you do need context to parse anything that uses user-defined things). Parentheses are still needed for the left operand of a dyadic function if it is to take an expression more complicated than a plain array.
If you had functions of higher arity, then it would become necessary to add parens, delimiters, or a stack.
Not particularly related. It's just that every function is either monadic (operand on the right) or dyadic (infix). That makes it a case of not needing to explicitly specify where the function arguments start and end, still without using a stack; it is purely syntactic, and obvious (although you do need context to parse anything that uses user-defined things). Parentheses are still needed for the left operand of a dyadic function if it is to take an expression more complicated than a plain array.
If you had functions of higher arity, then it would become necessary to add parens, delimiters, or a stack.
I don't have anything substantive to add, just a nitpick: wouldn't unary be a better term than monadic here? In functional programming, monadic function is generally used to mean, well, a monadic function.
Why is is better? It just seems different.
APL's usage of monad predates its use in conjunction with modern functional programming languages, by the way. It goes back to the 60s, and there are plenty of books and papers where these terms are used that way.
https://en.wikipedia.org/wiki/Monad_(functional_programming)...
I can't say I care too much which terms people use, but in context of APL, I prefer the terms that were used by Iverson and have been in print for more than half a century.
APL's usage of monad predates its use in conjunction with modern functional programming languages, by the way. It goes back to the 60s, and there are plenty of books and papers where these terms are used that way.
https://en.wikipedia.org/wiki/Monad_(functional_programming)...
I can't say I care too much which terms people use, but in context of APL, I prefer the terms that were used by Iverson and have been in print for more than half a century.
It is confusing, nevertheless, and perhaps merits clarification like any uncommon bit of language does. (Also like any uncommon bit of language, it may seem perfectly normal until people outside your usual circle point out they don’t understand you.)
It would be interesting to track down where these terms came from. The typed functional programming usage of the term monad, being identical to the current mathematical usage, apparently comes[1] from Mac Lane’s classic Categories for the working mathematician (1971) and seems to be motivated by the preexisting term monoid (which I dislike, so that’s a bit disappointing). The use of monadic, dyadic, etc. for relations and operations of (what is now usually called) particular arity is, as far as I can tell, mostly obsolete in mathematics post 1960 or so except for the occasional use by logicians (particularly of a philosophical bent). I’ve found it[2] as far back as Russell and Whitehead’s Principia mathematica (1910–13), but don’t know where they got it from. Still, that explains the use in logic (not that it means it’s a good idea: most of notation in Russell and Whitehead[3] is now spectacularly obscure, and parts of it were obscure even at the time).
[1]: https://english.stackexchange.com/a/30661
[2]: https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Pri...
[3]: https://plato.stanford.edu/entries/pm-notation/
It would be interesting to track down where these terms came from. The typed functional programming usage of the term monad, being identical to the current mathematical usage, apparently comes[1] from Mac Lane’s classic Categories for the working mathematician (1971) and seems to be motivated by the preexisting term monoid (which I dislike, so that’s a bit disappointing). The use of monadic, dyadic, etc. for relations and operations of (what is now usually called) particular arity is, as far as I can tell, mostly obsolete in mathematics post 1960 or so except for the occasional use by logicians (particularly of a philosophical bent). I’ve found it[2] as far back as Russell and Whitehead’s Principia mathematica (1910–13), but don’t know where they got it from. Still, that explains the use in logic (not that it means it’s a good idea: most of notation in Russell and Whitehead[3] is now spectacularly obscure, and parts of it were obscure even at the time).
[1]: https://english.stackexchange.com/a/30661
[2]: https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Pri...
[3]: https://plato.stanford.edu/entries/pm-notation/
> Lisp only needs parentheses because its operators have variable arity, that’s about as deep as the “type system” goes.
List needs parentheses because its parser does not depend on knowledge of operator's arity, it just parses generic abstract syntax tree.
Arity is property of functions, not expressions, so you would need static type system to assigning arity-types to expressions.
Also, you would still need parentheses to express structural data, where no operator arity is relevant.
List needs parentheses because its parser does not depend on knowledge of operator's arity, it just parses generic abstract syntax tree.
Arity is property of functions, not expressions, so you would need static type system to assigning arity-types to expressions.
Also, you would still need parentheses to express structural data, where no operator arity is relevant.
About this last point from the article:
> Why have I never seen...
> ...a Lisp that can drop nested parentheses when the meaning is clear from context?
I once wrote a Lisp that dropped closing parentheses for one and zero-argument functions. This was done by introducing simple syntax sugar:
For zero-arg functions the syntax was:
The `f[x]` syntax by itself also has the advantage of removing nesting for curried functions, i.e `(((f x) y) z)` becomes `f[x][y][z]`. In fact in this syntax two consecutive brackets `[[` were illegal.
So it both eliminated consecutive opening parens and substantially reduced consecutive closing parens. This was an effort to fix the major readability problems for people coming into Lisp.
For the curious, both the syntax and the language overall is described here (my master's thesis): https://djedr.github.io/masters_thesis.pdf (Chapter 2 in particular).
> Why have I never seen...
> ...a Lisp that can drop nested parentheses when the meaning is clear from context?
I once wrote a Lisp that dropped closing parentheses for one and zero-argument functions. This was done by introducing simple syntax sugar:
foo | bar
foo[bar]
(foo bar)
For zero-arg functions the syntax was:
foo!
foo[]
(foo)
The `f[x]` syntax by itself also has the advantage of removing nesting for curried functions, i.e `(((f x) y) z)` becomes `f[x][y][z]`. In fact in this syntax two consecutive brackets `[[` were illegal.
So it both eliminated consecutive opening parens and substantially reduced consecutive closing parens. This was an effort to fix the major readability problems for people coming into Lisp.
For the curious, both the syntax and the language overall is described here (my master's thesis): https://djedr.github.io/masters_thesis.pdf (Chapter 2 in particular).
Interesting ideas! Would it make sense to "sugarify" currying even further? For instance, `f[x][y][z]` could become something like `f→[x y z]`.
> Interesting ideas!
:-)
> Would it make sense to "sugarify" currying even further? For instance, `f[x][y][z]` could become something like `f→[x y z]`.
Technically it could be done. Does it make sense? Depends on what are you trying to achieve. Personally I tend toward an _extremely_ minimalist approach and the complexity of that would not be worth it for me. In fact today I'd question the addition of `|` and `!` as too specific.
The syntax you proposed does save a few brackets, but the functionality could also be achieved with a specialized function:
:-)
> Would it make sense to "sugarify" currying even further? For instance, `f[x][y][z]` could become something like `f→[x y z]`.
Technically it could be done. Does it make sense? Depends on what are you trying to achieve. Personally I tend toward an _extremely_ minimalist approach and the complexity of that would not be worth it for me. In fact today I'd question the addition of `|` and `!` as too specific.
The syntax you proposed does save a few brackets, but the functionality could also be achieved with a specialized function:
→[f x y z]
Interesting. Did you encounter any trade-offs or downsides in choosing this over a traditional s-expression style lisp? I am curious why this hasn’t been seen in a mainstream lisp before.
> Did you encounter any trade-offs or downsides in choosing this over a traditional s-expression style lisp?
No downsides for `f[x]` instead of `(f x)`. It really does fix the problem of overnesting without any significant trade-off that I can see. Net value of this improvement is the highest.
For `foo | bar` instead of `foo[bar]` I see some downsides from a minimalist point of view. Slight complexity is added to the parser. The `|` is right-associative which has to be kept in mind when reading the code:
> I am curious why this hasn’t been seen in a mainstream lisp before.
Not sure. Certainly I have not seen this exact improvement anywhere before or since. I think it's mostly a matter of tradition. Somehow S-expressions stuck as the defining feature of Lisp and a fundamental ALGOL-like change like that would be too much to stay in the family, certainly not in the mainstream.
Indeed, as @wgoodall01 mentions there is the Wolfram Language based around something similar to M-expressions, but it is neither mainstream nor (classified as) a Lisp. The syntax is also more complex overall.
There is also Rebol[0] and its variants, but it is also not mainstream and diverges from Lisp substantially.
Nothing else of note comes to mind.
I think John McCarthy had the right idea with M-expressions. Perhaps the definition should have been a bit more minimal back then and today we would have a major Lisp with this sort of syntax.
[0] https://en.wikipedia.org/wiki/Rebol
No downsides for `f[x]` instead of `(f x)`. It really does fix the problem of overnesting without any significant trade-off that I can see. Net value of this improvement is the highest.
For `foo | bar` instead of `foo[bar]` I see some downsides from a minimalist point of view. Slight complexity is added to the parser. The `|` is right-associative which has to be kept in mind when reading the code:
foo | bar | baz
foo[bar[baz]]
> I am curious why this hasn’t been seen in a mainstream lisp before.
Not sure. Certainly I have not seen this exact improvement anywhere before or since. I think it's mostly a matter of tradition. Somehow S-expressions stuck as the defining feature of Lisp and a fundamental ALGOL-like change like that would be too much to stay in the family, certainly not in the mainstream.
Indeed, as @wgoodall01 mentions there is the Wolfram Language based around something similar to M-expressions, but it is neither mainstream nor (classified as) a Lisp. The syntax is also more complex overall.
There is also Rebol[0] and its variants, but it is also not mainstream and diverges from Lisp substantially.
Nothing else of note comes to mind.
I think John McCarthy had the right idea with M-expressions. Perhaps the definition should have been a bit more minimal back then and today we would have a major Lisp with this sort of syntax.
[0] https://en.wikipedia.org/wiki/Rebol
This has been seen in a mainstream lisp before! (sort of)
Wolfram Language uses almost this exact syntax—function application looks like f[x,y], but in all other respects, it works like a LISP would.
Wolfram Language uses almost this exact syntax—function application looks like f[x,y], but in all other respects, it works like a LISP would.
> Why have I never seen...
Simply put, limited history/experience. That's not a bad thing. Rediscovery is good, and often coming at things new, with ideas not weighed down by past thinking can allow for breakthroughs.
> ...a stack language that evaluates right-to-left?
APL, J, K, etc.
> ...a stack language that allows parentheses as a sanity check?
Factor. Not really parentheses, but there are stack languages that use the stack notation ( x -- x x ) to verify stack balance and some that even use the stack notation to validate types. Types and stack balance can even be inferred.
> ...a Lisp that can drop nested parentheses when the meaning is clear from context?
REBOL and now Red, et al. But, as @mananaysiempre stated in another comment, the primary use of parentheses in Lisp is due to functions that allow for variable arity.
Simply put, limited history/experience. That's not a bad thing. Rediscovery is good, and often coming at things new, with ideas not weighed down by past thinking can allow for breakthroughs.
> ...a stack language that evaluates right-to-left?
APL, J, K, etc.
> ...a stack language that allows parentheses as a sanity check?
Factor. Not really parentheses, but there are stack languages that use the stack notation ( x -- x x ) to verify stack balance and some that even use the stack notation to validate types. Types and stack balance can even be inferred.
> ...a Lisp that can drop nested parentheses when the meaning is clear from context?
REBOL and now Red, et al. But, as @mananaysiempre stated in another comment, the primary use of parentheses in Lisp is due to functions that allow for variable arity.
Logo is close to "a lisp with no parentheses", and it also doesn't have any special forms. You can have parens, but they are optional. Compare:
item random size :list :list
(item (random (size :list)) :list)
I'm not familiar with Logo. How are you supposed to know where parentheses are implicitly opened and closed?
If you know the valence (argument count) of a given word, you know how many following expressions to read, recursively. Parens in s-exprs simply make the valence an explicit syntactic feature of each evaluation. Some dialects of Logo have procedures which permit a variable number of arguments, and in those cases you might be required to include parens.
In the places where you need a list (or block), square brackets are used. for example, a classic turtle-graphics phrase:
As for how you parse Logo expressions into a tree form, the strategy I've taken in my interpreters is "don't". Parse everything into flat lists of words, and then at interpretation time peel off words one at a time, measure their valence, and recur.
In the places where you need a list (or block), square brackets are used. for example, a classic turtle-graphics phrase:
repeat 4 [forward 10 right 90]
As for how you parse Logo expressions into a tree form, the strategy I've taken in my interpreters is "don't". Parse everything into flat lists of words, and then at interpretation time peel off words one at a time, measure their valence, and recur.
Oh, that makes sense. Your explanation made me realize I was assuming a few things about the language that apparently aren't true. Thank you.
>Then an expression like (Foo bar (Baz qux)) could be rewritten as (Foo bar Baz qux)
Until you want to pass Baz as an argument of Foo. I understand the value of sugar in a language, but I also think that sometimes you don't need more than one way to skin a cat.
Until you want to pass Baz as an argument of Foo. I understand the value of sugar in a language, but I also think that sometimes you don't need more than one way to skin a cat.
I feel like I may have misunderstood the point of the article because this seems like an obvious explanation to me. A pair of parentheses in Scheme tells the interpreter that it needs to open a new environment, evaluate the expression inside, and return the value. If there aren't parentheses, the evaluator will look up the value of the symbol in the current environment. These are very different things and, it seems to me, mixing them would make it unnecessarily difficult to pass named functions as arguments.
For example, (map car '((a b) (c d) (e f))) evaluates to '(a c e), while (map (car '((a b) (c d) (e f)))) yields an error.
In this case, I don't want my interpreter to 'helpfully' add the parentheses in around car when it see it's a one-argument function that expects a list and the following expression is a list. And even if the interpreter is able to disambiguate it and thus avoid introducing errors, a huge benefit of the parentheses in Scheme is how easy is (as a human) to see the structure of your code at a glance. In my mind, introducing ambiguity here would only serve to undermine this while bring minimal benefit.
For example, (map car '((a b) (c d) (e f))) evaluates to '(a c e), while (map (car '((a b) (c d) (e f)))) yields an error.
In this case, I don't want my interpreter to 'helpfully' add the parentheses in around car when it see it's a one-argument function that expects a list and the following expression is a list. And even if the interpreter is able to disambiguate it and thus avoid introducing errors, a huge benefit of the parentheses in Scheme is how easy is (as a human) to see the structure of your code at a glance. In my mind, introducing ambiguity here would only serve to undermine this while bring minimal benefit.
I go further, parenthesis are really just functions (in the mathematical sense); so all of first order logic comes down to making functions into variables (a la `y=f(...)`).
It's crucial to not mix together these variable-functions and regular variables. The real cool thing is having two levels of "variableness" without ever acknowledging as such. That way you mix both levels of variability without ever blending them together. Similarly you also get to mix together a function description and its result; but like before, the mathematical formalisms will prevent any blending of both.
in any case, I still some questions about quantifiers...
It's crucial to not mix together these variable-functions and regular variables. The real cool thing is having two levels of "variableness" without ever acknowledging as such. That way you mix both levels of variability without ever blending them together. Similarly you also get to mix together a function description and its result; but like before, the mathematical formalisms will prevent any blending of both.
in any case, I still some questions about quantifiers...
>> I go further, parenthesis are really just functions (in the mathematical
sense); so all of first order logic comes down to making functions into
variables (a la `y=f(...)`).
I don't get what you mean. Here's a quick reminder of first-order logic (FOL) syntax. In FOL, an atomic formula or atom is a predicate symbol followed by n ≥ 0 comma-separated terms in parentheses, where n is the arity of the predicate, terms are variables or functions, variables are quantified over functions and constants, a function is a function symbol followed by m ≥ 0 comma-separated terms in parentheses where m is the arity of the function and a constant is a function with arity 0.
A FOL language consists of disjoint sets of predicate symbols and functions, and variables. So for example, suppose you have a language with set of predicate symbols S = {P/2} (i.e. P has arity 2), set of function symbols F = {ƒ/1} and set of variables V = {x, y}. We can create the following atoms: P(ƒ(x), y), P(x, ƒ(x)), P(ƒ(y), y), P(x, ƒ(y)), P(ƒ(ƒ(x)),y), P(x, ƒ(ƒ(y))), ... etc.
We can combine atoms with the two quantifiers, ∀ and ∃ and the four logic operators ∧, ∨, → and ¬ to make well-formed formulae: ∀x∃y: P(ƒ(x), y)) ∨ P(x, ƒ(x)) etc.
With this in mind, how is FOL making functions into variables? Can you explain this a bit?
I don't get what you mean. Here's a quick reminder of first-order logic (FOL) syntax. In FOL, an atomic formula or atom is a predicate symbol followed by n ≥ 0 comma-separated terms in parentheses, where n is the arity of the predicate, terms are variables or functions, variables are quantified over functions and constants, a function is a function symbol followed by m ≥ 0 comma-separated terms in parentheses where m is the arity of the function and a constant is a function with arity 0.
A FOL language consists of disjoint sets of predicate symbols and functions, and variables. So for example, suppose you have a language with set of predicate symbols S = {P/2} (i.e. P has arity 2), set of function symbols F = {ƒ/1} and set of variables V = {x, y}. We can create the following atoms: P(ƒ(x), y), P(x, ƒ(x)), P(ƒ(y), y), P(x, ƒ(y)), P(ƒ(ƒ(x)),y), P(x, ƒ(ƒ(y))), ... etc.
We can combine atoms with the two quantifiers, ∀ and ∃ and the four logic operators ∧, ∨, → and ¬ to make well-formed formulae: ∀x∃y: P(ƒ(x), y)) ∨ P(x, ƒ(x)) etc.
With this in mind, how is FOL making functions into variables? Can you explain this a bit?
> Can you explain this a bit?
Not very well but I'll try. The idea is I'm trying to describe cannot be restricted to syntax, the summary of FOL you give is strictly syntactical. What I'm trying to observe is how predicates, functions, and variables are all variable. I mean they're all substitute-able; in this sense they're all "variable".
Predicates get evaluated to booleans so I understand them in the same "level of variable" as logical connectives. Functions always end up being evaluated into things in the domain, same as the variables; so I understand both variables and functions in their own "second level of variable".
And so, understanding (trying to) FOL this way, syntactically defined functions aren't really functions, but indirect variables. Which makes me think that the quantifiers are the actual functions (the parenthesis) which I was referring to.
In this sense the real important thing about parenthesis is the binding variables, setting them into a scope. But by this point my intuition tells me I've assumed something wrong or maybe I just leaped over something(?).
All I know is there's a reason quantifiers only take in variables (as syntactically defined) and I am trying to pin down this reason, but as I said, I still *have questions about quantifiers. In any case I've already spent way too long writing this post which might be wrong or slightly wrong/imprecise and I cannot tell how wrong and somebody would need to tell me or ask me something poignant.
Not very well but I'll try. The idea is I'm trying to describe cannot be restricted to syntax, the summary of FOL you give is strictly syntactical. What I'm trying to observe is how predicates, functions, and variables are all variable. I mean they're all substitute-able; in this sense they're all "variable".
Predicates get evaluated to booleans so I understand them in the same "level of variable" as logical connectives. Functions always end up being evaluated into things in the domain, same as the variables; so I understand both variables and functions in their own "second level of variable".
And so, understanding (trying to) FOL this way, syntactically defined functions aren't really functions, but indirect variables. Which makes me think that the quantifiers are the actual functions (the parenthesis) which I was referring to.
In this sense the real important thing about parenthesis is the binding variables, setting them into a scope. But by this point my intuition tells me I've assumed something wrong or maybe I just leaped over something(?).
All I know is there's a reason quantifiers only take in variables (as syntactically defined) and I am trying to pin down this reason, but as I said, I still *have questions about quantifiers. In any case I've already spent way too long writing this post which might be wrong or slightly wrong/imprecise and I cannot tell how wrong and somebody would need to tell me or ask me something poignant.
I think what you're getting has truth. For myself, I would generalize what you're saying as any given formula/expression is embedded in some context/environment. If one continues to "step back" or go one meta (or repeatedly so), you'll find that at some point, you, the reader/interpreter, will need to fill in some implicit or unreified context. We could call these things (shared) assumptions or axioms. As you say, if I use a function `f` to form a term in my formula written in first-order logic, the definition of `f` is implied because it is expressed "somewhere else". The question is then "where is that expressed?". Since the definition of `f` is assumed from the point of view (semantics) of first-order logic, the definition of `f` could be interpreted as "variable" at a "higher" level.
Going to your parenthesis point, I agree that it is indicating the scope (i.e., the context/environment), and in that sense, I interpret parenthesis here as a kind of meta function, akin to how macros are "compile-time" functions rather than "run-time" functions.
I think first-order logic and relatedly most (all?) logic programming languages are missing a facility for "reasoning" about terms themselves. The reflexive answer to this is types, but this is largely wielded as a developer tool not as a means of expressing meaning. Adding constraints to logic programming is perhaps some of the way there and has the benefit (hope) that type-like ideas could be expressed compositionally as logical formulas rather than as declarations provided by the language.
My own pursuit of this subject is to see if these "levels", as you hint at, can be traversed and integrated into one logical formula language and notation. This all implies some kind of homoiconic metaprogramming, but easier said than done.
Going to your parenthesis point, I agree that it is indicating the scope (i.e., the context/environment), and in that sense, I interpret parenthesis here as a kind of meta function, akin to how macros are "compile-time" functions rather than "run-time" functions.
I think first-order logic and relatedly most (all?) logic programming languages are missing a facility for "reasoning" about terms themselves. The reflexive answer to this is types, but this is largely wielded as a developer tool not as a means of expressing meaning. Adding constraints to logic programming is perhaps some of the way there and has the benefit (hope) that type-like ideas could be expressed compositionally as logical formulas rather than as declarations provided by the language.
My own pursuit of this subject is to see if these "levels", as you hint at, can be traversed and integrated into one logical formula language and notation. This all implies some kind of homoiconic metaprogramming, but easier said than done.
Indeed, I feel like I'm reaching towards a generalized understanding of context.
It seems to me that unless the logical languages are restricted from reasoing about themselves they become either incomplete or worse, inconsistent.
I have a sensation that on the computer science side of things, unless "reasoning about terms themselves" is somehow 'handled' (restricted) one can end up with undecidable systems, or worse...
But I still have questions about complexity so I cannot really undesrtand how completeness and soundness realte to decideability.
It seems to me that unless the logical languages are restricted from reasoing about themselves they become either incomplete or worse, inconsistent.
I have a sensation that on the computer science side of things, unless "reasoning about terms themselves" is somehow 'handled' (restricted) one can end up with undecidable systems, or worse...
But I still have questions about complexity so I cannot really undesrtand how completeness and soundness realte to decideability.
Thank you for the explanation. I think I understand what you're trying to say,
but what you're trying to say doesn't work in FOL. Perhaps it works in the
context of programming languages, but I can't really say.
The reason it doesn't work is that in FOL, variables, predicates and functions are not "all substitute-able". Predicates don't "evaluate to booleans". They do in some programming languages, but not in FOL. Perhaps more counter-intuitively, not even functions are "substitute-able": there are no rules for replacing a function with its value in FOL.
Let me back up a bit and point out the terminology again. I appreciate that you think what I said above is "strictly syntactical" but the idea that there is a difference between syntax and semantics is, itself, a programming language idea that does not work in FOL. In FOL, syntax and semantics are one, that's part of its power: FOL is unambiguous; what you see is what you get. For example, P ∧ Q is a conjunction: syntactically and semantically. There is no way to take P ∧ Q as anything but a conjunction, there is no compiler or interpreter translating P ∧ Q into something else. It's how you write a conjunction and it is a conjunction. FOL is WYSIWIG, yes?
So if I tell you that ƒ(x) is a function, coming from a programming language background you'd expect me to tell you how ƒ(x) is defined (as sdbrady says). In FOL, if ƒ(x) is a function, then that's the function, right there. There's nothing else to it: it's a function symbol followed by n comma-separated terms in parentheses. There's no definition of ƒ(x) "somewhere else". There is no "somewhere else". More to the point, ƒ(x) does not evaluate to anything and you can't replace ƒ(x) with its value.
In the same way predicates don't "get evaluated to booleans" - they do in some programming languages, but not in FOL. I think also you're using "predicate" itself in a programming language sense. In FOL, a predicate is the name of a relation between n entities in the domain of discourse, where n is the arity of the predicate. So P(x,y) is not a predicate, it's an atom of the predicate P of arity 2. And note that in P(x,y), x and y are variables.
Here's how this really works. In FOL, an atom is ground when it has no variables. P(x,y) is not ground, P(a,b) is ground if a and b are constants. Ground atoms are assigned truth values by an interpretation. An interpretation can be written as the set of true atoms. So for example, I = {P(a,b), P(c,d)} is an interpretation under which the atoms P(a,b) and P(c,d) are true and all other atoms are false. Note that interpretations are in a sense completely arbitrary, in that the same set of atoms can be assigned different truth values by different interpretations and there can be as many interpretations as subsets of a set of atoms. So it's literally "an interpretation".
Interpretations assign truth values to atoms so given an interpretation we can derive the truth values of more complex formulae. Remember that atoms are "atomic formulae", i.e. the simplest FOL formulae. We can make more complex formulae by using the four logical operators. So for instance, we can write the formula P(a,b) ∧ P(c,d). Under the interpretation I in my example above, the preceding formula is true, because both of the operands of the conjunction are true under I. The formula P(a,b) ∧ P(d,e) is not true under I because P(d,e) is not true under I.
How about variables and quantifiers? Remember that an atom is a predicate symbol followed by n comma-separated terms in parentheses and that terms are variables or functions (including constants, i.e. functions of arity 0). So P(x,y) is an atom with variables as terms. But, interpretations assign truth values to ground atoms, so what is the truth value of P(x,y)? It depends on the quantification of its variables. Essentially, quantifiers are a convenience that allow us to avoid having to write every formula as a -possibly infinite- set of ground atoms in order to determine the truth of the formula.
So for example, if we write ∃x,y: P(x,y) (I read that as: "there exist x and y such that P(x,y) is true") that ... does what it says on the tin. P(x,y) is true under the current interpretation for any values of x and y. If we write instead ∃x∀y: P(x,y) then we're saying that P(x,y) is true under the current interpretation for at least one value of x and all values of y.
In our example, ∃x,y: P(x,y) is true under I because there exist at least two values of x and y that make P(x,y) true, under I. ∃x∀y: P(x,y) is false because there exists no value of x that makes P(x,y) true for all y under I.
Now let's go back to functions and how they're not actually replaced by their values. The canonical example of a function in FOL is probably the Peano axiom that describes the natural numbers. Here it is, in all its quantified glory:
Insted, FOL enables us to define rules of inference such as the method of analytical Tableaus or the Resolution principle. Inference rules in turn allow us to determine logical equivalences between FOL formulae. That's how it all comes together. So, under Tableau or Resolution, we can prove that (1) is equivalent to the following atomic formulae:
Oh, but you'll notice that a substitution has happened: all instances of the variable x in (1) have been substituted for ground terms in (2). Variable sustbistitutions (but not "predicate" or function substitutions!) are a mechanism introduced by Tableau and Resolution (full disclosure: I have only a hazy idea of Tableau, but I think variable subsitutions are defined slightly differently than in Resolution). They are not part of FOL, as such, but more like plug-ins. In FOL, variables are quantified over terms, and that's all. Inference rules allow us to derive new atoms (or entire new theorems) from FOL formulae with quantified variables by substituting those variables with other terms, but that's inference rules, built on top of FOL and not FOL itself. Inference rules perform reasoning over FOL expressions. In a sense, FOL is the language and the inference rules are the speakers of the language.
Well, that's my interpretation. You'll be hard pressed, unfortunately, to find all that in one place all together, and you may find bits and pieces of it lying around scattered in papers or books about logic programming and in particular Prolog. I assume that's where you get your definitions from, perhaps from functional programming books that also discuss logic programming? This is a rather large comment already but suffice it to say that logic programming is _yet another_ extension of FOL (usually based on the Resoultion inference rule) and that the most popular logic programming language, Prolog, takes many liberties with both logic programming principles and FOL principles. Prolog definitely has "syntax" and "semantics" that are two different things. In particular, Prolog syntax has a declarative semantics and a procedural semantics, and neither of the two is quite exactly FOL. To make matters worse, Prolog runs roughshod over FOL terminology, so for example what are called "atoms" in Prolog are actually constants in FOL, and that can cause much confusion (true story). But like I say, that's a different story, for another Saturday, perhaps.
The reason it doesn't work is that in FOL, variables, predicates and functions are not "all substitute-able". Predicates don't "evaluate to booleans". They do in some programming languages, but not in FOL. Perhaps more counter-intuitively, not even functions are "substitute-able": there are no rules for replacing a function with its value in FOL.
Let me back up a bit and point out the terminology again. I appreciate that you think what I said above is "strictly syntactical" but the idea that there is a difference between syntax and semantics is, itself, a programming language idea that does not work in FOL. In FOL, syntax and semantics are one, that's part of its power: FOL is unambiguous; what you see is what you get. For example, P ∧ Q is a conjunction: syntactically and semantically. There is no way to take P ∧ Q as anything but a conjunction, there is no compiler or interpreter translating P ∧ Q into something else. It's how you write a conjunction and it is a conjunction. FOL is WYSIWIG, yes?
So if I tell you that ƒ(x) is a function, coming from a programming language background you'd expect me to tell you how ƒ(x) is defined (as sdbrady says). In FOL, if ƒ(x) is a function, then that's the function, right there. There's nothing else to it: it's a function symbol followed by n comma-separated terms in parentheses. There's no definition of ƒ(x) "somewhere else". There is no "somewhere else". More to the point, ƒ(x) does not evaluate to anything and you can't replace ƒ(x) with its value.
In the same way predicates don't "get evaluated to booleans" - they do in some programming languages, but not in FOL. I think also you're using "predicate" itself in a programming language sense. In FOL, a predicate is the name of a relation between n entities in the domain of discourse, where n is the arity of the predicate. So P(x,y) is not a predicate, it's an atom of the predicate P of arity 2. And note that in P(x,y), x and y are variables.
Here's how this really works. In FOL, an atom is ground when it has no variables. P(x,y) is not ground, P(a,b) is ground if a and b are constants. Ground atoms are assigned truth values by an interpretation. An interpretation can be written as the set of true atoms. So for example, I = {P(a,b), P(c,d)} is an interpretation under which the atoms P(a,b) and P(c,d) are true and all other atoms are false. Note that interpretations are in a sense completely arbitrary, in that the same set of atoms can be assigned different truth values by different interpretations and there can be as many interpretations as subsets of a set of atoms. So it's literally "an interpretation".
Interpretations assign truth values to atoms so given an interpretation we can derive the truth values of more complex formulae. Remember that atoms are "atomic formulae", i.e. the simplest FOL formulae. We can make more complex formulae by using the four logical operators. So for instance, we can write the formula P(a,b) ∧ P(c,d). Under the interpretation I in my example above, the preceding formula is true, because both of the operands of the conjunction are true under I. The formula P(a,b) ∧ P(d,e) is not true under I because P(d,e) is not true under I.
How about variables and quantifiers? Remember that an atom is a predicate symbol followed by n comma-separated terms in parentheses and that terms are variables or functions (including constants, i.e. functions of arity 0). So P(x,y) is an atom with variables as terms. But, interpretations assign truth values to ground atoms, so what is the truth value of P(x,y)? It depends on the quantification of its variables. Essentially, quantifiers are a convenience that allow us to avoid having to write every formula as a -possibly infinite- set of ground atoms in order to determine the truth of the formula.
So for example, if we write ∃x,y: P(x,y) (I read that as: "there exist x and y such that P(x,y) is true") that ... does what it says on the tin. P(x,y) is true under the current interpretation for any values of x and y. If we write instead ∃x∀y: P(x,y) then we're saying that P(x,y) is true under the current interpretation for at least one value of x and all values of y.
In our example, ∃x,y: P(x,y) is true under I because there exist at least two values of x and y that make P(x,y) true, under I. ∃x∀y: P(x,y) is false because there exists no value of x that makes P(x,y) true for all y under I.
Now let's go back to functions and how they're not actually replaced by their values. The canonical example of a function in FOL is probably the Peano axiom that describes the natural numbers. Here it is, in all its quantified glory:
∀x: n(0) ∧ n(x) → n(s(x)) (1)
Insted, FOL enables us to define rules of inference such as the method of analytical Tableaus or the Resolution principle. Inference rules in turn allow us to determine logical equivalences between FOL formulae. That's how it all comes together. So, under Tableau or Resolution, we can prove that (1) is equivalent to the following atomic formulae:
n(0), n(s(0)), n(s(s(0))), n(s(s(s(0)))), ... (2)
Oh, but you'll notice that a substitution has happened: all instances of the variable x in (1) have been substituted for ground terms in (2). Variable sustbistitutions (but not "predicate" or function substitutions!) are a mechanism introduced by Tableau and Resolution (full disclosure: I have only a hazy idea of Tableau, but I think variable subsitutions are defined slightly differently than in Resolution). They are not part of FOL, as such, but more like plug-ins. In FOL, variables are quantified over terms, and that's all. Inference rules allow us to derive new atoms (or entire new theorems) from FOL formulae with quantified variables by substituting those variables with other terms, but that's inference rules, built on top of FOL and not FOL itself. Inference rules perform reasoning over FOL expressions. In a sense, FOL is the language and the inference rules are the speakers of the language.
Well, that's my interpretation. You'll be hard pressed, unfortunately, to find all that in one place all together, and you may find bits and pieces of it lying around scattered in papers or books about logic programming and in particular Prolog. I assume that's where you get your definitions from, perhaps from functional programming books that also discuss logic programming? This is a rather large comment already but suffice it to say that logic programming is _yet another_ extension of FOL (usually based on the Resoultion inference rule) and that the most popular logic programming language, Prolog, takes many liberties with both logic programming principles and FOL principles. Prolog definitely has "syntax" and "semantics" that are two different things. In particular, Prolog syntax has a declarative semantics and a procedural semantics, and neither of the two is quite exactly FOL. To make matters worse, Prolog runs roughshod over FOL terminology, so for example what are called "atoms" in Prolog are actually constants in FOL, and that can cause much confusion (true story). But like I say, that's a different story, for another Saturday, perhaps.
[deleted]
Maybe I should have said 'interpretation instead of 'evaluation' (now wondering about the subtle difference between these two, if any)
Everything concerning interpretation is on the semantic side of any analysis of any logical system, such as FOL.
The point I'm trying to note is that predicates, and constant atomic terms are on the ground level; maybe we can say that they get interpreted into boolean. And functions, constants (0-arity functions) are on a different level; maybe I'll say they get evaluated into elements in the domain; i.e. they are not interpreted into boolean truth/false values.
All these because personally I find something dissatisfying about quantifiers...
So maybe I'm just trying to reinterpret quantifiers as some sort of a generalized function-like object which corresponds to parenthesis and their context-defining abilities?
Finally, I'll add that I've never learned prolog, and that a lot of these thoughts are not limited to classic FOL. I'm also thinking about modal logic, µ-calculus with it's quantifier-like fixed point operators, etc...
thanks btw.
Everything concerning interpretation is on the semantic side of any analysis of any logical system, such as FOL.
The point I'm trying to note is that predicates, and constant atomic terms are on the ground level; maybe we can say that they get interpreted into boolean. And functions, constants (0-arity functions) are on a different level; maybe I'll say they get evaluated into elements in the domain; i.e. they are not interpreted into boolean truth/false values.
All these because personally I find something dissatisfying about quantifiers...
So maybe I'm just trying to reinterpret quantifiers as some sort of a generalized function-like object which corresponds to parenthesis and their context-defining abilities?
Finally, I'll add that I've never learned prolog, and that a lot of these thoughts are not limited to classic FOL. I'm also thinking about modal logic, µ-calculus with it's quantifier-like fixed point operators, etc...
thanks btw.
You're welcome, but I think you're still mixing up programming language concepts with FOL concepts.
>> The point I'm trying to note is that predicates, and constant atomic terms are on the ground level; maybe we can say that they get interpreted into boolean. And functions, constants (0-arity functions) are on a different level; maybe I'll say they get evaluated into elements in the domain; i.e. they are not interpreted into boolean truth/false values.
Not in FOL. There are no "boolean truth/false values" in FOL. That is to say, there are two truth values that can be assigned to atoms by an interpretation, but they do not have any concrete representation in FOL. There isn't any FOL entity, term, atom, or formula, that means "true" nor one that means "false". Accordingly, nothing "evaluates" or "is interpreted" into "true" or "false" or to anything else. There's no way to write, in FOL something like "P(a,b) = true" and even equality is not a FOL concept. You certainly can't magically replace P(a,b) with its truth value in a formula, because there's nothing that can represent a truth value in a formula in FOL. Neither can you replace ƒ(x,y) with the constant "a" in some atom, because there are no rules for replacing anything with anything else at all, in FOL.
I appreciate that you find it hard to believe, and think that I'm somehow confusing your "semantic analysis" with a syntactic description of FOL because that's how it works in programming languages, but like I said before, that is part of the power of FOL: syntax and semantics are one. All of FOL is right there in the four logical operators, the sets of predicate and function symbols and the parentheses and commas used to form well-formed formulae. Well-formed formulae have a truth value that depends on the truth values assigned to atoms by the current interpretation but there's no "evaluation" or "interpretation", or even "computation" and there isn't any rule for replacing anything with "true" and "false" values or "elements in the domain" because there is nothing representing truth values and there are no rules for replacing atoms or functions with anything. You form a FOL formula and it is either true or false, depending on how you formed it. You might misread it or misunderstand it, but that's another matter.
The reason for all this weirdness is that FOL is made to be used by humans, not computers. FOL was created before computers and computers were modelled after mathematical logic concepts some of which were borrowed from FOL. But FOL is not for computers, it's for human beings. And human beings don't need to do and probably are even incapable of, the semantic analysis that a computer must, to process a statement in a formal language. So if you're trying to understand FOL in the context of computers, you're in the wrong context.
Anyway, good luck with what you're doing, but I think it will help you to try to clear up your understanding of the various terminologies and formalisms you are trying to use. Unfortunatly I don't know what text to recommend for this puprose. My go-to source for FOL is Foundations of Inductive Logic Programming by Nienhuys-Cheng and De Wolf. It's about ILP, but to understand ILP it is necessary to understand logic programming, to understand logic programming it is necessary to understand FOL and to understand FOL it is necessary to understand propositional logic so the first couple of chapters are about propositional logic and FOL. Still, it's probably not the kind of source you need. You can probably find a suitable textbook with an online search though.
>> The point I'm trying to note is that predicates, and constant atomic terms are on the ground level; maybe we can say that they get interpreted into boolean. And functions, constants (0-arity functions) are on a different level; maybe I'll say they get evaluated into elements in the domain; i.e. they are not interpreted into boolean truth/false values.
Not in FOL. There are no "boolean truth/false values" in FOL. That is to say, there are two truth values that can be assigned to atoms by an interpretation, but they do not have any concrete representation in FOL. There isn't any FOL entity, term, atom, or formula, that means "true" nor one that means "false". Accordingly, nothing "evaluates" or "is interpreted" into "true" or "false" or to anything else. There's no way to write, in FOL something like "P(a,b) = true" and even equality is not a FOL concept. You certainly can't magically replace P(a,b) with its truth value in a formula, because there's nothing that can represent a truth value in a formula in FOL. Neither can you replace ƒ(x,y) with the constant "a" in some atom, because there are no rules for replacing anything with anything else at all, in FOL.
I appreciate that you find it hard to believe, and think that I'm somehow confusing your "semantic analysis" with a syntactic description of FOL because that's how it works in programming languages, but like I said before, that is part of the power of FOL: syntax and semantics are one. All of FOL is right there in the four logical operators, the sets of predicate and function symbols and the parentheses and commas used to form well-formed formulae. Well-formed formulae have a truth value that depends on the truth values assigned to atoms by the current interpretation but there's no "evaluation" or "interpretation", or even "computation" and there isn't any rule for replacing anything with "true" and "false" values or "elements in the domain" because there is nothing representing truth values and there are no rules for replacing atoms or functions with anything. You form a FOL formula and it is either true or false, depending on how you formed it. You might misread it or misunderstand it, but that's another matter.
The reason for all this weirdness is that FOL is made to be used by humans, not computers. FOL was created before computers and computers were modelled after mathematical logic concepts some of which were borrowed from FOL. But FOL is not for computers, it's for human beings. And human beings don't need to do and probably are even incapable of, the semantic analysis that a computer must, to process a statement in a formal language. So if you're trying to understand FOL in the context of computers, you're in the wrong context.
Anyway, good luck with what you're doing, but I think it will help you to try to clear up your understanding of the various terminologies and formalisms you are trying to use. Unfortunatly I don't know what text to recommend for this puprose. My go-to source for FOL is Foundations of Inductive Logic Programming by Nienhuys-Cheng and De Wolf. It's about ILP, but to understand ILP it is necessary to understand logic programming, to understand logic programming it is necessary to understand FOL and to understand FOL it is necessary to understand propositional logic so the first couple of chapters are about propositional logic and FOL. Still, it's probably not the kind of source you need. You can probably find a suitable textbook with an online search though.
[deleted]
My instincts say that you're saying something revelatory/insightful here, at least to me, but I'm not quite sure. Would you mind expounding, either with more context or more examples?
I feel the same. The two levels of “variableness”, and the prohibition of mixing them, must have something to do with lazy vs eager evaluation, right?
The parentheses are just one of the more portable ways of showing structure. Yes, sometimes they can be dropped, but then moving an expression might become ambiguous. This is easily seen in languages like yaml where moved code is not put with the intended indention level.
Which isn't really contradicting anything here. At least, not intending to. Structure is a part of typing. And sometimes the structure is the least interesting part of the type.
Which isn't really contradicting anything here. At least, not intending to. Structure is a part of typing. And sometimes the structure is the least interesting part of the type.
I thought they denote a tree structure. At least that's how I remember it being in Scheme. You could follow the order of evaluation back to the root node. Something I wish was explained earlier, because initially I found all the parentheses confusing as Scheme was my intro to programming language.
This is true. It just so happens that stacks and trees can map to each other.
If we're talking about different syntax for Lips are-there some Lisp-variant which use fn(arg1 arg2...) instead of (fn arg1 arg2 ...) ?
I think that this is more readable as this reflects that the "role" of the first argument is different from the other arguments..
I don't know of any such variant, and I've looked. There seems to be nothing. I had this idea too, and I implemented it, see my comment here[0].
The readability argument is arguably subjective -- `fn` can be seen as special on either side of the paren -- either way it's special because it's the thing next to the paren.
The syntax is certainly more familiar for most people who had anything to do with math or ALGOL-like languages.
What is objective about this syntax though is that it removes nesting for curried functions (see the linked comment for details). I think this is the right idea.
[0] https://news.ycombinator.com/item?id=27625295
The readability argument is arguably subjective -- `fn` can be seen as special on either side of the paren -- either way it's special because it's the thing next to the paren.
The syntax is certainly more familiar for most people who had anything to do with math or ALGOL-like languages.
What is objective about this syntax though is that it removes nesting for curried functions (see the linked comment for details). I think this is the right idea.
[0] https://news.ycombinator.com/item?id=27625295
On lisp and types, I prefer this article: https://alhassy.github.io/TypedLisp a primer - let's explore Lisp's fine-grained type hierarchy! with a shallow comparison to Haskell.
>"Consider this Scheme expression, taken from the Rosetta Code example for the Mandelbrot set:
(boolean->integer
Stack languages are a mirror image of Lisps, written in postfix rather than prefix notation.
So a Forth-like version of this expression would be the same words in reverse, without the parentheses:
j pixel-size * y-offset -
i pixel-size * x-offset +
make-rectangular inside? boolean->integer"
PDS: I know about both LISP and Forth -- but until I read this article, I never made this simple, intuitive, elegant, and utterly brilliant -- connection!
Yes, it's absolutely true!
And it's utterly, utterly brilliant!!!
To the Author: Thank you for writing this article!!!
(boolean->integer
(inside?
(make-rectangular (+ x-offset (\* pixel-size i))
(- y-offset (\* pixel-size j))))
Stack languages are a mirror image of Lisps, written in postfix rather than prefix notation.
So a Forth-like version of this expression would be the same words in reverse, without the parentheses:
j pixel-size * y-offset -
i pixel-size * x-offset +
make-rectangular inside? boolean->integer"
PDS: I know about both LISP and Forth -- but until I read this article, I never made this simple, intuitive, elegant, and utterly brilliant -- connection!
Yes, it's absolutely true!
And it's utterly, utterly brilliant!!!
To the Author: Thank you for writing this article!!!
Sort of. The parenthesis around an expression like (a b +) imply a result of some type. That type is defined by the whatever type promotion rules are in place for the operands and operators. Thus, if a and b are integers in the range -MIN_VALUE to MAX_VALUE, and + is defined as integer addition, then the 'type' implied by (a b +) is an integer in that range (or possibly an error condition, if under/overflow).
The reason you don't see a stack language that evaluates from left to right is because then it wouldn't be a stack language.
The reason you don't see a stack language that evaluates from left to right is because then it wouldn't be a stack language.
But stack languages generally do evaluate left to right.
I don't see why you couldn't do right to left. Makes no semantic difference.
But the original post has a snippet that should not only be evaluated right to left, but also bottom to top. Unless their indentation implies hidden parens.
I don't see why you couldn't do right to left. Makes no semantic difference.
But the original post has a snippet that should not only be evaluated right to left, but also bottom to top. Unless their indentation implies hidden parens.
Yeah, I mean right-to-left, in response to the question the article asks: Why have I never seen... ...a stack language that evaluates right-to-left?
it's because the tokens are evaluated in the order they are consumed by the parser. But now that I think about it, the tokens only look left-to-right because that's how the text is displayed. So what's really happening is that tokens are evaluated in FIFO, and there's no reason the tokens for (a b +) couldn't be written as (+ b a).
it's because the tokens are evaluated in the order they are consumed by the parser. But now that I think about it, the tokens only look left-to-right because that's how the text is displayed. So what's really happening is that tokens are evaluated in FIFO, and there's no reason the tokens for (a b +) couldn't be written as (+ b a).
dominant is right to left reading cultures western In
But it's entirely reasonable to ask why we didn't learn to
think in right to left reading of stack order
didn't nonetheless but
oh sorry
tub sselehtenon t'ndid
oh sorry (trys again)
bibn'ɟ nonɘɟ⑁ɘlɘƨƨ duɟ
After all, treat your strings badly in Python and they do
expose as .. lists .. which are .. stacks .. kinda.>a Lisp that can drop nested parentheses when the meaning is clear from context
It's not a lisp, but Elm with Aaron VonderHaar's elm-format does that and it is very pleasant.
It's not a lisp, but Elm with Aaron VonderHaar's elm-format does that and it is very pleasant.
Red and Rebol have prefix notation and no parentheses to delimit the arguments. That means you have to know the arity of each function to understand how to build the parse tree. This is apparently not as hard as it sounds, because natural languages work the same way, although they can be ambiguous, at least if you're familiar with all the functions.
Stoical uses {} instead of () to do grouping, and is a reverse polish concatenative language. I tried to port it to 64 bit C, but my C foo isn't up to the task.
http://stoical.sourceforge.net/documentation.php
http://stoical.sourceforge.net/documentation.php
If comparing to something like Forth, I think it's better to consider the parens as push and pop operators.
- Lisp only needs parentheses because its operators have variable arity, that’s about as deep as the “type system” goes.
- The concatenative languages wiki <https://concatenative.org> only lists Om <http://om-language.org> among the (non-reverse) Polish notation concatenative languages, but its semantics are a bit more tricky than those for RPN languages when expressed in terms of left-to-right evaluation (stream processing, not stacks).
- Unrelated, but see XY <http://www.nsl.com/k/xy/xy.htm> for a very elegant RPN semantics.
- I think I’ve heard that the APL semantics is commonly described right to left so might be related?
- The proposed Lisp-2 notation with a syntactic distinction between operators and operands strongly reminds me of how the Self expression syntax <https://handbook.selflanguage.org/2017.1/langref.html#expres...> works (its main difference from Smalltalk).