Talk:Normalization property (abstract rewriting)

This is the talk page for discussing improvements to the Normalization property (abstract rewriting) redirect.
This is not a forum for general discussion of the article's subject.

Put new text under old text. Click here to start a new topic.
New to Wikipedia? Welcome! Learn to edit; get help.

Article policies

Find sources: Google (books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL

Example weakly but not strongly

An example of a sequence that is weakly normalizing but not strongly would be useful — Preceding unsigned comment added by LiveDuo (talk • contribs) 13:28, 8 May 2016 (UTC)[reply]

Strongly normalizing proglang cannot be Turing-complete?

Totality is not the same as Turing-completeness. Consider this [total] Brainfuck interpreter written in Agda: https://github.com/wouter-swierstra/Brainfuck

It's tempting to qualify the article statement as original research, but I'll just put in a citation request. --141.228.106.147 (talk) 17:28, 9 December 2014 (UTC)[reply]

Well, canonically, any programming language whose programs always terminate is necessarily incomplete. This is not supposed to be something mysterious that requires a citation. (for example, one total language can provide an interpreter for another; thus its no surprise that agda can interpret brainfuck. The point is that branfuck cannot interpret itself, although you can create a brainfuck-prime by attaching the agda interpreter to it. But then brainfuck-prime cannot interpret itself... etc. However, as I'm now digging around, its clear that ... the situation is subtle. See the comment immediately below, regarding Andrej Bauer, F-omega and system T. 67.198.37.16 (talk) 20:11, 15 December 2018 (UTC)[reply]

Breaking through the normalization barrier

There is a recent paper by Matt Brown and Jens Palsberg, "Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega", which constructs a self-interpreter for the strongly normalizing Fω, contrary to a claim in the article (which is even mentioned in the paper itself!):

[T]here are computable functions that cannot be defined in the simply typed lambda calculus [...]. As an example, it is impossible to define a self-interpreter in any of the calculi cited above.

It would be great if someone knowledgeable cited this paper in the article, and made it clear what was actually achieved and if the claim indeed holds. —Matěj Grabovský (talk) 23:52, 16 February 2016 (UTC)[reply]

The rebuttal is here: Andrej Bauer, "On Self-Interpreters for System T and other Typed Lambda-Calculi", which I don't understand. The upshot seems to be that the concept of "self-interpreters" includes implicit, unstated assumptions that lead to contradictory results. (Well, the diagonal argument "famously" proves that total languages can't have self-interpreters, so when one can prove that they do, something funny is going on somewhere... but again, I don't understand...) 67.198.37.16 (talk) 03:02, 16 December 2018 (UTC)[reply]

I've addressed the apparent contradictory statement emerging from that article. The authors use a nonstandard (though they did not invent it) definition of "self-interpreter" and misrepresent what this Wikipedia page is saying. LParreaux (talk) 18:34, 2 May 2021 (UTC)[reply]