(Co)-monads and terminating implementations

Suppose we set $ \mathbb{M} \alpha := r \to \alpha$ , where $ r$ is some fixed type, and $ \alpha$ an arbitrary type, of the STLC (Simply-Typed Lambda Calculus)

Suppose we want to define a co-monad, which contains Co-unit and Co-join, with the following types (where $ \mathbb{M}$ binds more tightly than $ \to$ and $ \mathbb{M}$ is as stated above):

  1. Co-unit $ \;\;\;\; \mathbb{M} \alpha \to \alpha$
  2. Co-join $ \;\;\;\;\mathbb{M}\mathbb{M} \alpha \to \mathbb{M} \alpha$

I have been told that this will not work and that we could not create a co-monad in this way, since there is no terminating implementation for the type $ (e \to a) \to a$ .

But in the pure STLC all terms are "terminating"(i.e, reductions always lead to a (unique) normal form). So I don’t understand how this comment can be relevant in the case of the STLC.

Is there some link between (co)-monads and terminating implementations? Or is this just about creating a co-monad in Haskell?

Why would we not be able to construct a co-monad in the way described above?

Probability of terminating in a state in a probabilistic algorithm

Suppose i have a circular array of $ n$ elements. At time $ t=0$ i am in position 0 of the array. The algorithm moves left or right with probability $ p=1/2$ (since the array is circular when it moves left from 0 it goes to position $ n$ ). When i visited all the positions at least once the algorithm returns the position it terminated into.
Launching the algorithms many times shows that it stops with the same probability in any of the n positions (except for zero obviously). How do i demonstrate that the probability of ending up in each state is uniform?
My understanding is that this process is explained by a doubly stochastic Markov chain, but is there a theorem i can quote about this specific case?

Proof strategy to show that an algorithm cannot be implemented using just hereditarily terminating procedures

I am taking my question here from there. Consider the following scenario:

You are given a fixed programming language with no nonlocal control flow constructs. In particular, the language does not have

  • Exceptions, first-class continuations, etc.
  • Assertions, in the sense of “runtime tests that crash the program if they fail”.

Remark: An example of such a language could be Standard ML, minus the ability to raise exceptions. Inexhaustive pattern matching implicitly raises the Match exception, so it is also ruled out.

Moreover, you are forced to program using only hereditarily terminating values. Inductively, we define hereditarily terminating values as follows:

  • Data constructors (including numeric and string literals) are hereditarily terminating.
  • Applications of data constructors to hereditarily terminating arguments are hereditarily terminating.
  • A procedure f : foo -> bar is hereditarily terminating if, for every hereditarily terminating x : foo, evaluating the expression f x always terminates and the final result is a hereditarily terminating value of type bar.

Remarks:

  • Hereditarily terminating procedures need not be pure. In particular, they may read from or write to a mutable store.

  • A procedure is more than just the function it computes. In particular, functions do not have an intrinsic asymptotic time or space complexity, but procedures do.


Hereditarily terminating procedures formalize my intuitive idea of “program that is amenable to local reasoning”. Thus, I am interested in what useful programs one can write using only hereditarily terminating procedures. At the most basic level, programs are built out of algorithms, so I want to investigate what algorithms are expressible using only hereditarily terminating procedures.

Unfortunately, I have hit an expressiveness ceiling much earlier than I expected. No matter how hard I tried, I could not implement Tarjan’s algorithm for finding the strongly connected components of a directed graph.

Recall that Tarjan’s algorithm performs a depth-first search of the graph. In addition to the usual depth-first search stack, the algorithm uses an auxiliary stack to store the nodes whose strongly connected components have not been completely explored yet. Eventually, every node in the current strongly connected component will be explored, and we will have to pop them from the auxiliary stack. This is the step I am having trouble with: The loop that pops the nodes from the stack terminates when a given reference node has been found. But, as far as the type checker can tell, the reference node could not be in the stack at all! This results in an extra control flow path in which the stack is empty after popping everything from it and still not finding the reference node. At this point, the only thing the algorithm can do is fail.

This leads to the following…

Conjecture: Tarjan’s algorithm cannot be implemented in Standard ML using only hereditarily terminating procedures.

My questions are:

  1. What kind of proof techniques would be necessary to prove the above conjecture?

  2. What is the bare minimum type system in which Tarjan’s algorithm can be expressed as a hereditarily terminating program? That is, what is the bare minimum type system that can “understand” that the auxiliary stack is guaranteed to contain the reference node, and thus will not add a control flow path in which the auxiliary stack is empty before the reference node has been found?


Final remark: It is possible to rewrite this program inside a partiality monad. Then every procedure would be a Kleisli arrow. Instead of

val tarjan : graph -> scc list 

we would have something like

val tarjan : graph -> scc list option 

But, obviously, this defeats the point of the exercise, which is precisely to take out the procedure out of the implicit partiality monad present in most programming languages. So this does not count as a solution.

Ubuntu 19.04 xrdp server terminating connection immediately

I just made a fresh install of Ubuntu 19.04 into a VM. Installed xrdp via apt. Left everything on default: I believe this is how my 18.04 worked perfectly.

However, trying to connect to this VM via Remmina or Windows RDP client fails. Remmina shows a bit more because it attempts reconnection and so the result looks like this:

The login screen appears, login dialog shows but then immediately the connection is dropped.

This loops indefinitely with Remmina, but doesn’t even show with Windows RDP client.

Tried the same with kubuntu 19.04 but result remains the same.

Игра “Змейка” с ошибкой “Process is terminating due to StackOverflowException.”

для школьного проекта пишу змейку на c#. Имеется 3 класса: главный класс игры Programm, Snake и FoodFactory. При реализации передвижения хвостовых частей с помощью рекурсии (иного решения в голову не идет) возникает ошибка. Спасибо.

Programm.cs

using System; using System.Threading; using System.Collections.Generic; using System.Linq;  namespace std {     class Game     {         static void Main()         {             int n = 7;             char[,] field = new char[n, n];              for (int i = 0; i < n; i++)             {                 for (int j = 0; j < n; j++)                     if (i == 0 || i == n-1 || j == 0 || j == n-1)                     {                         field[i, j] = '#';                     }                     else                     {                         field[i, j] = ' ';                     }             }             FoodFactory.generateNewFood(field, n);              //show(field, n);             Snake snake = new Snake(2,1, field);              while (true)             {                 Console.Clear();                 show(field, n);                 char c = (char)Console.Read();                  if (c == 'w')                 {                     field = snake.move( snake.x - 1 , snake.y, field);                 }                 if (c == 's')                 {                     field = snake.move(snake.x + 1, snake.y, field);                 }                 if (c == 'a')                 {                    field =  snake.move(snake.x , snake.y - 1, field);                 }                 if (c == 'd')                 {                     field = snake.move(snake.x, snake.y + 1, field);                 }              }          }// Main()           public static void show(char[,] field, int n)         {             for (int i = 0; i < n; i++)             {                 for (int j = 0; j < n; j++)                 {                     Console.Write(field[i, j]);                 }                 Console.Write("\n");             }         }     } } 

Snake.cs

using System; using System.Collections.Generic; using System.Linq;  namespace std {     internal class Snake     {         public int x;         public int y;         private int x0;         private int y0;         private char HeadSnake;         private Snake anotherBody = null;         private static List<Snake> snakes = new List<Snake>();         private static FoodFactory foodFactory  = new FoodFactory ('0');         public bool isFeed = false ;           public Snake(int x, int y, char [,] field)         {             this.x = x;             this.y = y;             field[x, y] = '@';         }          public char[,] move(int x1, int y1, char[,] mainField)         {             char[,] field = mainField;             if (field[x1, y1] == '#' || field[x1, y1] == '@')             {                 theEnd();              }               if (field[x1, y1] == '0')             {                 isFeed = true;                 anotherBody = new Snake(x1,y1,field);                 field = FoodFactory.generateNewFood(field, 7);             }              x0 = x;             y0 = y;             field[x, y] = ' ';             x = x1;             y = y1;             field[x, y] = '@';              if (anotherBody != null)             {                 field = anotherBody.move(x0, y0, field, isFeed);              }              isFeed = false;             return field;         }          public char[,] move(int x1, int y1, char[,] mainField, bool Feed)         {             char[,] field = mainField;              if (Feed)             {                 isFeed = true;                 anotherBody = new Snake(x1,y1,field);              }              x0 = x;             y0 = y;             field[x, y] = ' ';             x = x1;             y = y1;             field[x, y] = '@';              if (anotherBody != null)             {                 field = anotherBody.move(x0, y0, field, isFeed);              }              return field;         }          public static void theEnd () {                 Console.Clear();                  Console.WriteLine("YOU LOSE");                 Console.ReadKey();          }     } } 

Checked luggage & terminating trip during layover

I have a Canada bound Delta flight next month with a layover in New York where I plan to abandon the trip (the flight to Canada was cheaper than to USA, hidden city ticketing).

Now I know all international flights stopping over in the USA requires passengers to deplane, pass through immigration and customs with their bags and then check in to their local connecting flight so I should have no problem retrieving my checked bags.

My question is for other countries where one doesn’t get access to checked bags during international layovers, are the airlines mandated to return passengers luggage to me at the location where a passenger decides to abandon the remaining legs of the trip? Or airlines have the right to deliver it to the final purported destination and it’s up to the passengers to figure out how to retrieve it?

Terminating app due to uncaught exception ‘NSInvalidArgumentException’, reason: ‘Receiver () has no segue with identifier ‘pizzaSegue’ [migrated]

I am new to swift programming and running into errors with performing a segue from a tableview cell when it is pressed to a view controller giving details about that cell. The error I am getting is: Terminating app due to uncaught exception ‘NSInvalidArgumentException’, reason: ‘Receiver () has no segue with identifier ‘pizzaSegue”

I have already tried the following: 1) Tried renaming the storyboard and make sure to set the main storyboard in the project settings and in the info.plist file (Key is ‘Main storyboard file base name’). I currently have the storyboard named: “Main.storyboard”

2) Tried doing a clean of the product (Product -> Clean) and rebuild but this gives same error

3) I have tried deleting the app from the simulator and running it again

4) I have double checked and the segue identifier in interface builder is called “pizzaSegue” and it is the same in my code.

import UIKit import Alamofire  struct Drink {     let id: String     let name: String     let description: String     let amount: Float     let image: UIImage      init(data: [String: Any]) {         self.id = data["id"] as! String         self.name = data["name"] as! String         //self.amount = data["amount"] as! Float         self.amount = ((data["amount"] as? NSNumber)?.floatValue)!         self.description = data["description"] as! String         self.image = data["image"] as! UIImage     } }  class DrinkTableViewCell: UITableViewCell {     @IBOutlet weak var cellName: UILabel!     @IBOutlet weak var cellAmount: UILabel!     @IBOutlet weak var cellDescription: UILabel!     @IBOutlet weak var cellImage: UIImageView!      override init(style: UITableViewCell.CellStyle, reuseIdentifier: String!) {         super.init(style: style, reuseIdentifier: reuseIdentifier)     }      required init?(coder aDecoder: NSCoder) {         fatalError("init(coder:) has not been implemented")     }  }  class DrinkListTableViewController: UITableViewController {      var drinks: [Drink] = []      override func viewDidLoad() {         super.viewDidLoad()         navigationItem.title = "Drink Selection"         tableView.dataSource = self         tableView.delegate = self         //tableView.register(DrinkTableViewCell.self, forCellReuseIdentifier: "cell")          tableView.register(DrinkTableViewCell.self as AnyClass, forCellReuseIdentifier: "cell")          //tableView.register(UINib(nibName: "DrinkTableViewCell", bundle: Bundle.main), forCellReuseIdentifier: "cell")          //tableView.estimatedRowHeight = 134         //tableView.rowHeight = UITableView.automaticDimension          fetchInventory { drinks in             guard drinks != nil else { return }             self.drinks = drinks!             //print("Data from API call: ", self.drinks)             //self.tableView.reloadData() //            DispatchQueue.main.async { [weak self] in //                self?.tableView.reloadData() //            }         }     }      override func viewDidAppear(_ animated: Bool) {         super.viewDidAppear(animated)         DispatchQueue.main.async { [weak self] in             self?.tableView.reloadData()         }     }       override func tableView(_ tableView: UITableView, didSelectRowAt indexPath: IndexPath) {             performSegue(withIdentifier: "pizzaSegue", sender: self.drinks[indexPath.row] as Drink)         //trying another method below?         //self.navigationController?.pushViewController(UIViewController() as! PizzaViewController, animated: true)     }        override func prepare(for segue: UIStoryboardSegue, sender: Any?) {          if segue.identifier == "pizzaSegue" {             guard let vc = segue.destination as? PizzaViewController else { return }             vc.pizza = sender as? Pizza         }     }      private func fetchInventory(completion: @escaping ([Drink]?) -> Void) { Alamofire.request("http://127.0.0.1:4000/inventory", method: .get)         .validate()         .responseJSON { response in             guard response.result.isSuccess else { return completion(nil) }             guard let rawInventory = response.result.value as? [[String: Any]?] else { return completion(nil) }             let inventory = rawInventory.compactMap { pizzaDict -> Drink? in                 var data = pizzaDict!                 data["image"] = UIImage(named: pizzaDict!["image"] as! String)                 //print("Printing each item: ", Drink(data: data))                 //printing all inventory successful                 return Drink(data: data)             }             completion(inventory)     } }      // MARK: - Table view data source      override func numberOfSections(in tableView: UITableView) -> Int {         return 1     }      override func tableView(_ tableView: UITableView, numberOfRowsInSection section: Int) -> Int {         print("ROWS: ", drinks.count)         return drinks.count     }       override func tableView(_ tableView: UITableView, cellForRowAt indexPath: IndexPath) -> UITableViewCell {          //let cell = tableView.dequeueReusableCell(withIdentifier: "cell", for: indexPath) as! DrinkTableViewCell          //let cell = UITableViewCell(style: UITableViewCell.CellStyle.subtitle, reuseIdentifier: "cell")          let cell:DrinkTableViewCell = self.tableView.dequeueReusableCell(withIdentifier: "cell") as! DrinkTableViewCell          //cell.cellName?.text = drinks[indexPath.row].name         //cell.cellAmount?.text = String(drinks[indexPath.row].amount)         //cell.cellDescription?.text = drinks[indexPath.row].description         //cell.cellImage?.image = drinks[indexPath.row].image          cell.imageView?.image = drinks[indexPath.row].image         cell.textLabel?.text = drinks[indexPath.row].name         cell.detailTextLabel?.text = drinks[indexPath.row].description          //print(cell.textLabel?.text)         //print(cell.detailTextLabel?.text)          print(cell.cellName?.text as Any)         //print(cell.cellImage?.image)         return cell     }       override func tableView(_ tableView: UITableView, heightForRowAt indexPath: IndexPath) -> CGFloat {      return 100.0      }  } 

Screenshot showing error in console and the segue identifier in storyboard