1
$\begingroup$

This question is sequel from How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"? which further explains the notation and context.

So - I have anonymous Boolean-valued function F(y)=λx.Φ(x) (of course, y and x point to the same variable, I just used different syntactic names, to point out, that x is bound variable) and I would like to write the statement, that F(x) is true for all the values of the argument and it can be written ∀x.F(x). But F(x) is named function, but I would like to write the same expression (that λx.Φ(x) is true for all values of argument, all values of x) for the anonymous function that uses lambda, so I am with my suggestion: ∀x.λx.Φ(x) or ∀x.λy.Φ(y)? And apparently they both are wrong. What is correct way to express, using quantifier, that expression λx.Φ(x) is true for all values of x?

Generally my concern (and therefore - my question) is valid. Let's consider F(x,y)=λx.λy.Φ(x, y). In that case ∀F is ambigous (there is big difference between ∀x.F(x, y) and ∀y.F(x, y)) and ∀∀F and would be even more ambigous for functions with argument count n>=3. So, should mention argument explicitly. But I guess - noone can refer to some argument explicitly for the function that is written in anonymous form (with λ) or am I wrong? I am so confused about this notation - how to refere the argument of anonymous function which is referred by ?

What I am trying to achieve? I just want to build parser for language that is declared in https://www.isa-afp.org/browser_info/current/AFP/GoedelGod/GoedelGod.html. This language contains expressions like [∀(λΦ. P (λx. m¬ (Φ x)) m→ m¬ (P Φ))].

I am using ANTLR grammar for lambda calculus https://github.com/antlr/grammars-v4/blob/master/lambda/lambda.g4 and I understand that the 1) quantifiers; 2) logical connectives; 3) arithmetic functions are just another lambda functions (it is just syntactic sugar that they are written in the specific non-lambda syntax/prefix form etc.) and as such I express them in the existing lambda.g4 grammar https://github.com/antlr/grammars-v4/blob/master/lambda/lambda.g4. So - my first step is to write the cited expressions with the named functions and then I will just replace them with anonymous functions because lambda.g4 has no options to introduce named functions. But it is so confusing to write anonymous function and the quantifier function for the same argument.

Just side question - maybe there is better ANTLR grammar for lambda calculus with syntactic sugar for quantifiers and connectives?

$\endgroup$
12
  • 1
    $\begingroup$ I'm having a hard time understanding what your question is. Might you be able to edit the question to help state clearly what question you want answered? Also, the site's format is usually best for questions that are self-contained and don't require reading other resources to understand what's being asked. $\endgroup$
    – D.W.
    Aug 21, 2020 at 1:02
  • 1
    $\begingroup$ Didn't the answer to the linked question (which you accepted) actually answer the question? It seems like this question just requires a repetiton of that other answer. Using $\forall$ as a binding form just confuses the issue because it is not (essentially) a binding form; it is a function whose domain is functions and whose range is boolean values. Insisting on writing "$\forall y F(y) \text{ where } F=\lambda x.\Phi(x)$" makes an unnecessary cloud of bindings; what is actually meant is simply $\forall \Phi$. $\endgroup$
    – rici
    Aug 21, 2020 at 5:38
  • 1
    $\begingroup$ That is, $\forall\Phi$ evaluates to $true$ if $\Phi x$ is true for every $x$. $\endgroup$
    – rici
    Aug 21, 2020 at 5:39
  • 1
    $\begingroup$ No-one is asking you to accept $\forall x.F(x)$. If you can shake off the need to write that, you'll find the language is quite simple. $\forall$ is just a unary operator like $\neg$. $\endgroup$
    – rici
    Aug 21, 2020 at 5:49
  • 1
    $\begingroup$ What does $\forall.xF(x,y)$ mean to you? Is that $y$ a free variable? In that case, you can curry $F$ (or $\Phi$ directly). Or does it have some other meaning? $\endgroup$
    – rici
    Aug 21, 2020 at 6:33

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.