The tag has no usage guidance.

learn more… | top users | synonyms

-2
votes
0answers
24 views

Rectangular and n-Dimensional Pairing Functions?

Has anyone worked out a "rectangular" or $n$-dimensional variant of Szudzik's pairing function? It is useful anytime you want to enumerate a product of finite sets, or map a finite set into a product ...
0
votes
1answer
33 views

Observational Equivalence of open terms in PCF

The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms. Lets consider the simple case where the terms ...
-2
votes
1answer
77 views

Can we say that Church encoding is a form of Gödelization?

We see here the following statement about Godelization: Gödel numbering in computer science means more or less "source code" and "data in binary format", so I hope the significance of this should ...
1
vote
0answers
30 views

Best Asymptotic Complexity for Persistent Union Find

In this paper https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf, they claim to have a practically fast persistent union-find data structure for most use-cases, but it's still not polylogarithmic ...
7
votes
1answer
202 views

What type system fits the subclass of λ-terms that can be reduced optimally?

There is a subset of λ-calculus terms that can be reduced by Lamping's Abstract Algorithm without using the Oracle. That is an interesting subset, because only for those terms it is proven that ...
0
votes
0answers
23 views

What is the power and limits of fold/reduce in distributed computing?

It seems most operations on data can be theoretically handled by some construct of fold/reduce. Is there a theory of what is possible and what isn't with fold?
1
vote
0answers
23 views

Efficient compilation of interaction combinators with infinite cell types to usual interaction combinators?

It is known that interaction combinators can implement any interaction net system efficiently. Now, let us define a modification of interaction combinators, which, instead of two types of fan cells, ...
1
vote
1answer
86 views

Is the topsort from “Structuring Depth-First Search Algorithms” guaranteed to be (reverse) stable?

In "Structuring Depth-First Search Algorithms in Haskell", implemented in Data.Graph in the Haskell standard library, an algorithm for topologically sorting graphs is given: ...
-2
votes
2answers
179 views

How to implement a functional programming language efficiently?

Thanks to Petr and Andrej for their feedback. I'm rephrasing my question and give a bit of a context: Functional programming languages are mostly based on lambda calculus. Implementing a functional ...
10
votes
1answer
164 views

How do you encode Lamping's abstract algorithm using interaction combinators?

Interaction combinators have been proposed as a compile target for the λ-calculus before. That paper implements the full λ-calculus. It is also known that it is possible to optimize interaction-net ...
6
votes
0answers
85 views

Is it possible to unambiguously read back λ terms from interaction nets without node types?

A class of lambda terms can be evaluated using Lamping's abstract algorithm - that is, converting them to interaction nets and applying a set of rules. In order to get the result, you have to read ...
2
votes
1answer
80 views

Is there a pair of different lambda terms in the normal form that behave identically when applied to any input?

Let f and g be lambda terms in the normal form, such that f is intensionally different from ...
9
votes
2answers
235 views

Category theory and parsers — references wanted

Since I'm interested in parsers (mainly in parser expression grammars), I'm wondering if there's some work that gives a categorical treatment of parsing. Any reference on applications of category ...
10
votes
1answer
177 views

Type systems preventing laziness-related memory leaks?

Perhaps the main source of performance problems in Haskell is when a program inadvertently builds up a thunk of unbounded depth - this causes both a memory leak and a potential stack overflow when ...
3
votes
0answers
164 views

Distributive law between monads in Haskell

A distributive law between monads must satisfy laws that are usually given in terms of the units $\eta$ and multiplications $\mu$ of the two monads. Among the four laws there are: $\mu^S T \circ S l ...
5
votes
0answers
283 views

Is there a purely functional vector with O(1) access to the front and back but O(log n) concatenation?

Context: For fun and perhaps for actual use, I'm making my own programming language that would compile to Typed Racket, a statically-typed Lisp dialect. One of the major features I want to implement ...
3
votes
2answers
97 views

Typechecking liveness properties of coprograms

Clarification: in Total Functional Programming terminology, a program terminates with useful input, while a coprogram doesn't necessarily terminates, and repeatedly produces useful input. I am ...
0
votes
1answer
54 views

Can we design our own `if` clause in Normal Order evaluation

I have been reading SICP and have been thinking over a thing for quite some time related to evaluation using Substitution with ...
6
votes
0answers
90 views

Purely functional uniquely-represented deques

There are a number of purely functional deques that support $O(1)$ operations at each end. None that I know of are "uniquely represented" - deques with the same number of items can have different ...
4
votes
2answers
162 views

Can programming help one understand constructive mathematics?

I have read about the principles of constructive mathematics, for example, the principle of excluded middle is not allowed, and now I want to do some exercises to increase my understanding of the ...
23
votes
5answers
1k views

Are there any annotated formal verification systems for pure functional programming languages?

ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified. I have not looked into it, but I imagine that the ...
8
votes
2answers
315 views

Explaining monad transformers in categorical terms

Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers. How could monad transformers be described in the terms ...
5
votes
0answers
180 views

Generalizing Haskell: could we replace Hask with Cat?

N.B. I asked the same question on Stack Overflow but it was suggested that it is too theoretical for this forum. It is great that Haskell allows us to walk around in the category $Hask$. But ...
4
votes
2answers
166 views

Isomorphism between algebraic data-types

I have two types of trees in Haskell, defined as the least solution of the following equations: $T_1(A) \cong 1 + A + T_1(A) \times T_1(A)$ $T_2(A) \cong 1 + A \times T_2(A) + T_2(A) \times T_2(A)$ ...
4
votes
1answer
159 views

How can the actor model be applied to allow pure functional languages to have side-effects?

I just read this blog post which argues that monads might be too obscure or difficult to understand as the default "interface to the impure world" in purely functional programming languages; instead, ...
7
votes
1answer
149 views

Are there stronger notions of equivalence over lambda terms than beta equivalence?

I should add the context that I am concerned with strongly normalizing systems like System-F. I have what I consider a very strong notion of equivalence for lambda terms that goes something like the ...
2
votes
0answers
156 views

Is there any system where function equality (extensionality) is decidable?

Is there any programming language or system where function equality (extensionality) is decidable?
6
votes
0answers
233 views

Complete combinator basis for System F-omega

The S and K combinators form a complete (and Turing complete) basis when untyped. Within the Hindley-Milner type-system, and I believe within system $F$ as well, S and K can encode any well-typed ...
3
votes
1answer
140 views

A curious Wilf equivalence class of function compositions

I was enumerating pairs of functions from a size $n$ set into itself, and ran into these three relations which all generate the same integer sequence starting at index zero: 1, 1, 6, 87, 2200, 84245. ...
3
votes
1answer
784 views

Terminology for f(g(x)) = g(f(x))

There is a paper by Ritt from 1923 that calls the relation, $f(g(x)) = g(f(x))$, permutable functions. Is there a more recent terminology used in the literature, or is this still the standard?
10
votes
1answer
330 views

Algorithm to determine function equality on the simply typed lambda calculus?

We know that beta-equality of simply typed lambda-terms is decidable. Given M,N:σ→τ, is it decidable whether for all X:σ, MX $≃_β$ NX?
9
votes
1answer
196 views

What exactly does “semantically observable” side-effect mean?

I have question regarding pure functions. According to the Wikipedia page one of the requisites for a pure function is : Evaluation of the result does not cause any semantically observable side ...
8
votes
3answers
331 views

Is the class of primitive recursion functionals equivalent to the class of functions which Foetus proves to terminate?

Foetus, if you have not heard of it, can be read up on here. It uses a system of 'call matrices' and 'call graphs' to find all 'recursion behaviors' of recursive calls in a function. To show that a ...
16
votes
1answer
462 views

What are the practical issues with intersection and union types?

I'm designing a simple statically typed functional programming language as a learning experience. It appears that the type system I have implemented so far could (with a little extra work) ...
6
votes
3answers
656 views

How to make the Lambda Calculus strong normalizing without a type system?

Is there any system similar to the lambda calculus that is strong normalizing, without the need to add a type system on top of it?
4
votes
2answers
442 views

What is higher-order in higher-order abstract syntax?

I understand that using higher-order abstract syntax essentially means using host (meta) language abstraction facilities to represent binders in embedded (object) language. But, Why exactly is it ...
2
votes
0answers
104 views

Evaluation contexts: outside-in vs inside-out

I heard that there exist two styles to define an evaluation context: outside-in and inside-out. Can someone give the definitions? Why are they so named (inside-out and outside-in)? What is the ...
2
votes
1answer
243 views

Learning road map for functional programming from the viewpoint of category theory

I am now considering about studying functional programming from the viewpoint of category theory. There are a lot of books about functional programming and category theory, I want some suggestions ...
1
vote
2answers
196 views

Using partial functions to prove correctness

I'm interested in proving that a program (which may or may not terminate) will give the correct answer if it terminates. Given: $P$ is a family of programs, parameterized by a function $f$. Write ...
1
vote
3answers
467 views

Is there an array structure that allows for O(1) complexity for reverse, zip, slice etc operations?

Many operations on arrays have $O(n)$ complexity. If we represent arrays as accessors methods, many of them could be done in $O(1)$. For example, the $i$th item in the reverse of an array $A$ of ...
13
votes
2answers
459 views

Continuation passing transform of binary functions

Recall the continuation passing transform (CPS transform) which takes $A$ to $\beta A \mathrel{{:}{=}} R^{R^A}$ (where $R$ is fixed) and $f : A \to B$ to $\beta f : \beta A \to \beta B$ defined by ...
1
vote
3answers
243 views

“lambda” term usage in programming

could any one please let me know what is the relation between "lambda" and anonymous functions in programming? in other words why we say lambda function to an anonymous function? I am here trying to ...
1
vote
1answer
145 views

A few questions about ISWIM

I recently read Landin's paper "The Next 700 Programming Languages". But I was a bit confused by ISWIM. In particular, are functions first-class objects in ISWIM? It seems not because every ...
1
vote
8answers
1k views

What are the simplest turing-complete systems? [closed]

Lambda Calculus is very simple. Are there even simpler turing-complete systems? Which is the simplest of them all?
5
votes
1answer
758 views

Trampoline that automatically balances heap and stack

While working through Fogus' Functional Javascript, I came across the trampoline function, which can be used to make safe recursive functions that don't blow up the stack. In Fogus' words, "Of course ...
5
votes
2answers
493 views

Formal representation of algorithm using recursive algebraic data types

I have an algorithm written in Haskell which I am describing in my thesis. In the code for the algorithm I have a recursive data type similar to this: data Data = A Int | B Data | C Data Now I ...
0
votes
1answer
193 views

Newbie question: Meta-functions?

Consider a function F that takes a function and produces a function based on structure of the input function. As an example consider F that takes all functions having at least two conditionals and ...
4
votes
1answer
314 views

Is there any work on purely functional approximation algorithms?

It seems to me that approximating a solution to an NP-hard problem would be especially hard for the functional programmer. For example, graph problems are commonly NP-hard. But graphs are ...
8
votes
2answers
627 views

Free theorems, where?

I've found this webapp which lets you generate a free theorem for a given type. The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of ...
11
votes
2answers
902 views

What is a zipper, and how does it relate to a tree-like structure?

I was reading a chapter in LYAH which didn't really make sense to me. I understand that zippers can arbitrarily traverse a tree-like structure, but I need some clarification on it. Also, can zippers ...