Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

I believe that any such problems are due to non-totality and/or non-strict semantics, and generally aren't important in practice. For example, from the abstract for "Fast and Loose Reasoning is Morally Correct" (http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loos...):

  Two languages are defined, one total and one partial, with identical
  syntax. The semantics of the partial language includes partial and infinite
  values, and all types are lifted, including the function spaces. A partial
  equivalence relation (PER) is then defined, the domain of which is the total
  subset of the partial language. For types not containing function spaces the
  PER relates equal values, and functions are related if they map related values
  to related values.  It is proved that if two closed terms have the same
  semantics in the total language, then they have related semantics in the
  partial language. It is also shown that the PER gives rise to a bicartesian
  closed category which can be used to reason about values in the domain of the
  relation.



Consider applying for YC's Fall 2025 batch! Applications are open till Aug 4

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: