Delphi.science

Full beta normal-order normalization for untyped lambda terms

Source: github.com/Arthur742Ramos/Math-Formalization/tree/dacdaecac…

Arthur Freitas Ramos, David Barros Hulak, Ruy José Guerra Barretto de Queiroz

Palomar Registrypalomar/PALOMAR-2026-11-03-000014Nov 3, 2026math.LOscore 0

Defines the deterministic full-beta leftmost-outermost strategy and proves it reaches any reachable normal form on de Bruijn terms, including open terms.

RepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-11-03-000014
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-03-000014/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-03-000014/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'