which self-referential sentence are you trying to avoid?
it keeps sounding to me like you’re saying “i want a λ-calculus combinator that produces the fixpoint of a given function f, but i don’t want to use the Y combinator”.
do you deny the alleged analogy between the normal proof of löb and the Y combinator? (hypothesis: maybe you see that the diagonal lemma is just the type-level Y combinator, but have not yet noticed that löb’s theorem is the corresponding term-level Y combinator?)
if you follow the analogy, can you tell me what λ-term should come out when i put in f, and how it’s better than (λ s. f (s s)) (λ s. f (s s))?
or (still assuming you follow the analogy): what sort of λ-term representing the fixpoint of f would constitute “referring to itself (instead of being a term about types that refer to themselves)”? in what sense is the term (λ s. f (s s)) (λ s. f (s s)) failing to “refer to itself”, and what property are you hoping for instead?
(in case it helps with communication: when i try myself to answer these questions while staring at the OP, my best guess is that you’re asking “instead of the Y combinator, can we get a combinator that goes like f ↦ f ????”, and the two obvious ways to fill in the blanks are f ↦ f (Y f) and f ↦ f (f (f (.... i discussed why both of those are troublesome here, but am open to the possibility that i have not successfully understood what sort of fixpoint combinator you desire.)
(ETA: also, ftr, in the proof-sketch of löb’s theorem that i gave above, the term "g "g"" occurs as a subterm if you do enough substitution, and it refers to the whole proof of löb’s theorem. just like how, in the version of the Y combinator given above, the term g g occurs as a subterm if you do enough β-reduction, and it refers to the whole fixpoint. which i note b/c it seems to me that you might have misunderstood a separate point about where the OP struggles as implying that the normal proof isn’t self-referring.)
((the OP is gonna struggle insofar as it does the analog of asking for a λ-term x that is literally syntactically identical to f x, for which the only solution is f (f (f (... which is problematic. but a λ-term y that β-reduces pretty quickly to f y is easy, and it’s what the standard constuction produces.))
At this point I’m more interested in hashing out approaches that might actually conform to the motivation in the OP. Perhaps I’ll come back to this discussion with you after I’ve spent a lot more time in a mode of searching for a positive result that fits with my motivation here. Meanwhile, thanks for thinking this over for a bit.
well, in your search for that positive result, i recommend spending some time searching for a critch!simplified alternative to the Y combinator :-p.
not every method of attaining self-reference in the λ-calculus will port over to logic (b/c in the logical setting lots of things need to be quoted), but the quotation sure isn’t making the problem any easier. a solution to the OP would yield a novel self-reference combinator in the λ-calculus, and the latter might be easier to find (b/c you don’t need to juggle quotes).
if you can lay bare the self-referential property that you’re hoping for in the easier setting of λ-calculus, then perhaps others will have an easier time understanding what you want and helping out (and/or you’ll have an easier time noticing why your desires are unsatisfiable).
(and if it’s still not clear that löb’s theorem is tightly connected to the Y combinator, such that any solution to the OP would immediately yield a critch!simplified self-reference combinator in the λ-calculus, then I recommend spending a little time studying the connection between the Y combinator, löb’s theorem, and lawvere’s fixpoint theorem.)
which self-referential sentence are you trying to avoid?
it keeps sounding to me like you’re saying “i want a λ-calculus combinator that produces the fixpoint of a given function f, but i don’t want to use the Y combinator”.
do you deny the alleged analogy between the normal proof of löb and the Y combinator? (hypothesis: maybe you see that the diagonal lemma is just the type-level Y combinator, but have not yet noticed that löb’s theorem is the corresponding term-level Y combinator?)
if you follow the analogy, can you tell me what λ-term should come out when i put in
f, and how it’s better than(λ s. f (s s)) (λ s. f (s s))?or (still assuming you follow the analogy): what sort of λ-term representing the fixpoint of f would constitute “referring to itself (instead of being a term about types that refer to themselves)”? in what sense is the term
(λ s. f (s s)) (λ s. f (s s))failing to “refer to itself”, and what property are you hoping for instead?(in case it helps with communication: when i try myself to answer these questions while staring at the OP, my best guess is that you’re asking “instead of the Y combinator, can we get a combinator that goes like
f ↦ f ????”, and the two obvious ways to fill in the blanks aref ↦ f (Y f)andf ↦ f (f (f (.... i discussed why both of those are troublesome here, but am open to the possibility that i have not successfully understood what sort of fixpoint combinator you desire.)(ETA: also, ftr, in the proof-sketch of löb’s theorem that i gave above, the term
"g "g""occurs as a subterm if you do enough substitution, and it refers to the whole proof of löb’s theorem. just like how, in the version of the Y combinator given above, the termg goccurs as a subterm if you do enough β-reduction, and it refers to the whole fixpoint. which i note b/c it seems to me that you might have misunderstood a separate point about where the OP struggles as implying that the normal proof isn’t self-referring.)((the OP is gonna struggle insofar as it does the analog of asking for a λ-term
xthat is literally syntactically identical tof x, for which the only solution isf (f (f (...which is problematic. but a λ-termythat β-reduces pretty quickly tof yis easy, and it’s what the standard constuction produces.))At this point I’m more interested in hashing out approaches that might actually conform to the motivation in the OP. Perhaps I’ll come back to this discussion with you after I’ve spent a lot more time in a mode of searching for a positive result that fits with my motivation here. Meanwhile, thanks for thinking this over for a bit.
well, in your search for that positive result, i recommend spending some time searching for a critch!simplified alternative to the Y combinator :-p.
not every method of attaining self-reference in the λ-calculus will port over to logic (b/c in the logical setting lots of things need to be quoted), but the quotation sure isn’t making the problem any easier. a solution to the OP would yield a novel self-reference combinator in the λ-calculus, and the latter might be easier to find (b/c you don’t need to juggle quotes).
if you can lay bare the self-referential property that you’re hoping for in the easier setting of λ-calculus, then perhaps others will have an easier time understanding what you want and helping out (and/or you’ll have an easier time noticing why your desires are unsatisfiable).
(and if it’s still not clear that löb’s theorem is tightly connected to the Y combinator, such that any solution to the OP would immediately yield a critch!simplified self-reference combinator in the λ-calculus, then I recommend spending a little time studying the connection between the Y combinator, löb’s theorem, and lawvere’s fixpoint theorem.)