Talk:Deductive lambda calculus

This is a start only.

I have doubts about the usefulness of the Set theoretic domain section. I think it is important but I have not convinced myself or the reader that this is important. I would like to have some good references to read on this.

I have concerns that the Domain of lambda calculus section is going to be too abstract and not useful to the general reader. I am trying to represent the viewpoint of a person studying pure untyped lambda calculus, but at a simple level.

I would really appreciate the input of lambda calculus mathematicians. I would like more references. What does Barendregt say about this subject? I am hoping that the article can evolve from this start.

If any editors can suggest further reading I would be pleased to follow it up.

Thepigdog (talk) 00:16, 22 February 2014 (UTC)

Clarification

Thanks for the requests for clarification. I have responded to,

1. Indicate whether typed or untyped Lambda calculus is meant here. In untyped Lambda calculus, not every term has a normal form.
2. Indicate clearly where the 'Logical inconsistency' mentioned in the section heading consists in. Having equations with zero or multiple solutions doesn't appear to be an inconsistency.

I have modified the text in order to clarify the text. For point (1) I am trying to start with a computer programmers understanding of lambda Calculus, where lambda calculus is as an expression in the domains commonly used in mathematics. In section 6 Domain of lambda calculus, I attempt to explain a pure lambda calculus interpretation where every lambda term represents a single value.

Thepigdog (talk) 06:55, 19 May 2014 (UTC)

Thank you for your explanations. Unfortunatley, I still don't understand your argumentation. I have put some new lengthy "clarify" requests at some places where I have problems. Feel free to remove them if you find them annoying - I'm aware that they should better be discussed on this talk page, but I liked to omit lengthy descriptions of the place I refer to (like "In the 3rd line from above in section 'No solutions', ..."). My vague overall impression of section "Logical inconsistency" is that if I could understand it, its point might be the same that is already made in Curry's paradox#Lambda calculus. - Jochen Burghardt (talk) 19:38, 20 May 2014 (UTC)

Thank you for your requests for clarification. Feel free to add clarification points and or add comments under talk, as you feel is best to make your point. I will address them as soon as I can. I really want the article to be correct and clear, so any input you make is greatly valued.

Thepigdog (talk) 00:55, 21 May 2014 (UTC)

Clarification points,

• Since x was defined by the equation x = ¬x, it cannot be defined again as y y. So, apparently y shall be defined here as a (or: the only?) solution of the equation x = y y. In order for this definition to be acceptable, it should be justified why such a (unique?) solution exists. As a side remark, it would be helpful to explain that 'y y' means (as I guess) function application of lambda terms, not multiplication of Church-encoded numbers.

'y y' means function application. I have added a terminology section to hopefully clarify this.

The numbers for this discussion are the reals. I am not considering Church encoding here.

• Is this a redefinition of x?

I have reworked this section.

• Indicate which equality is meant by '=' in the following set expression. (It might be helpful anyway throughout the whole article to use different characters for syntactic equality of lambda terms and for the 'mathematical interpretation', i.e. for equality modulo beta and eta reduction.) Also note that there is an untyped lambda term f such that (f f) evaluates to (¬ (f f)), viz. f = λx.(¬ (x x)). So it is not clear in which sense the set expression should be read in order to get cardinality 0.

The equality is mathematical equality (see new Terminology section).

The domain here is the real domain, not the lambda calculus domain of functions. I have attempted to clarify this in the terminology section.

Comment:

• added remarks as clarify requests, cf. talk page; suggested parantheses to distinguish let equation x = (let f y =¬(y y) in f f ) from -nonsensical- equation chain x = (let f y) = (¬(y y) in f f ))

But too many brackets are confusing for the reader (and me). I have added the let expression to the new terminology section. I hope that will suffice. Let and in bracket a condition, applied to another condition. I haven't specified exactly what the precedence is but I consider let/in to have a lower precedence than = but higher than equivalence, implication.

Thepigdog (talk) 11:02, 21 May 2014 (UTC)

---

Anonymous remarks

1. "\x.y z" usually means "\x(y z)"

Yes you can write it like that. It is not the notation used in this article.

2. "As beta reduction is implied from eta reduction, there is no contradiction between the two definitions." Rules \beta and \eta are indeopendent.

"In the mathematical interpretation, lambda terms represent values. Eta and beta reductions are deductive steps that do not alter the values of expressions." This makes beta and eta reduction not independent. Beta reduction is implied by eta reduction.

I moved the terminology section out into a separate section. Hopefully this will make the argument easier to follow.

3. "The left hand side may often be shown to be false where x = f" Nonsence: The x is placeholder, you cannnot substitute. Moreover, x is variable , f is lambda-term, so they are different syntactical categories.

Restructured this section. The notation was confusing.

4. "2 * (r + s) = 2*r + 2*s" -> 2*(r + s) = r+s+r+s ?=? r+r+s+s = 2*r + 2*s, only if + is commutative. Functions aren't commutative. You have different functions, which sometimes give the same result. - for church numerals

\r\s.2*(r+s) = \r\s.2*r + 2*s according to the distributive law these functions are extensionally equal. They are the same function. But they are different functions and not equal by intensional equality.

I have changed the wording to hopefully clarify from the start that the two functions are not intensionally equal but the distributive law says they are equal.

4a. Exaample is strange: Discriminate: functions values are the same for all church numerals versus (extensionality ->) for all lambda terms

Not sure if I understand your point.

My point is that the two functions given are extensionally equal but not intensionally equal. The two functions applied to church numerals will get the same result. But the two functions not applied to any parameter cannot beta reduce further and are therefore not equal, even though they are extensionally equal.

5. "This definition is an unsolved equation for F. So is there a solution for F?" - Yes, it is. Single point F = {0}.

The proof does not rule this out.

"Therefore, if there exists a function that may not be applied to itself, then there is no set F satisfying the above definition of 'all functions'".

5a. As you don't rule out in the following this solution, the proof is incorrect (or incomplete). Try compare with Rice's theorem for usual approach.

The proof is only that there is no solution for F including a function that can not be applied to itself. So it does not completely rule out a set of function F. It just restricts it. What is your suggestion?

I have changed the wording to hopefully clarify the issue. There is no actual problem with the lambda calculus domain, considered as a set, but if you add functions that are not defined on themselves, you get a contradiction. Interested in your comments on this and if there is a better approach here.

The set theoretic approach given here is similar to Rice's theorem. But it is simpler to understand

6. "instantiate x as g." - You cannot, as you supposed that g g is undefined.

I have,

$f\in F\iff (\forall x:x\in F\implies f\ x\in F)$

I have said that g g is not in F, but not that g is not in f. Therefore I am entitled to instantiate x as g.

And this leads to a contradiction.

7. "If not then the undecidability of equivalence shows that in general there is no algorithm to determine if two lambda terms are equal." - What it has to do with domains?

If you can't decide if two expressions are equal how can you determine the set of elements in the domain?

8. "represents two values in the domain of the signed numbers. However it is a lambda expression so has only one value in the lambda calculus domain. Beta reduction of this lambda term never reaches normal form. However it represents a value, so a single value in the lambda calculus domain represents two values in the signed number domain." - it represents the function as well, which for positive resp. negative argument returns positive resp. negative root. (The n can be zero.) Or divergence for negative n - as in the previous example in the article.

Yes for n not equal to zero, two values.

Yes in the lambda calculus domain, it is one value by definition. It is what it is.

But considered as an expression on signed numbers it represents two values in the domain of signed numbers (for non zero n).

What change are you suggesting?

89.103.101.115 (talk) 21:25, 18 September 2014 (UTC)

I apologize for the delay in responding. I value your comments. I have tried to address them in the comments above. Thepigdog (talk) 05:54, 30 October 2014 (UTC)

Request for assistance

• Henk Barendregt, The Impact of the Lambda Calculus in Logic and Computer Science. The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997.

• Illative lambda calculus
• Type systems
• Illative lambda calculi

Request for the addition of a section on this subject.

Thepigdog (talk) 18:17, 14 November 2014 (UTC)

Where does this material come from?

I don't recognise this term from secondary literature. Does it come from a reference that we can name? — Charles Stewart (talk) 07:13, 16 June 2016 (UTC)

I'm fairly certain this term was invented by User:Thepigdog. —Ruud 10:14, 16 June 2016 (UTC)

Curry used the term illative.

illative ɪˈleɪtɪv/Submit adjective 1. of the nature of or stating an inference.

Deductive seemed more accessible to the average reader.

(interesting addition about omega-rule)

Thepigdog (talk) 01:18, 20 August 2016 (UTC)

Question

In general the definition,

$f\ x=y\iff f=\lambda x.y$

leads to contradictions. What is the condition C on f that makes that definition valid?

$C(f)\iff (f\ x=y\iff f=\lambda x.y)$

Thanks for your assistance.

Thepigdog (talk) 21:47, 20 August 2016 (UTC)

Question

In general the definition,

$f\ x=y\iff f=\lambda x.y$

leads to contradictions. What is the condition C on f that makes that definition valid?

$C(f)\iff (f\ x=y\iff f=\lambda x.y)$

Thanks for your assistance.

Thepigdog (talk) 21:47, 20 August 2016 (UTC)

WHATS FV

NO ONE KNOWS WHAT FV IS

X IS NOT IN IT THOUGH WHEN ETA REDUTION HAPPENS

THANK YOU

FV is short for Free Variable. It is a meta-function that gives the free variables of an expression. Thepigdog (talk) 04:00, 11 July 2021 (UTC)