# Tag Info

27

Here are a few things to keep in mind: Although we generally think we know what we mean by set-theoretic intersection and union, there have been several different takes on what exactly intersection and union types are. So, it's worth pinning this down before you embark on an implementation. One element which I think is awfully important for understanding ...

22

I can think of a few possible answers coming from linear logic. The simplest one is the affine lambda-calculus: consider only lambda-terms in which every variable appears at most once. This condition is preserved by reduction and it is immediate to see that the size of affine terms strictly decreases with each reduction step. Therefore, the untyped affine ...

19

All of the following comments are premised on the choice of a standard implementation strategy using closures to represent function values and a call-by-value evaluation order: For the pure lambda calculus, garbage collection is not necessary. This is because it is not possible to form cycles in the heap: every newly-allocated value can only contain ...

17

It's common to say that $f$ and $g$ commute with respect to composition (where the property is known as commutativity). See, e.g., http://en.wikipedia.org/wiki/Function_composition.

16

You may wish to look at cost semantics for functional languages. These are various computational complexity measures for functional languages that do not pass through any kind of Turing machine, RAM machine, etc. A good place to start looking is this Lambda the Ultimate post, which has some good further references. Section 7.4 of Bob Harper's Practical ...

15

You can think of $\lambda$-abstraction as an operator $\Lambda$ which takes a function from terms to terms into a term: $$\Lambda : (\mathsf{Term} \to \mathsf{Term}) \to \mathsf{Term}.$$ The type of $\Lambda$ is higher-order because it maps functions to objects, so it is a functional of rank 2. This is where the name comes from. For example, if $\mathsf{id}$...

15

You might want to check out Liquid Haskell, which allow working with type refinements rather than dependent types. Type refinements can be seen as a restricted logical language that allow you to express Hoare-style properties of the inhabitants of various datatypes. Another possible candidate is the $F^*$ language, which offers similar constructs. There ...

14

At the request of Andrej and PhD, I am turning my comment into an answer, with apologies for self-advertising. I recently wrote a paper in which I look at how to prove the Cook-Levin theorem ($\mathsf{NP}$-completeness of SAT) using a functional language (a variant of the λ-calculus) instead of Turing machines. A summary: the key notion is that of affine ...

13

As I said in my comment, the answer in general is no. The important point to understand (I say this for Viclib, who seems to be learning about these things) is that having a programming language/set of machines in which all programs/computations terminate by no means implies that function equality (i.e., whether two programs/machines compute the same ...

13

Honda and Yoshida's A Compositional Program Logic for Polymorphic Higher-Order Functions (probably) pioneered Hoare logics for purely functional languages. This work is based on Hennessy-Milner logic and Milner's encoding of functions into processes, as described here: From Process Logic to Program Logic The work by Régis-Gianas et al mentioned in ...

12

Is it possible to make a "smart" trampoline function that takes two forms of a function, a trampolined version and a non-trampolined version, and chooses (or predicts) the most efficient strategy?* Yes, it's possible to do things like this, but if you control the compiler, it's usually faster and easier to do something else. The main exception is when you ...

12

The original paper by Church and Rosser, "Some Properties of Conversion," describes something that may be an example of what you're looking for. If you use the strict lambda calculus, where in every occurrence of $\lambda x.M$ you have that $x$ appears free in $M$, then without a type system the following property holds (it's Theorem 2 in Church and Rosser'...

11

A semantics of a program is a model of its behavior which, like any scientific model, ignores aspects that you don't want to study. An extremely detailed model of the execution of a program would model the physical behavior of the computer that executes it, including the execution time, power consumption, electromagnetic radiation, etc. Such aspects are ...

11

See also Yann Régis-Gianas PhD thesis work with François Pottier: A Hoare Logic for Call-by-Value Functional Programs (MPC'08). This work was extended to cover the usual ML side-effects by Johannes Kanig and Jean-Cristophe Filliatre in 2009: Who: A Verifier for Effectful Higher-order Programs.

10

Here's a fun one, by Neil Jones and Nina Bohr: Call-by-value Termination in the Untyped $\lambda$-calculus It shows how to apply the size-change analysis (a type of control flow analysis that detects infinite loops) on untyped $\lambda$-terms. This is quite nice in practice, but of course is restricted to $\lambda$-terms without defined constants (though ...

10

You're quite right that the "queue = two lists" approaches don't give you the running time you want when you have the ability to re-use earlier versions. To get O(1) running time (amortized or worst case), you need a way to reverse the rear list and append it to the front list incrementally. Instead of doing the reverse&append all at once, taking O(N) ...

10

The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan Davies and Frank Pfenning's A Judgmental Reconstruction of Modal Logic, which gives a constructive proof theory for S4 modal logic with box and diamond, and ...

9

9

One of the very first applications of category theory to a subject outside of algebraic geometry was to parsing! The keywords you want to guide your search are "Lambek calculus" and "categorial grammar". In modern terms, Joachim Lambek invented noncommutative linear logic in order to model sentence structure. The basic idea is that you can give basic parts ...

9

It's not entirely clear what do you mean by a functional programming language without closures. Can you give an example? Functional programming languages are usually based on lambda calculus, whose essential part is that you can have open lambda terms. For example the term for the constant function (the K-combinator) $\lambda x . \lambda y . x$ can be ...

9

I think that the type system you want is elementary affine logic with fixpoints. A distinctive feature (actually, the distinctive feature) of light logics, including elementary linear/affine logic, is that types do not ensure termination: unlike usual logical system, cut-elimination follows from a structural property of proofs (namely, stratification), the ...

9

For question 1, the answer is no, and is no for almost any type discipline (except certain intersection types): the fact that a term is (strongly or weakly) normalizable does not imply in general that it is typable. Typability implies termination, not the other way around. The specific case of of $\lambda EA$, however, brings up another issue which may be ...

9

I think you are looking for a typed variant of anti-unification. Anti-unification can be described as follows. First, suppose that we have a grammar of terms as follows: t ::= () | (t, t) | C t | X Here, () and (t, t) denote units and pairs, C t is a term with a leading constructor, and X is a term variable, which could be substituted for any term. The ...

8

The Rule 110 cellular automaton (often simply Rule 110) is an elementary cellular automaton with interesting behavior on the boundary between stability and chaos. In this respect it is similar to Game of Life. Rule 110 is known to be Turing complete. This implies that, in principle, any calculation or computer program can be simulated using this automaton. ...

8

There is a paper in this year's ICFP, refinement types for Haskell. The paper deals with termination checking rather than full Hoare logic, but hopefully that's a start in this direction. The related work section in that paper contains some pointers, such as Xu, Peyton-Jones, and Claessen's static contract checking for Haskell, and Sonnex, Drossopoulou, and ...

8

Agda is a dependently typed programming language and/or proof assistant for Martin-Löf type theory. Programming in Agda feels very much like programming in Haskell. For example, inductive proofs are written as recursive functions with multiple equations that pattern match on the function arguments. So programming and/or proving in Agda is a good way to learn ...

7

There is a popular formal system called Lambda calculus. It is Turing complete and has great importance in the theory of programming languages. Lambda calculus is based on anonymous functions with very simple syntax. You start a new function with a $\lambda$, list the arguments, place a dot, and write down the return value. For example, $\lambda x.x$ is the ...

7

The closest I've seen to an answer to this question is the first picture in the Gallery of Doctor Melliès, illustrating the map $$\neg\neg A \otimes \neg\neg B \longrightarrow \neg\neg(A \otimes B)$$ which exists in any dialogue category (i.e., a monoidal category with closures into a fixed object). Note that the left-to-right CPS transform of general ...

7

Following up on the 2012 paper linked above, the work on RRB vectors has since been extended and published in ICFP'15. RRB vector: a practical general purpose immutable sequence http://dl.acm.org/citation.cfm?id=2784739

7

Yes, the Foetus checker can typecheck everything in Goedel's T. You can show this by using the checker to show that the iteration operator in T is terminating. For example, the following definition will work:  \begin{array}{lcl} \mathit{iter} & : & A \to (A \to A) \to \mathbb{N} \to A \\ \mathit{iter} \;i \;f \;0 & = & i \\ \mathit{iter} ...

Only top voted, non community-wiki answers of a minimum length are eligible