Ott
1 program
Added 2026-03-12T10:00:00Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: —
Provenance: commit d4c064e850 · authored 2026-03-12T02:34:45+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
Untyped Lambda Calculus
Provenance: commit d4c064e850 · authored 2026-03-12T02:34:45+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled
metavar termvar, x ::=
grammar
t :: 't_' ::=
| x :: :: var {{ com variable }}
| \ x . t :: :: lam {{ com abstraction }}
| t1 t2 :: :: app {{ com application }}
| ( t ) :: S :: paren {{ coq ([[t]]) }}
subrules
v <:: t
grammar
v :: 'v_' ::=
| \ x . t :: :: lam
terminals :: 'terminals_' ::=
| \ :: :: lambda {{ tex \lambda }}
| --> :: :: red {{ tex \longrightarrow }}
defns
Jop :: '' ::=
defn
t --> t' :: :: step :: 'step_' {{ com small-step evaluation }} by
--------------------------------------- :: beta
(\ x . t12) v2 --> t12 [ x := v2 ]
t1 --> t1'
---------------------- :: app1
t1 t2 --> t1' t2
t2 --> t2'
---------------------- :: app2
v1 t2 --> v1 t2'