Typing inference as a map on abstract syntax trees Is there a reference that explains typing inference for Martin-Löf type theory as a computable map from abstract syntax trees of terms to abstract syntax trees of types? I don't want to identify non-identical judgmentally equal things.
The terms and the types are all defined in the empty context and we also include annotations for the variable types in lambda abstractions.
If there is such a map then is it true if a type is not in beta normal form then it has no terms in beta normal form map to it?
Type inference for dependent type theory is undecidable in general, so what you're asking for is impossible. However, it is possible to separate the syntax into inferrable terms and checkable terms, and implement inference for the inferrable fragment. This is the approach taken by bidirectional typechecking. The paper on LambdaPi by Andres Löh, Conor McBride and Wouter Swierstra describes a tutorial implementation of a dependent typechecker in this style. More advanced typecheckers for dependently typed languages typically rely on higher-order unification to infer the types for more expressions, a good example is the paper on Higher-order Dynamic Pattern Unification by Andreas Abel and Brigitte Pientka.
Regarding your second question, this claim is false: the conversion rule of dependent type theory says that a type is inhabited if and only if its normal form is inhabited. So a type such as (\(X:Type). x) Nat is not in beta normal form but is inhabited by the normal forms zero, suc zero, ...